Comments (13)
will62794
commented on August 16, 2024
1
@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.
from examples.
damiendoligez
commented on August 16, 2024
1
OK I managed to reproduce the problem under Ubuntu.
from examples.
damiendoligez
commented on August 16, 2024
1
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.
from examples.
ahelwer
commented on August 16, 2024
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
from examples.
ahelwer
commented on August 16, 2024
@will62794 that's very cool, and a neat project! Is the python script published as a module on pypi?
from examples.
muenchnerkindl
commented on August 16, 2024
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.
from examples.
will62794
commented on August 16, 2024
@helwer No, the script is not published, but feel free to extend/modify it and publish it there if you want.
from examples.
ahelwer
commented on August 16, 2024
@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?
from examples.
muenchnerkindl
commented on August 16, 2024
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.
from examples.
muenchnerkindl
commented on August 16, 2024
I believe that all proofs now work again. Thanks for uncovering these issues!
from examples.
ahelwer
commented on August 16, 2024
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
\/ <<num[self], self>>
\prec <<num[nxt[self]], nxt[self]>>
/\ unchecked'
= [unchecked EXCEPT
![self] = unchecked[self] \ {nxt[self]}]
/\ pc' = [pc EXCEPT !
[self] = "w1"]
/\ UNCHANGED <<num, flag, max, nxt>>,
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"}
/\ <<num[i], i>> \prec <<num[j], j>>
/\ 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"}
/\ <<num[i], i>> \prec <<num[j], j>>
/\ 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 <<active, counter, pending>>,
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
from examples.
ahelwer
commented on August 16, 2024
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.
from examples.
damiendoligez
commented on August 16, 2024
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?
from examples.
Related Issues (20)
- Submodules vs. copying specs into the repo HOT 2
- `ctl[p]` is never equal `"req"` in specifications/SpecifyingSystems/Liveness properties HOT 6
- GitPod & Codespaces - make sure bitrot hasn't set in
- Add TLC models for all specs for which it's viable
- Add some Apalache models HOT 5
- Bakery-Boulangerie specs don't satisfy `DeadlockFree` or `StarvationFree` liveness properties HOT 1
- Can't come up with working model for cbc_max or spanning HOT 1
- Liveness and Safety properties fail in SpanTreeRandom.tla HOT 11
- Deactivate macOS CI runners? HOT 3
- Add optional fields to manifest.json recording total and unique states for each model
- Add proof checking time to manifest details
- EWD998 model checking failure when running TLC from outside tlaplus/examples repo HOT 5
- Parameterize version of TLA+ tools used during CI run HOT 2
- Question about the specification of reliable broadcast algorithm by Bracha & Toueg (1985) HOT 8
- CI workflow fails on ubuntu HOT 7
- Do not suppress TLC output HOT 3
- Possible TLC regression on specifications/ewd998/EWD998ChanID.cfg HOT 7
- ERROR in specifications/SpecifyingSystems/Composing/CompositeFIFO.tla: In evaluation, the identifier in is either undefined or not an operator. HOT 1
- Remove deadlock flag in manifest.json in favor of `CHECK_DEADLOCK` in config file HOT 4
- Install TLA+ unicode converter into gitpod and codespaces HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from examples.