search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.27k stars 197 forks source link

Specs failing proof validation #67

Open ahelwer opened 1 year ago

ahelwer commented 1 year ago

I whipped up a quick script then downloaded & ran TLAPS 1.4.5 on macOS against all the modules containing proofs, and the following failed validation (no additional solvers installed, no additional command-line parameters given other than -I for include directory):

specifications/LoopInvariance/BinarySearch.tla
specifications/LoopInvariance/SumSequence.tla
specifications/Paxos/Consensus.tla
specifications/Paxos/Voting.tla
specifications/PaxosHowToWinATuringAward/Consensus.tla
specifications/PaxosHowToWinATuringAward/Voting.tla
specifications/ewd998/AsyncTerminationDetection_proof.tla
specifications/ewd998/EWD998_proof.tla
specifications/lamport_mutex/LamportMutex_proofs.tla

@muenchnerkindl I'd be interested in knowing how many of these are real proof failures and how many are due to wrong options or lack of installed solvers. My script was very simple, it just ran tlapm against each file and printed out the path if it returned a nonzero error code.

ahelwer commented 1 year ago

I re-ran the script using the 202210041448 1.5.0 pre-release and these are the list of failures instead:

Succeeded in 1.4.5 but fail in 1.5.0:

specifications/Bakery-Boulangerie/Bakery.tla
specifications/Bakery-Boulangerie/Boulanger.tla

Fail in both 1.4.5 and 1.5.0:

specifications/LoopInvariance/BinarySearch.tla
specifications/Paxos/Consensus.tla
specifications/Paxos/Voting.tla
specifications/PaxosHowToWinATuringAward/Consensus.tla
specifications/PaxosHowToWinATuringAward/Voting.tla
specifications/ewd998/EWD998_proof.tla
specifications/lamport_mutex/LamportMutex_proofs.tla

Upgrading to 1.5.0 fixed these proofs:

specifications/LoopInvariance/SumSequence.tla
specifications/ewd998/AsyncTerminationDetection_proof.tla
will62794 commented 1 year ago

@ahelwer If it might be of any help, I wrote a small Python script a bit ago to parse the command line output of the TLAPS proof manager into a slightly more structured format. Just wanted to mention it in case it might be helpful to build on at any point e.g. to improve proof checking diagnostics in future.

ahelwer commented 1 year ago

@will62794 that's very cool, and a neat project! Is the python script published as a module on pypi?

muenchnerkindl commented 1 year ago

Thanks for checking the proofs in the examples repository. I fixed most of the broken proofs, except for the ones in LamportMutex_proofs that I'm still working on: we had to dumb down the SMT backend because it was getting a little too smart, and this broke a number of legitimate proofs.

I think the lesson for us is that we should consider the proofs in this repository, as we do for the examples in the prover distribution. For an interactive proof system, it doesn't make sense to promise backward compatibility. Some changes may be considered beneficial overall but still break existing proofs. But we should do a best-effort attempt at fixing proofs that we break.

The detail of what I found is below.

specifications/LoopInvariance/BinarySearch.tla fixed (UNCHANGED not taken into account)

specifications/LoopInvariance/SumSequence.tla works for me

specifications/MisraReachability/ParReachProofs.tla works for me (this was mentioned in the original list but has since disappeared)

specifications/MisraReachability/ReachabilityProofs.tla idem

specifications/MisraReachability/ReachableProofs.tla idem

specifications/Paxos/Consensus.tla fixed (in fact, added the proof: the existing proof was only a sketch of what we believed that temporal proofs could look like before we had support for temporal logic in the prover)

specifications/Paxos/Voting.tla fixed (but didn't add the proof, it's available in the TLAPS distribution and should eventually be copied here)

specifications/PaxosHowToWinATuringAward/Consensus.tla as above

specifications/PaxosHowToWinATuringAward/Voting.tla as above

specifications/TwoPhase/TwoPhase.tla works for me (again, this one no longer appears above)

specifications/ewd840/EWD840_proof.tla works for me

specifications/ewd998/AsyncTerminationDetection_proof.tla as noted at the top of the module, it requires using the development version of TLAPS for checking the liveness proofs

specifications/ewd998/EWD998_proof.tla idem

specifications/lamport_mutex/LamportMutex_proofs.tla still working on those ...

I haven't looked at the proofs in Bakery-Boulangerie yet that were not in the original list.

will62794 commented 1 year ago

@helwer No, the script is not published, but feel free to extend/modify it and publish it there if you want.

ahelwer commented 1 year ago

@muenchnerkindl sorry for the false reports! Might have been some interaction of the 1.4.5 fingerprint files with the 1.5.0 fingerprint files. I deleted the .tlacache directory. The updated set of proof failures is:

specifications/Bakery-Boulangerie/Bakery.tla
specifications/Bakery-Boulangerie/Boulanger.tla
specifications/lamport_mutex/LamportMutex_proofs.tla

Finally, specifications/ewd998/EWD998_proof.tla seemingly fails due to #66:

Error: Operator "FoldFunctionOnSet" not found
 tlapm ending abnormally with Failure("Expr.Anon: 4")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from E_anon.anon#expr in file "e_anon.ml", line 226, characters 17-35
Called from E_visit.map#expr in file "e_visit.ml", line 59, characters 20-35
Called from E_anon.anon#expr in file "e_anon.ml", line 226, characters 17-35
Called from E_anon.anon_sg#defn in file "e_anon.ml", line 214, characters 14-30
Called from M_elab.normalize.spin in file "m_elab.ml", line 1368, characters 45-66
Called from M_elab.normalize in file "m_elab.ml", line 1457, characters 12-66
Called from Tlapm.process_module in file "tlapm.ml", line 293, characters 29-68
Called from Tlapm.main.f in file "tlapm.ml", line 503, characters 23-43
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 506, characters 13-40
Called from Tlapm.init in file "tlapm.ml", line 518, characters 8-33

when run with:

./tlapm-install/bin/tlapm specifications/ewd998/EWD998_proof.tla -I specifications/ewd
998 -I CommunityModules -I StandardModules

Can you help me out with caching proof results so that re-checking them is fast? How would I do that?

muenchnerkindl commented 1 year ago

For older versions of tlapm, fingerprints are stored at /path/to/module/module.tlaps/fingerprints

More recent versions store them at /path/to/module/.tlacache/module.tlaps/fingerprints

I don't think there is a command line option to change these paths so I'm assuming that if you want to persist the fingerprint files you'll have to do that in a script.

muenchnerkindl commented 1 year ago

I believe that all proofs now work again. Thanks for uncovering these issues!

ahelwer commented 1 year ago

Hi @muenchnerkindl thank you for your work! Unfortunately I am still running into issues with the following proofs, using release https://github.com/tlaplus/tlapm/releases/tag/202210041448 on Linux; click the dropdowns to see associated errors:

specifications/Bakery-Boulangerie/Bakery.tla

``` File "./specifications/Bakery-Boulangerie/Bakery.tla", line 398, characters 5-6: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, Procs == 1..N, \prec(a, b) == \/ a[1] < b[1] \/ a[1] = b[1] /\ a[2] < b[2], NEW VARIABLE num, NEW VARIABLE flag, NEW VARIABLE pc, NEW VARIABLE unchecked, NEW VARIABLE max, NEW VARIABLE nxt, ProcSet == Procs, w2(self) == /\ pc[self] = "w2" /\ \/ num[nxt[self]] = 0 \/ <> \prec <> /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] /\ pc' = [pc EXCEPT ! [self] = "w1"] /\ UNCHANGED <>, TypeOK == /\ num \in [Procs -> Nat] /\ flag \in [Procs -> BOOLEAN] /\ unchecked \in [Procs -> SUBSET Procs] /\ max \in [Procs -> Nat] /\ nxt \in [Procs -> Procs] /\ pc \in [Procs -> {"ncs", "e1", "e2", "e3", "e4", "w1", "w2", "cs", "exit"}], Before(i, j) == /\ num[i] > 0 /\ \/ pc[j] \in {"ncs", "e1", "exit"} \/ /\ pc[j] = "e2" /\ \/ i \in unchecked[j] \/ max[j] >= num[i] \/ /\ pc[j] = "e3" /\ max[j] >= num[i] \/ /\ pc[j] \in {"e4", "w1", "w2"} /\ <> \prec <> /\ pc[j] \in {"w1", "w2"} => i \in unchecked[j], Inv == /\ TypeOK /\ \A i \in Procs : /\ pc[i] \in {"e4", "w1", "w2", "cs"} => num[i] # 0 /\ pc[i] \in {"e2", "e3"} => flag[i] /\ pc[i] = "w2" => nxt[i] # i /\ pc[i] \in {"w1", "w2"} => i \notin unchecked[i] /\ pc[i] \in {"w1", "w2"} => (\A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j)) /\ (/\ pc[i] = "w2" /\ \/ pc[nxt[i]] = "e2" /\ i \notin unchecked[nxt[i]] \/ pc[nxt[i]] = "e3") => max[nxt[i]] >= num[i] /\ pc[i] = "cs" => (\A j \in Procs \ {i} : Before(i, j)), N \in Nat , Inv , [Next]_vars , NEW CONSTANT self \in Procs, <2>7 , Z3 PROVE Inv' File "./specifications/Bakery-Boulangerie/Bakery.tla", line 1, character 1 to line 457, character 77: [ERROR]: 1/121 obligations failed. ```

specifications/Bakery-Boulangerie/Boulanger.tla

``` File "./specifications/Bakery-Boulangerie/Boulanger.tla", line 490, characters 7-8: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, Procs == 1..N, \prec(a, b) == \/ a[1] < b[1] \/ a[1] = b[1] /\ a[2] < b[2], NEW VARIABLE num, NEW VARIABLE flag, NEW VARIABLE pc, NEW VARIABLE unchecked, NEW VARIABLE max, NEW VARIABLE nxt, NEW VARIABLE previous, ProcSet == Procs, TypeOK == /\ num \in [Procs -> Nat] /\ flag \in [Procs -> BOOLEAN] /\ unchecked \in [Procs -> SUBSET Procs] /\ max \in [Procs -> Nat] /\ nxt \in [Procs -> Procs] /\ pc \in [Procs -> {"ncs", "e1", "e2", "e3", "e4", "w1", "w2", "cs", "exit"}] /\ previous \in [Procs -> Nat \cup {-1}], Before(i, j) == /\ num[i] > 0 /\ \/ pc[j] \in {"ncs", "e1", "exit"} \/ /\ pc[j] = "e2" /\ \/ i \in unchecked[j] \/ max[j] >= num[i] \/ j > i /\ max[j] + 1 = num[i] \/ /\ pc[j] = "e3" /\ \/ max[j] >= num[i] \/ j > i /\ max[j] + 1 = num[i] \/ /\ pc[j] \in {"e4", "w1", "w2"} /\ <> \prec <> /\ pc[j] \in {"w1", "w2"} => i \in unchecked[j] \/ /\ num[i] = 1 /\ i < j, Inv == /\ TypeOK /\ \A i \in Procs : /\ pc[i] \in {"ncs", "e1", "e2"} => num[i] = 0 /\ pc[i] \in {"e4", "w1", "w2", "cs"} => num[i] # 0 /\ pc[i] \in {"e2", "e3"} => flag[i] /\ pc[i] = "w2" => nxt[i] # i /\ pc[i] \in {"e2", "w1", "w2"} => i \notin unchecked[i] /\ pc[i] \in {"w1", "w2"} => (\A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j)) /\ (/\ pc[i] = "w2" /\ \/ pc[nxt[i]] = "e2" /\ i \notin unchecked[nxt[i]] \/ pc[nxt[i]] = "e3") => max[nxt[i]] >= num[i] /\ (/\ pc[i] = "w2" /\ previous[i] # -1 /\ previous[i] # num[nxt[i]] /\ pc[nxt[i]] \in {"e4", "w1", "w2", "cs"}) => Before(i, nxt[i]) /\ pc[i] = "cs" => (\A j \in Procs \ {i} : Before(i, j)), N \in Nat , Inv , [Next]_vars , NEW CONSTANT self \in Procs, <3>_a23 , <3>2 , Z3 PROVE Inv' File "./specifications/Bakery-Boulangerie/Boulanger.tla", line 1, character 1 to line 532, character 77: [ERROR]: 1/125 obligations failed. ```

specifications/Paxos|PaxosHowToWinATuringAward/Consensus.tla

``` File "./specifications/Paxos/Consensus.tla", line 44, characters 5-6: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT Value, NEW VARIABLE chosen, TypeOK == /\ chosen \subseteq Value /\ IsFiniteSet(chosen), Next == /\ chosen = {} /\ \E v \in Value : chosen' = {v}, Inv == /\ TypeOK /\ Cardinality(chosen) =< 1, FS_Singleton PROVE Inv /\ Next => Inv' File "./specifications/Paxos/Consensus.tla", line 1, character 1 to line 58, character 77: [ERROR]: 1/12 obligations failed. ```

specifications/lamport_mutex/LamportMutex_proofs.tla

``` File "./specifications/lamport_mutex/LamportMutex_proofs.tla", line 667, characters 11-12: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, NEW CONSTANT maxClock, NType == N \in Nat, maxClockType == maxClock \in Nat, Clock == Nat \ {0}, NEW VARIABLE clock, NEW VARIABLE req, NEW VARIABLE ack, NEW VARIABLE network, NEW VARIABLE crit, TypeOK == /\ clock \in [Proc -> Clock] /\ req \in [Proc -> [Proc -> Nat]] /\ ack \in [Proc -> SUBSET Proc] /\ network \in [Proc -> [Proc -> Seq(Message)]] /\ crit \in SUBSET Proc, Precedes(s, mt1, mt2) == \A i, j \in 1..Len(s) : s[i].type = mt1 /\ s[j].type = mt2 => i < j, TypeOK , BasicInv , ClockInv , [Next]_vars , NEW CONSTANT n \in Proc, NEW CONSTANT k \in Proc \ {n}, m == Head(network[k][n]), <3>_a713 , NEW CONSTANT p \in Proc, NEW CONSTANT q \in Proc \ {p}, pq == network[p][q], qp == network[q][p], <4>_a714 , NEW CONSTANT i \in 1..Len(qp'), <3>1 , <4>1 , <5>5 PROVE FALSE File "./specifications/lamport_mutex/LamportMutex_proofs.tla", line 640, characters 7-8: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, NEW CONSTANT maxClock, NType == N \in Nat, maxClockType == maxClock \in Nat, Clock == Nat \ {0}, NEW VARIABLE clock, NEW VARIABLE req, NEW VARIABLE ack, NEW VARIABLE network, NEW VARIABLE crit, TypeOK == /\ clock \in [Proc -> Clock] /\ req \in [Proc -> [Proc -> Nat]] /\ ack \in [Proc -> SUBSET Proc] /\ network \in [Proc -> [Proc -> Seq(Message)]] /\ crit \in SUBSET Proc, Contains(s, mtype) == \E i \in 1..Len(s) : s[i].type = mtype, ClockInvInner(p, q) == LET pq == network[p][q] qp == network[q][p] IN /\ \A i \in 1..Len(pq) : pq[i].type = "req" => pq[i].clock = req[p][p] /\ Contains(qp, "ack") \/ q \in ack[p] => (/\ req[q][p] = req[p][p] /\ clock[q] > req[p][p] /\ Precedes(qp, "ack", "req") => ( \A i \in 1..Len(qp) : qp[i].type = "req" => qp[i].clock > req[p][p])) /\ p \in crit => beats(p, q), ClockInv == \A p \in Proc : \A q \in Proc \ {p} : ClockInvInner(p, q), TypeOK , BasicInv , ClockInv , [Next]_vars , NEW CONSTANT n \in Proc, NEW CONSTANT k \in Proc \ {n}, m == Head(network[k][n]), <3>1 PROVE m.clock = req[k][k] File "./specifications/lamport_mutex/LamportMutex_proofs.tla", line 1, character 1 to line 811, character 78: [ERROR]: 2/654 obligations failed. ```

One final strange one is specifications/ewd998/EWD998_proof.tla, which will ordinarily fail because it cannot find Randomization.tla. If I extract the standard modules (which include Randomization.tla) from the nightly tla2tools.jar and put them on the tlaps path with the -I flag, nearly all modules with proofs will fail. If I put Randomization.tla on the paths included with -I alone, it fails with this error:

specifications/lamport_mutex/LamportMutex_proofs.tla

``` File "./specifications/ewd998/EWD998_proof.tla", line 782, characters 9-10: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, NAssumption == N \in Nat \ {0}, NEW VARIABLE active, NEW VARIABLE color, NEW VARIABLE counter, NEW VARIABLE pending, NEW VARIABLE token, terminationDetected == /\ token.pos = 0 /\ token.color = "white" /\ token.q + counter[0] = 0 /\ color[0] = "white" /\ ~active[0], NAssumption , NodeIsNode , TypeOK , TypeOK' , Inv , Inv' , [Next]_vars , <3>2 , <3>4 PROVE /\ (token').pos = 0 /\ ~active[0] /\ pending[0] = 0 File "./specifications/ewd998/EWD998_proof.tla", line 666, characters 17-18: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, NAssumption == N \in Nat \ {0}, Node == 0..N - 1, Token == [pos : Node, q : Int, color : Color], NEW VARIABLE active, NEW VARIABLE color, NEW VARIABLE counter, NEW VARIABLE pending, NEW VARIABLE token, TypeOK == /\ active \in [Node -> BOOLEAN] /\ color \in [Node -> Color] /\ counter \in [Node -> Int] /\ pending \in [Node -> Nat] /\ token \in Token, InitiateProbe == /\ token.pos = 0 /\ \/ token.color = "black" \/ color[0] = "black" \/ counter[0] + token.q > 0 /\ token' = [pos |-> N - 1, q |-> 0, color |-> "white"] /\ color' = [color EXCEPT ! [0] = "white"] /\ UNCHANGED <>, B == Sum(pending, Node), Termination == /\ \A i \in Node : ~active[i] /\ B = 0, NAssumption , atMaster == token.pos = 0, tknWhite == token.color = "white", allWhite == \A i \in Node : color[i] = "white", P(n) == /\ Termination /\ n \in Node /\ token.pos = n /\ allWhite /\ tknWhite /\ token.q = Sum(counter, Rng(n + 1, N - 1)), Q == P(0), R(n) == BSpec => [](P(n) => <>Q), S == Termination /\ atMaster /\ allWhite, T == P(N - 1), TypeOK , S , System , <4>_a881 , <3>1 , SumEmpty PROVE T' File "./specifications/ewd998/EWD998_proof.tla", line 519, characters 7-8: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, NAssumption == N \in Nat \ {0}, Node == 0..N - 1, Token == [pos : Node, q : Int, color : Color], NEW VARIABLE active, NEW VARIABLE color, NEW VARIABLE counter, NEW VARIABLE pending, NEW VARIABLE token, TypeOK == /\ active \in [Node -> BOOLEAN] /\ color \in [Node -> Color] /\ counter \in [Node -> Int] /\ pending \in [Node -> Nat] /\ token \in Token, B == Sum(pending, Node), Termination == /\ \A i \in Node : ~active[i] /\ B = 0, Inv == /\ P0::(B = Sum(counter, Node)) /\ \/ P1::/\ \A i \in Rng(token.pos + 1, N - 1) : active[i] = FALSE /\ IF token.pos = N - 1 THEN token.q = 0 ELSE token.q = Sum(counter, Rng(token.pos + 1, N - 1)) \/ P2::(Sum(counter, Rng(0, token.pos)) + token.q > 0) \/ P3::\E i \in Rng(0, token.pos) : color[i] = "black" \/ P4::(token.color = "black"), NAssumption , TypeOK , Inv , Termination , token.pos = 0 , ~terminationDetected , <2>1 , <3>1 PROVE counter[0] + token.q = 0 File "./specifications/ewd998/EWD998_proof.tla", line 432, characters 9-10: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, NAssumption == N \in Nat \ {0}, Node == 0..N - 1, NEW VARIABLE active, NEW VARIABLE color, NEW VARIABLE counter, NEW VARIABLE pending, NEW VARIABLE token, TypeOK == /\ active \in [Node -> BOOLEAN] /\ color \in [Node -> Color] /\ counter \in [Node -> Int] /\ pending \in [Node -> Nat] /\ token \in Token, Rng(a, b) == {i \in Node : a =< i /\ i =< b}, NAssumption , TypeOK , Inv , terminationDetected , <4>1 , SumEmpty PROVE Sum(counter, Rng(0, 0)) = counter[0] File "./specifications/ewd998/EWD998_proof.tla", line 249, characters 11-12: [ERROR]: Could not prove or check: ASSUME NEW CONSTANT N, NAssumption == N \in Nat \ {0}, Token == [pos : Node, q : Int, color : Color], NEW VARIABLE active, NEW VARIABLE color, NEW VARIABLE counter, NEW VARIABLE pending, NEW VARIABLE token, TypeOK == /\ active \in [Node -> BOOLEAN] /\ color \in [Node -> Color] /\ counter \in [Node -> Int] /\ pending \in [Node -> Nat] /\ token \in Token, NAssumption , TypeOK , TypeOK' , Inv , [Next]_vars , NEW CONSTANT i \in Node \ {0}, <5>1 , <5>2 , <5>3 , <5>4 , <5>5 PROVE Sum(counter, Rng(0, token.pos))' + (token').q = Sum(counter, Rng(0, token.pos)) + token.q File "./specifications/ewd998/EWD998_proof.tla", line 1, character 1 to line 860, character 77: [ERROR]: 5/758 obligations failed. ```

You can also see these errors occurring in this CI run: https://github.com/tlaplus/Examples/actions/runs/4347799514/jobs/7595536785

ahelwer commented 1 year ago

I am also seeing strange behavior with fingerprint caching. Only some proofs seem to benefit from it; if I delete the .tlacache directory (which is output in the working directory from which I run TLAPS) then I see:

[ahelwer@node examples]$ python .github/scripts/check_proofs.py 
specifications/LoopInvariance/BinarySearch.tla
Checked proofs in 6.2s
specifications/MisraReachability/ParReachProofs.tla
Checked proofs in 1.4s
specifications/MisraReachability/ReachabilityProofs.tla
Checked proofs in 5.7s
specifications/MisraReachability/ReachableProofs.tla
Checked proofs in 5.4s
specifications/Paxos/Voting.tla
Checked proofs in 0.7s
specifications/PaxosHowToWinATuringAward/Voting.tla
Checked proofs in 0.7s
specifications/TeachingConcurrency/Simple.tla
Checked proofs in 0.2s
specifications/TeachingConcurrency/SimpleRegular.tla
Checked proofs in 5.3s
specifications/TwoPhase/TwoPhase.tla
Checked proofs in 0.2s
specifications/ewd840/EWD840_proof.tla
Checked proofs in 0.5s
specifications/ewd998/AsyncTerminationDetection_proof.tla
Checked proofs in 0.8s
specifications/ewd998/EWD998_proof.tla
Checked proofs in 0.2s

If I then run it again without deleting the fingerprints, I get:

[ahelwer@node examples]$ python .github/scripts/check_proofs.py 
specifications/LoopInvariance/BinarySearch.tla
Checked proofs in 0.7s
specifications/MisraReachability/ParReachProofs.tla
Checked proofs in 0.6s
specifications/MisraReachability/ReachabilityProofs.tla
Checked proofs in 5.7s
specifications/MisraReachability/ReachableProofs.tla
Checked proofs in 0.6s
specifications/Paxos/Voting.tla
Checked proofs in 0.7s
specifications/PaxosHowToWinATuringAward/Voting.tla
Checked proofs in 0.7s
specifications/TeachingConcurrency/Simple.tla
Checked proofs in 0.1s
specifications/TeachingConcurrency/SimpleRegular.tla
Checked proofs in 0.1s
specifications/TwoPhase/TwoPhase.tla
Checked proofs in 0.1s
specifications/ewd840/EWD840_proof.tla
Checked proofs in 0.3s
specifications/ewd998/AsyncTerminationDetection_proof.tla
Checked proofs in 0.2s
specifications/sums_even/sums_even.tla
Checked proofs in 0.1s

So for some reason specifications/MisraReachability/ReachabilityProofs.tla (and possibly Voting.tla) is not hitting the fingerprint cache and seems to be checking all proofs from scratch.

damiendoligez commented 1 year ago

I compiled and installed from a fresh checkout of 202210041448 and couldn't reproduce any of the failures you reported. Could you run tlapm --config and post the output here?

damiendoligez commented 1 year ago

OK I managed to reproduce the problem under Ubuntu.

damiendoligez commented 1 year ago

specifications/Bakery-Boulangerie/Bakery.tla

This one is easy, it's a timeout. Z3 is given 5 seconds to solve the proof obligation, but (on my machine) it takes about 11 seconds. I've submitted #73 to increase the timeout to 30 seconds.