[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]


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?


Attachment: eucset.tla
Description: Binary data