# Re: [tlaplus] "Broken" proofs after tlaps upgrade

I have had many previous experiences with proofs breaking as the toolbox updates. Although not with the v1.6. Also, the obligation you pointed is proved on my machine (it's a 6th gen i5 processor dual core, 8gb ram)

With an ever evolving system like TLA+ I think it is not unreasonable to expect some proofs breaking as versions update. I typically try invoking Z3 explicitly first, especially for arithmetic and algebraic obligations. If that doesn't work, I just break the proof down a bit more and make certain "EXCEPT" statements in the obligation as subgoals and that usually clears things out.

Hope this helps,
Saksham

On Thu, Mar 5, 2020, 9:01 PM JosEdu Solsona <josedusolsona@xxxxxxxxx> wrote:
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, 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.

--
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.