| Hello,
Leslie explained why currently there are more regressions in the proofs than we'd like to have. We should have made this explicit in the announcement of the new version of the prover.
Returning to the example, as Saksham says, that proof should work out of the box. The failure of the proof of <2>1 could indicate that the PM does not find an SMT solver. You can pass the "--verbose" flag to the prover (invoke the prover using C-G C-P and add --verbose in the field for additional command-line options) to get more detailed output on the invocation of the backends in the TLAPM console.
The default SMT solver is now Z3, and a recent version of Z3 is contained in the distribution. It is not recommended to change the default installation directory (/usr/local/bin/tlaps).
Best regards, Stephan
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 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: <capt.PNG>
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.
-- 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/CAJSuO--nzJ1k8SYYyQTf%2BQMFcT%2BLfrize6TZpzn%2B5b0S-%3D_A1A%40mail.gmail.com.
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/1DB7872B-D443-4AA6-906B-7A693542C674%40gmail.com.
|