I updated toolbox to 1.6 and tlaps to 1.4.5. Some of my previously proved assertions are not passing.
As an example, for the Hour-Minute clock spec i had:
VARIABLES h, m
Init == h \in 1..12 /\ m \in 0..59
Next == /\ m' = IF m # 59 THEN m + 1 ELSE 0
/\ m < 59 => UNCHANGED h
/\ m = 59 => h' = IF h # 12 THEN h + 1 ELSE 1
Spec == Init /\ [][Next]_<<h,m>>
-----------------------------------------------------------------------------
TypeOk == h \in 1..12 /\ m \in 0..59
The proof state now:
This is typically happening on sub-proofs involving primed expressions.
Any suggestion?
Thanks.