"Broken" proofs after tlaps upgrade

[JosEdu Solsona]

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.

[Saksham Chand]

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

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

[Leslie Lamport]

Saksam is right about improvements to provers often breaking some

proofs.  However, I'm afraid that people may find more previously

successful proofs breaking than they should.  This is because there

were bugs in the previous version that could have allowed TLAPS to

prove false assertions.  Fixing those bugs has made it not prove some

things it used to.  We believe it is unlikely that any assertions

people actually proved with the previous version were not true.

However, if you find that this did happen, please send us the proof in

which it did.  We will add it to our regression tests to help us

make sure that those bugs do not reappear.

We apologize for this, and we are working to make the prover again

prove the correct assertions that it used to.

Leslie

[Stephan Merz]

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

On 6 Mar 2020, at 03:23, Saksham Chand <sch...@cs.stonybrook.edu> wrote:

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 <josedu...@gmail.com> 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:

<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+u...@googlegroups.com.
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+u...@googlegroups.com.

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.

[José Eduardo Solsona]

Thanks for the response Saksham, Leslie and Stephan.

Indeed, when the proof was not passing, the first thing i tried was to change the prover invocation to something more explicit. But it didn't help.

Im aware about the default dir recomendation, so im using "/usr/local/bin/tlaps".  For more info, the machine is an "old" Intel Core 2 Duo - 4GB RAM - Win7 64-bit.

Now, using the verbose flag as Stephan suggested, i share my current output next. From what i can tell, i think Z3 (SMT) was found. 
Also, if i try to prove something like:

THEOREM \A x \in Nat: x=0 => x=0+1
  BY Z3

it gives me "status:failed" (although passes ok with OBVIOUS calling Isabelle), but i don't interpret that as if Z3 is missing.

Could be Z3 broken somehow?.

The prover output: 

---------------- New Prover Launch --------------
cygpath: can't convert empty path
sh: line 0: type: cvc4: not found
sh: line 0: type: yices: not found
sh: line 0: type: veriT: not found
sh: line 0: type: SPASS: not found
-------------------- tlapm configuration --------------------
version == "1.4.5 (build 33809)"
built_with == "OCaml 4.04.2"
tlapm_executable == "/usr/local/bin/tlapm"
max_threads == 2
library_path == "/usr/local/lib/tlaps"
search_path == << "C:\cygwin\usr\local\lib\tlaps\"
                , "/usr/local/lib/tlaps" >>
Isabelle == "PATH= ...; isabelle-process -r -q -e \"(use_thy \\\"$file\\\"; writeln \\\"((TLAPS SUCCESS))\\\");\" TLA+"
Isabelle version == "Isabelle2011-1: October 2011"
zenon == "PATH= ...; zenon -p0 -x tla -oisar -max-time 1d \"$file\""
zenon version == "zenon version 0.8.4 [a268] 2017-11-14"
Executable "cvc4" not found in this PATH: ...  
Executable "yices" not found in this PATH: ...  

Z3 == "PATH= ... ; z3 -smt2 -v:0 AUTO_CONFIG=false smt.MBQI=true \"$winfile\""
Executable "veriT" not found in this PATH: ...
SMT == "PATH= ... ; z3 -smt2 -v:0 AUTO_CONFIG=false smt.MBQI=true \"$winfile\""
Executable "SPASS" not found in this PATH: ...
LS4 == "PATH= ... ; ptl_to_trp -i $file | ls4"
LS4 version == "unknown"
flatten_obligations == TRUE
normalize == TRUE

where the mentioned PATH is  "/usr/bin:/cygdrive/c/Ruby26-x64/bin:/cygdrive/c/ProgramData/Oracle/Java/javapath:/cygdrive/c/Program Files/Haskell/bin:/cygdrive/c/Program Files/Haskell Platform/7.10.3/lib/extralibs/bin:/cygdrive/c/Program Files/Haskell Platform/7.10.3/bin:/cygdrive/c/Program Files/Common Files/Microsoft Shared/Windows Live:/cygdrive/c/windows/system32:/cygdrive/c/windows:/cygdrive/c/windows/System32/Wbem:/cygdrive/c/windows/System32/WindowsPowerShell/v1.0:/cygdrive/c/Program Files/Intel/WiFi/bin:/cygdrive/c/Program Files/Common Files/Intel/WirelessCommon:/cygdrive/c/Program Files/Microsoft/Web Platform Installer:/cygdrive/c/Program Files (x86)/Microsoft ASP.NET/ASP.NET Web Pages/v1.0:/cygdrive/c/Program Files (x86)/Windows Kits/8.0/Windows Performance Toolkit:/cygdrive/c/TASM/BIN:/cygdrive/c/MinGW/bin:/cygdrive/c/Program Files/Haskell Platform/7.10.3/mingw/bin:/cygdrive/c/Leksah/bin:/cygdrive/c/BNFC:/cygdrive/c/Users/JosEdu/AppData/Local/Programs/MiKTeX 2.9/miktex/bin:/cygdrive/c/Program Files/Git/cmd:/cygdrive/c/Users/JosEdu/AppData/Roaming/cabal/bin:/cygdrive/c/Users/JosEdu/AppData/Roaming/local/bin:/cygdrive/c/Users/JosEdu/AppData/Local/Programs/MiKTeX 2.9/miktex/bin/x64:/usr/local/bin:/usr/local/lib/tlaps/bin"

Thanks!

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1DB7872B-D443-4AA6-906B-7A693542C674%40gmail.com.

--

Ing. José E. Solsona