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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d4803d48-5ab7-41ca-b6f0-0ae96e41db25%40googlegroups.com.