# [tlaplus] "Broken" proofs after tlaps upgrade

Hello all,

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, mInit == h \in 1..12 /\ m \in 0..59Next == /\ 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.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.