Hi,
When I check a constant expression with the TLA+ Tool box,
(Model > Model Checking Results : Evaluate constant expression),
I get the following error
"Level error in applying operator $Tuple:
The level of argument 2 exceeds the maximum level allowed by the operator"For instance, if I check the below theorem T,
/// TLA Specs: BEGINNING
EXTENDS Naturals
VARIABLE h
Init == h \in (0 .. 23)
Next == h' = (h+1)%24
Spec == Init /\ [][Next]_h
THEOREM T == Spec => []Init
/// TLA SPECS: END
then I get the error message. I am really puzzled...
Could someone please explain me (1) what does such error message mean, (2) where does the error come from, (3) how to evaluate theorems and constant expressions?
Thank you very much by advance.
Best
Gabriel