I copied the set-GCD code from the hyperbook (TLA file enclosed); model-checker keeps saying
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException: Attempted to evaluate an _expression_ of form P \/ Q when P was
a set of the form {e1, ... ,eN}.
line 31, col 34 to line 31, col 55 of module eucset
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 27, column 13 to line 27, column 24 in eucset
1. Line 28, column 13 to line 34, column 29 in eucset
2. Line 29, column 24 to line 31, column 56 in eucset
-------------------------------------------------
S has its value {6, 15, 27} from the model
Is there a simple fix?
Thanks