tlaplus / examples Goto Github PK
View Code? Open in Web Editor NEWA collection of TLA⁺ specifications of varying complexities
License: Other
A collection of TLA⁺ specifications of varying complexities
License: Other
# Attempted to access index 0 of tuple <<>>
'specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.cfg',
# Attempted to select nonexistent field "traces" from record
'specifications/ewd426/SimTokenRing.cfg',
# Initial error cannot find TLAPS; if fixed, cannot find property "Stable"
'specifications/ewd998/AsyncTerminationDetection_proof.cfg',
# Property is violated by the initial state
'specifications/ewd998/SmokeEWD998.cfg'
I tried both toolbox and the VScode TLC and both show the same behavior (shown below). In VScode I'm using the TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55).
In evaluation, the identifier in is either undefined or not an operator.
line 9, col 16 to line 9, col 17 of module CompositeFIFO
where line 9 is
SenderInit == (in.rdy \in BOOLEAN) /\ (in.val \in Message)
The first few lines of the "Full output" are as follows:
java -cp /home/me/.vscode-server/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar -XX:+UseParallelGC -Dtlc2.TLC.ide=vscode tlc2.TLC CompositeFIFO.tla -tool -modelcheck -coverage 1 -config CompositeFIFO.cfg -dump dot,actionlabels CompositeFIFO.dot
TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
Running breadth-first search Model-Checking with fp 122 and seed -6287525116577388646 with 1 worker on 8 cores with 3538MB heap and 64MB offheap memory [pid: 18014] (Linux 5.15.90.1-microsoft-standard-WSL2 amd64, Oracle Corporation 18.0.1.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Currently no specs included in the repository have an Apalache model. It would be nice to have some examples of this. The Einstein's Riddle spec would be an ideal first candidate, as TLC has a tough time with it. Apalache could then be added to the CI checks.
I fixed this myself by renaming some files, I don't yet have the woo to make a pull request. I have absolutely no idea what I am doing BTW, I was just trying out an example to test I had installed the TLA Toolbox correctly.
Hi, I believe the comment in the spec Bakery.tla that says "MutualExclusion asserts that two distinct processes are in their critical sections." is problematic, because no two distinct processes are allowed to be in the critical sections at the same time.
Unfinished, random math exercises collected from Specifying Systems, LearnTLA, and elsewhere.
---- MODULE F ----
EXTENDS Naturals, FiniteSets, Sequences
(* 1. Set of all permutations of {"T","L","A"} including repetitions. *)
PermsWithReps(S) ==
[ 1..Cardinality(S) -> S ]
ASSUME
PermsWithReps({"T","L","A"}) =
{<<"T", "T", "T">>, <<"T", "T", "L">>, <<"T", "T", "A">>,
<<"T", "L", "T">>, <<"T", "L", "L">>, <<"T", "L", "A">>,
<<"T", "A", "T">>, <<"T", "A", "L">>, <<"T", "A", "A">>,
<<"L", "T", "T">>, <<"L", "T", "L">>, <<"L", "T", "A">>,
<<"L", "L", "T">>, <<"L", "L", "L">>, <<"L", "L", "A">>,
<<"L", "A", "T">>, <<"L", "A", "L">>, <<"L", "A", "A">>,
<<"A", "T", "T">>, <<"A", "T", "L">>, <<"A", "T", "A">>,
<<"A", "L", "T">>, <<"A", "L", "L">>, <<"A", "L", "A">>,
<<"A", "A", "T">>, <<"A", "A", "L">>, <<"A", "A", "A">>}
(* 2. All combinations of a two-digit lock. *)
TwoDigitLock ==
[1..2 -> 0..9]
ASSUME
/\ (0..9) \X (0..9) = TwoDigitLock
/\ {<<n,m>> : n,m \in 10..19} \notin SUBSET TwoDigitLock
(* 3. All combinations of a three-digit lock. *)
ThreeDigitLock ==
[1..3 -> 0..9]
ASSUME
/\ (0..9) \X (0..9) \X (0..9) = ThreeDigitLock
/\ {<<n,m,o>> : n,m,o \in 10..19} \notin SUBSET ThreeDigitLock
(* 4. All pairs (including repetitions) of the natural numbers. *)
PairsOfNaturals ==
[1..2 -> Nat]
ASSUME
{<<n,m>> : n,m \in 0..100} \subseteq PairsOfNaturals
(* 5. All triples... *)
TriplesOfNaturals ==
[1..3 -> Nat]
ASSUME
{<<n,m,o>> : n,m,o \in 0..25} \subseteq TriplesOfNaturals
(* 6. Set of all pairs and triples... *)
PairsAndTriplesOfNaturals ==
[1..2 -> Nat] \cup [1..3 -> Nat]
ASSUME
/\ {<<n,m>> : n,m \in 0..100} \subseteq PairsAndTriplesOfNaturals
/\ {<<n,m,o>> : n,m,o \in 0..25} \subseteq PairsAndTriplesOfNaturals
(* 7. What is the Cardinality of 3. ? *)
Cardinality3 ==
Cardinality(ThreeDigitLock)
ASSUME Cardinality3 = 1000
(* 8. What is the Cardinality of 6. (PairsAndTriplesOfNaturals) ? *)
--------------------------------------------------------------
(* 9. The range/image/co-domain of a function. *)
Range(f) == { f[x]: x \in DOMAIN f }
ASSUME Range([a |-> 1, b |-> 2, c |-> 3]) = 1..3
(* 10. The permutations of a set _without_ repetition. *)
Perms(S) ==
{ f \in [S -> S] :
Range(f) = S }
ASSUME Perms({1,2,3}) =
{<<1, 2, 3>>, <<1, 3, 2>>,
<<2, 1, 3>>, <<2, 3, 1>>,
<<3, 1, 2>>, <<3, 2, 1>>}
Perms2(S) ==
\* If for all w in S there exists a v in S for which f[v]=w,
\* there can be no repetitions as a consequence. The predicate
\* demands for all elements of S to be in the range of f.
{ f \in [S -> S] :
\A w \in S :
\E v \in S : f[v]=w }
ASSUME Perms2({1,2,3}) =
{<<1, 2, 3>>, <<1, 3, 2>>,
<<2, 1, 3>>, <<2, 3, 1>>,
<<3, 1, 2>>, <<3, 2, 1>>}
Perms3(S) ==
{ f \in [S -> S] :
\A i,j \in DOMAIN f :
i # j => f[i] # f[j] }
ASSUME Perms3({1,2,3}) =
{<<1, 2, 3>>, <<1, 3, 2>>,
<<2, 1, 3>>, <<2, 3, 1>>,
<<3, 1, 2>>, <<3, 2, 1>>}
(* 11. Reverse a sequence (a function with domain 1..N). *)
Reverse(seq) ==
[ i \in 1..Len(seq) |-> seq[Len(seq)+1 - i] ]
ASSUME Reverse(<<1, 2, 3>>) = <<3, 2, 1>>
ASSUME Reverse(<<>>) = <<>>
(* 12. An (infix) operator to quickly define a function mapping an x to a y. *)
x :> y ==
[ e \in {x} |-> y ]
ASSUME "x" :> 42 = [ x |-> 42 ]
(* 13. Merge two functions f and g *)
f ++ g ==
[x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]
ASSUME <<1,2,3>> ++ [i \in 1..6 |-> i] = <<1, 2, 3, 4, 5, 6>>
(* 14. Advanced!!! Inverse of a function f (swap the domain and range). *)
Inverse(f) ==
CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s
ASSUME Inverse(("a" :> 0) ++ ("b" :> 1) ++ ("c" :> 2)) =
((0 :> "a") ++ (1 :> "b") ++ (2 :> "c"))
====
-------------------------- MODULE SyntaxExcercises --------------------------
(* The idea is that learners get the spec with the operator _definitions_ replaced
with TRUE. A learner can then check their definitions with TLC. *)
EXTENDS Integers, Sequences, TLC
(***************************************************************************)
(* The set of the fibonacci numbers: 1,1,2,3,5,8,13,... *)
(***************************************************************************)
MyNat == 1..21 \* perhaps, introduce model definitions right away?
fib[n \in MyNat] == IF n <= 2 THEN 1 ELSE fib[n-1] + fib[n-2]
ASSUME fib[12] = 144
RECURSIVE fibRecurse(_)
fibRecurse(n) == IF n <= 2 THEN 1 ELSE fibRecurse(n - 1) + fibRecurse(n - 2)
ASSUME fibRecurse(12) = 144
(***************************************************************************)
(* The set of fibonacci numbers in the range [10,20). *)
(***************************************************************************)
FibSet == { fib[n] : n \in 10..19 }
ASSUME FibSet = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}
FibSetRecurse == { fibRecurse(n) : n \in 10..19 }
ASSUME FibSetRecurse = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}
(***************************************************************************)
(* The sequence of fibonacci numbers in the range [10,20). *)
(***************************************************************************)
FibSeq == [ e \in 1..10 |-> fib[e+9] ]
ASSUME FibSeq = <<55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181>>
(***************************************************************************)
(* The range of a function func. *)
(***************************************************************************)
Range(func) == { func[e] : e \in DOMAIN func }
(* Change the 5., 10, 15. element of a function f to "abc", "def" and "ghi" *)
(* TCommit video Minute 12:30 *)
Replace(func, pos, value) == [func EXCEPT ![pos] = value ]
ASSUME [ i \in 1..3 |-> i^2 ] = Replace(Replace(Replace([i \in 1..3 |-> 0], 1, 1), 2, 4), 3, 9)
(***************************************************************************)
(* Excercise page 235/70 *)
(* The sequence obtained by removing the i-th element of seq. *)
(***************************************************************************)
Remove(seq, i) == [ j \in (1..Len(seq) - 1) |-> (IF j < i THEN seq[j] ELSE seq[j+1]) ]
(***************************************************************************)
(* Excercise page 341/91 *)
(* Recursive definition of the Len(seq) _operator_ with Tail. *)
(***************************************************************************)
RECURSIVE RecLen(_)
RecLen(seq) == IF seq = <<>> THEN 0
ELSE 1 + RecLen(Tail(seq))
(***************************************************************************)
(* An alternative variant which treats seq as the function it is and *)
(* returns the maximum of its DOMAIN which corresponds to the number of *)
(* elements in seq. *)
(***************************************************************************)
DomLen(seq) == CHOOSE m \in (DOMAIN seq): (DOMAIN seq) = 1..m
(***************************************************************************)
(* Write an operator that returns the cardinality of a given set. *)
(***************************************************************************)
RECURSIVE Card(_)
Card(S) == IF S = {} THEN 0 ELSE 1 + Card(S \ {CHOOSE e \in S : TRUE})
ASSUME Card({}) = 0 /\ Card({1,1,2,2,3,3}) = 3
(***************************************************************************)
(* Write an operator that takes a tuple/sequence and, if the tuple is *)
(* length two, returns the reversed tuple, and otherwise raises an error. *)
(***************************************************************************)
ReverseOfTwo(seq) == IF Len(seq) = 2 THEN <<seq[2], seq[1]>>
ELSE Assert(FALSE, "")
ASSUME <<4,5>> = ReverseOfTwo(<<5,4>>)
(***************************************************************************)
(* Write an operator that takes a sequence seq and, if the sequence is of *)
(* uneven length, returns the reversed sequence, otherwise return seq. *)
(***************************************************************************)
Uneven(n) == n % 2 = 1
Reverse(seq) == [ i \in 1..Len(seq) |-> seq[Len(seq) - (i-1)] ]
ReverseUneven(seq) == IF Uneven(Len(seq)) THEN Reverse(seq)
ELSE seq
ASSUME <<1,2,3,4,5>> = ReverseUneven(<<5,4,3,2,1>>)
ASSUME <<1,2,3,4>> = ReverseUneven(<<1,2,3,4>>)
(* Sum of elements in seq *)
(***************************************************************************)
(* Remove those elements from sequence seq for which Filter(_) holds. *)
(***************************************************************************)
RECURSIVE Subseq(_,_)
Subseq(Filter(_), seq) == IF seq = <<>>
THEN <<>>
ELSE IF Filter(Head(seq))
THEN <<Head(seq)>> \o Subseq(Filter, Tail(seq))
ELSE Subseq(Filter, Tail(seq))
Even(n) == ~Uneven(n)
ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = <<2,6,8,8,42>>
SelectSeq2(Test(_), s) ==
LET S[i \in 0..Len(s)] ==
IF i = 0 THEN << >> \* As a basis set the s[0] = <<>>
ELSE IF Test(s[i]) THEN S[i-1] \o <<s[i]>> \* copy previous value and concat with s[i]
ELSE S[i-1] \* just copy the previous value
IN S[Len(s)] \* The maximum (last function position) contains the collected sequence
ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = SelectSeq2(Even, <<1,2,1,3,3,6,8,8,23,42>>)
(***************************************************************************)
(* Given DOMAIN Tuple is the set of numbers Tuple is defined over, write *)
(* an operator that gives a set of the values of the Tuple, ie the range. *)
(***************************************************************************)
(***************************************************************************)
(* Write an operator that takes two sets S1 and S2 and determines if the *)
(* double of every element in S1 is an element of S2. *)
(***************************************************************************)
(***************************************************************************)
(* Given a sequence of sets, write an operator that determines if a given *)
(* element is found in any of the sequence’s sets. *)
(* IE Op("a", <<{"b", "c"}, {"a", "c"}>>) = TRUE. *)
(***************************************************************************)
(* Given the (built-in) set Nat (Naturals), create a subset of S whose largest element is 42. *)
(* Hint: Override Nat with 1..1000 on the Advanced Options page of the Model editor. By default *)
(* Nat is represented as a UserValue in TLC. A UserValue is _not_ enumerable, whereas a 1..1000 *)
(* is represented as a (finite) IntervalValue which subsequently can be enumerated. *)
Subset42 == { i \in Nat: i < 43 }
\*ASSUME Subset42 = 1..42
(* The inverse of a function *)
Inverse(f) ==
CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s
ASSUME Inverse("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) = (0 :> "a" @@ 1 :> "b" @@ 2 :> "c")
(* Merge two functions f and g *)
Merge(f, g) ==
[x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]
ASSUME Merge(<<1,2,3>>, [i \in 1..6 |-> i]) = <<1, 2, 3, 4, 5, 6>>
(* The permutations of a set *)
Perms(S) ==
{f \in [S -> S] : \A w \in S : \E v \in S : f[v]=w}
ASSUME Perms({1,2,3}) = {<<1, 2, 3>>, <<1, 3, 2>>, <<2, 1, 3>>, <<2, 3, 1>>, <<3, 1, 2>>, <<3, 2, 1>>}
=============================================================================
Graphs
With the definitions from the Graphs module, under what conditions
is <<p>>
an element of Path(G)
?
Find the following values, and use TLC to check your answers.
(See the file PrintValues.tla in the folder AsynchronousMemory.)
[i \in Nat |-> i^2][42]
LET f == [i \in Nat |-> i^2]
IN [f EXCEPT ![42] = 24][42]
LET f == [i \in Nat |-> i^2]
IN [f EXCEPT ![42] = @ - 24, ![24] = 42][42]
LET f[i \in Nat] == IF i = 0 THEN 0 ELSE f[i-1] + i
IN f[42]
[i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
ELSE 42].a
[i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
ELSE 42].bc
[a |-> 17, bc |-> 42, d |-> 42]["a"]
[a |-> 17, bc |-> 42, d |-> 42]["bc"]
DOMAIN [a |-> 17, bc |-> 42, d |-> 42]
LET f(a) == [i \in Nat |-> a^i]
g == [j \in Nat |-> f(j)]
IN g[2][3]
LET f(a) == [i \in Nat |-> a^i]
g == [j \in Nat |-> f(j)]
IN g[2][3]
[i \in Nat, j \in 1..10 |-> i*j][3,4]
Define an operator AF such that, if r is a record, then:
if r has a "count" field, then AF(r) is r with the count
field incremented by 1, otherwise, AF(r) is obtained from
r by adding a "count" field with value 0.
Define an operator Reverse, so if s is any sequence, then
Reverse(s) is sequence s in reverse order. (Hint: you
don't have to use recursion.) Test it with
TLC. (Don't forget to check that it works on the empty
sequence, << >>
.)
Define a function Sum
whose domain is Seq(Nat)
such
that Sum(s)
is the sum of the elements of s
. (Let
Sum(<< >>)
equal 0
.)
Determine which of the following formulas are tautologies.
(F => G) /\ (G => F) <=> (F <=> G)
(~F /\ ~G) <=> (~F) \/ (~G)
F => (F => G)
(F => G) <=> (~G => ~F)
(F => (G => H)) => ((F => G) => H)
(F <=> (G <=> H)) => ((F <=> G) <=> H)
(\A x : F /\ G) <=> (\A x : F) /\ (\A x : G)
(\E x : F /\ G) <=> (\E x : F) /\ (\E x : G)
(\A x : F \/ G) <=> (\A x : F) \/ (\A x : G)
(\E x : F \/ G) <=> (\E x : F) \/ (\E x : G)
(S \subseteq T) <=> (S \cup T = T)
(S \subseteq T) <=> \A x \in S : x \in T
(S = T) <=> (S \subseteq T) /\ (T \subseteq S)
(S \subseteq T) <=> (S \ T = {})
(S \ T) \cup (T \ S) = (S \cup T) \ (S \cap T)
(S \ (T \cap U)) = (S \ T) \cup (S \ U)
(a) <>[]<>F <=> []<>F
(b) []<>[]F <=> []<>F
(c) ~[](F \/ G) => <>~F /\ <>~G
(d) []([]F => G) => ([]F => []G)
(e) [](F => []G) => ([]F => []G)
(f) [][A /\ B]_v <=> [][A]_v /\ [][B]_v
(g) []<><<A /\ B>>_v <=> []<><<A>>_v /\ []<><<B>>_v
(h) [][A => B]_v <=> [][<<A>>_v => B]_v
(i) WF_v(A) /\ WF_v(B) => WF_v(A \/ B)
(j) SF_v(A) /\ SF_v(B) => SF_v(A \/ B)
(k) ENABLED (A /\ B) => (ENABLED A) /\ (ENABLED B)
(a) Use TLC to print all Pythagorean triples <<i,j,k>>
with
i^2 + j^2 = k^2
for natural numbers i,j,k \leq N.
Start with N=20. (Don't be clever and use the formula for
generating Pythagorean triples; have TLC to it in a straightforward
fashion.)
(b) Next, get TLC to print only essentially Pythagorean triples--that
is, Pythagorean triples <<i, j, k>>
such that i \leq j and i,j, and k
have no common factor. Try it with N = 50, 100, ... . Why does TLC
take longer to generate each example as N increases?
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/SimpleMath/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/AdvancedExamples/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/TLC/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/HourClock/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/Liveness/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/FIFO/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/CachingMemory/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/RealTime/README
@lemmy in an earlier issue you mentioned it would be useful to parameterize the version of the TLA+ tools used during the CI run, so you could for example trigger a build of the tlaplus/tlaplus repo and have the resulting binary be used during a CI run for the tlaplus/examples repo. Are you still interested in this feature? Will look into implementing it if so.
I've been defining models as part of work on #107. Currently these properties fail so these specs can only be subject to safety checking. Some fairness assumptions are required for the properties to be satisfied. @muenchnerkindl any idea what those fairness assumptions would be? The one in Spec
is insufficient.
From here: #61 (comment)
ewd998, which runs into a naming collision between the TLAPS and community modules. Specifically Functions.tla; it tries to use operators in the Community version of Functions.tla, while also importing various modules from the TLAPS standard library (which itself includes a Functions.tla that doesn't have those operators).
I confirm that the name clash between the TLAPS standard theorem library and some of the Community Modules (in particular Functions) is known and should be fixed in the long overdue release of TLAPS.
After merging a bug fix for one of the examples (aba-asyn-byz), the CI run succeeded for Windows and Mac OS but failed for Ubuntu due to an error in generating the Isabelle object logic heap. Why is this happening? Also, the updated example doesn't contain any proofs so the problem is clearly unrelated to the fix.
@ahelwer, could you please have a look?
@ahelwer Diagnosing CI failures becomes much easier when you have TLC's output included. I'm wondering, is there a particular reason why TLC's stdout/stderr is currently being suppressed?
Spec below needs polish to become an example.
------------------------------- MODULE TLCMC -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, TestGraphs
(***************************************************************************)
(* Converts the given Sequence seq into a Set of all the *)
(* Sequence's elements. In other words, the image of the function *)
(* that seq is. *)
(***************************************************************************)
SeqToSet(seq) == {seq[i] : i \in 1..Len(seq)}
(***************************************************************************)
(* Returns a Set of those permutations created out of the elements of Set *)
(* set which satisfies Filter. *)
(***************************************************************************)
SetToSeqs(set, Filter(_)) == UNION {{perm \in [1..Cardinality(set) -> set]:
\* A filter applied on each permutation
\* generated by [S -> T]
Filter(perm)}}
(***************************************************************************)
(* Returns a Set of all possible permutations with distinct elements *)
(* created out of the elements of Set set. All elements of set occur in *)
(* in the sequence. *)
(***************************************************************************)
SetToDistSeqs(set) == SetToSeqs(set,
LAMBDA p: Cardinality(SeqToSet(p)) = Cardinality(set))
(***************************************************************************)
(* A (state) graph G is a directed cyclic graph. *)
(* *)
(* A graph G is represented by a record with 'states' and 'actions' *)
(* components, where G.states is the set of states and G.actions[s] is the *)
(* set of transitions of s -- that is, all states t such that there is an *)
(* action (arc) from s to t. *)
(***************************************************************************)
IsGraph(G) == /\ {"states", "initials", "actions"} = DOMAIN G
/\ G.actions \in [G.states -> SUBSET G.states]
/\ G.initials \subseteq G.states
(***************************************************************************)
(* A set of all permutations of the initial states of G. *)
(***************************************************************************)
SetOfAllPermutationsOfInitials(G) == SetToDistSeqs(G.initials)
(***************************************************************************)
(* A Set of successor states state. *)
(***************************************************************************)
SuccessorsOf(state, SG) == {successor \in SG.actions[state]:
successor \notin {state}}
(***************************************************************************)
(* The predecessor of v in a forest t is the first element of the pair *)
(* <<predecessor, successor>> nested in a sequence of pairs. In an actual *)
(* implementation such as TLC, pair[1] is rather an index into t than *)
(* an id of an actual state. *)
(***************************************************************************)
Predecessor(t, v) == SelectSeq(t, LAMBDA pair: pair[2] = v)[1][1]
CONSTANT StateGraph, ViolationStates, null
ASSUME \* The given StateGraph is actually a graph
\/ IsGraph(StateGraph)
\* The violating states are vertices in the state graph.
\/ ViolationStates \subseteq StateGraph.states
(***************************************************************************
The PlusCal code of the model checker algorithm
--fair algorithm ModelChecker {
variables
\* A FIFO containing all unexplored states. A simple
\* set provides no order, but TLC should explore the
\* StateGraph in either BFS (or DFS => LIFO).
\* Note that S is initialized with each
\* possible permutation of the initial states
\* here because there is no defined order
\* of initial states.
S \in SetOfAllPermutationsOfInitials(StateGraph),
\* A set of already explored states.
C = {},
\* The state currently being explored in scsr
state = null,
\* The set of state's successor states
successors = {},
\* Counter
i = 1,
\* A path from some initial state ending in a
\* state in violation.
counterexample = <<>>,
\* A sequence of pairs such that a pair is a
\* sequence <<predecessor, successors>>.
T = <<>>;
{
(* Check initial states for violations. We could
be clever and check the inital states as part
of the second while loop. However, we then
either check all states twice or add unchecked
states to S. *)
init: while (i \leq Len(S)) {
\* Bug in thesis:
\*state := Head(S);
state := S[i];
\* state is now fully explored,
\* thus exclude it from any
\* futher exploration if graph
\* exploration visits it again
\* due to a cycle.
C := C \cup {state};
i := i + 1;
if (state \in ViolationStates) {
counterexample := <<state>>;
\* Terminate model checking
goto trc;
};
};
\* Assert that all initial states have been explored.
initPost: assert C = SeqToSet(S);
(* Explores all successor states
until no new successors are found
or a violation has been detected. *)
scsr: while (Len(S) # 0) {
\* Assign the first element of
\* S to state. state is
\* what is currently being checked.
state := Head(S);
\* Remove state from S.
S := Tail(S);
\* For each unexplored successor 'succ' do:
successors := SuccessorsOf(state, StateGraph) \ C;
if (SuccessorsOf(state, StateGraph) = {}) {
\* Iff there exists no successor besides
\* the self-loop, the system has reached
\* a deadlock state.
counterexample := <<state>>;
goto trc;
};
each: while (successors # {}) {
with (succ \in successors) {
\* Exclude succ in this while loop.
successors := successors \ {succ};
\* Mark successor globally visited.
C := C \cup {succ}; S := S \o <<succ>>;
\* Append succ to T and add it
\* to the list of unexplored states.
T := T \o << <<state,succ>> >>;
\* Check state for violation of a
\* safety property (simplified
\* to a check of set membership.
if (succ \in ViolationStates) {
counterexample := <<succ>>;
\* Terminate model checking
goto trc;
};
};
};
};
(* Model Checking terminated without finding
a violation. *)
\* No states left unexplored and no ViolationState given.
assert S = <<>> /\ ViolationStates = {};
goto Done;
(* Create a counterexample, that is a path
from some initial state to a state in
ViolationStates. In the Java implementation
of TLC, the path is a path of fingerprints.
Thus, a second, guided state exploration
resolves fingerprints to actual states. *)
trc : while (TRUE) {
if (Head(counterexample) \notin StateGraph.initials) {
counterexample := <<Predecessor(T, Head(counterexample))>> \o counterexample;
} else {
assert counterexample # <<>>;
goto Done;
};
};
}
}
***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES S, C, state, successors, i, counterexample, T, pc
vars == << S, C, state, successors, i, counterexample, T, pc >>
Init == (* Global variables *)
/\ S \in SetOfAllPermutationsOfInitials(StateGraph)
/\ C = {}
/\ state = null
/\ successors = {}
/\ i = 1
/\ counterexample = <<>>
/\ T = <<>>
/\ pc = "init"
init == /\ pc = "init"
/\ IF i \leq Len(S)
THEN /\ state' = S[i]
/\ C' = (C \cup {state'})
/\ i' = i + 1
/\ IF state' \in ViolationStates
THEN /\ counterexample' = <<state'>>
/\ pc' = "trc"
ELSE /\ pc' = "init"
/\ UNCHANGED counterexample
ELSE /\ pc' = "initPost"
/\ UNCHANGED << C, state, i, counterexample >>
/\ UNCHANGED << S, successors, T >>
initPost == /\ pc = "initPost"
/\ Assert(C = SeqToSet(S),
"Failure of assertion at line 116, column 18.")
/\ pc' = "scsr"
/\ UNCHANGED << S, C, state, successors, i, counterexample, T >>
scsr == /\ pc = "scsr"
/\ IF Len(S) # 0
THEN /\ state' = Head(S)
/\ S' = Tail(S)
/\ successors' = SuccessorsOf(state', StateGraph) \ C
/\ IF SuccessorsOf(state', StateGraph) = {}
THEN /\ counterexample' = <<state'>>
/\ pc' = "trc"
ELSE /\ pc' = "each"
/\ UNCHANGED counterexample
ELSE /\ Assert(S = <<>> /\ ViolationStates = {},
"Failure of assertion at line 164, column 8.")
/\ pc' = "Done"
/\ UNCHANGED << S, state, successors, counterexample >>
/\ UNCHANGED << C, i, T >>
each == /\ pc = "each"
/\ IF successors # {}
THEN /\ \E succ \in successors:
/\ successors' = successors \ {succ}
/\ C' = (C \cup {succ})
/\ S' = S \o <<succ>>
/\ T' = T \o << <<state,succ>> >>
/\ IF succ \in ViolationStates
THEN /\ counterexample' = <<succ>>
/\ pc' = "trc"
ELSE /\ pc' = "each"
/\ UNCHANGED counterexample
ELSE /\ pc' = "scsr"
/\ UNCHANGED << S, C, successors, counterexample, T >>
/\ UNCHANGED << state, i >>
trc == /\ pc = "trc"
/\ IF Head(counterexample) \notin StateGraph.initials
THEN /\ counterexample' = <<Predecessor(T, Head(counterexample))>> \o counterexample
/\ pc' = "trc"
ELSE /\ Assert(counterexample # <<>>,
"Failure of assertion at line 177, column 20.")
/\ pc' = "Done"
/\ UNCHANGED counterexample
/\ UNCHANGED << S, C, state, successors, i, T >>
Next == init \/ initPost \/ scsr \/ each \/ trc
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
Termination == <>(pc = "Done")
\* END TRANSLATION
Live == ViolationStates # {} => <>[](/\ Len(counterexample) > 0
/\ counterexample[Len(counterexample)] \in ViolationStates
/\ counterexample[1] \in StateGraph.initials)
=============================================================================
----------------------------- MODULE TestGraphs -----------------------------
EXTENDS Sequences, Integers
(***************************************************************************)
(* The definitions of some graphs, paths, etc. used for testing the *)
(* definitions and the algorithm with the TLC model checker. *)
(***************************************************************************)
\* Graph 1.
G1 == [states |-> 1..4,
initials |-> {1,2},
actions |-> << {1,2}, {1,3}, {4}, {3} >>
]
V1 == {4}
\* Graph 1a.
G1a == [states |-> 1..4,
initials |-> {3},
actions |-> << {1, 2}, {1, 3}, {4}, {3} >>]
\* Graph-wise it's impossible to reach state 1 from state 3
V1a == {1}
\* Graph 2. This graph is actually a forest of two graphs
\* {1,2} /\ {3,4,5}. {1,2} are an SCC.
G2 == [states |-> 1..5,
initials |-> {1,3},
actions |-> << {1, 2}, {1}, {4, 5}, {}, {} >> ]
V2 == {2,5}
\* Graph 3.
G3 == [states |-> 1..4,
initials |-> {2},
actions |-> << {1,2}, {2,3}, {3,4}, {1,4} >> ]
V3 == {1}
\* Graph 4.
G4 == [states |-> 1..9,
initials |-> {1,2,3},
actions |-> << {3}, {4}, {5}, {6}, {7}, {7}, {8, 9}, {}, {4} >> ]
V4 == {8}
\* Graph 5.
G5 == [states |-> 1..9,
initials |-> {9},
actions |-> << {4,2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {2} >> ]
V5 == {8}
\* Graph 6.
G6 == [states |-> 1..5,
initials |-> {5},
actions |-> << {2,4,5}, {2}, {1}, {4}, {3} >> ]
V6 == {2}
\* Graph Medium (node 22 is a sink)
G7 == [states |-> 1..50,
initials |-> {1},
actions |-> << {8,35},{15,46,22,23,50},{20,26,34},{5,18,28,37,43},{18,28},{44},{14,29},{42,45},{20,49},{10,12,31,47},
{1,8,29,30,35,42},{22,31},{10,12,22,27},{23,24,48},{9,22,49},{9,35,50},{10},{21,25,39},{7,29,33,43},{16,41},{},
{4,36,39,47},{7},{12,22,23},{5,6,39,44},{3,35},{10,13,17},{6,25,33,32,43},{23,30,40,45},{23,50},{24,38},
{19,33},{6,7,14,38,48},{3,9,20},{3,20,41},{10,38,47},{21,43},{6,10,36,48},{36,38,39},{19,43},{16},
{29,45},{32},{38,39},{40},{9,15,16,50},{17},{24,31},{13,22,34},{35,23,50} >> ]
V7 == {50}
\* Graph 8.
G8 == [states |-> 1..4,
initials |-> {1},
actions |-> <<{1,2},{2,3},{3,4},{4}>>]
V8 == {}
\* Graph 9.
G9 == [states |-> {1},
initials |-> {1},
actions |-> <<{1}>>]
V9 == {1}
\* Graph 10.
G10 == [states |-> {},
initials |-> {},
actions |-> <<{}>>]
V10 == {}
\* Graph 11.
G11 == [states |-> 1..10,
initials |-> {},
actions |-> <<{}>>]
V11 == {}
\* Graph 12.
G12 == [states |-> 1..3,
initials |-> {1,2,3},
actions |-> <<{},{},{}>>]
V12 == {1}
\* Graph 13 (simple sequence.
G13 == [states |-> 1..3,
initials |-> {1},
actions |-> <<{2},{3},{}>>]
V13 == {}
=============================================================================
My case to share is about the TLA+ Spec of Software Defined Perimeter (SDP) architecture and algorithm based on the open source project fwknop.
https://github.com/10227694/SDP_Verification
The subdirectory SDP_Attack_Spec contains the specification based on the following materials:
(* https://cloudsecurityalliance.org/artifacts/software-defined-perimeter-zero-trust-specification-v2/ )
( http://www.cipherdyne.org/fwknop/ *)
The subdirectory SDP_Attack_New_Solution_Spec contains the specification for the improved SDP architecture and algorithm which fixed the discovered vulnerability.
The slide "Specifying and Verifying SDP Protocol Based Zero Trust Architecture Using TLA+.pptx" contains the key description of the reserach work.
For detail descriptions, please refer to:
I'm confused about some of the choices made when the specification for this algorithm was encoded in TLA+. If I'm understanding things correctly, sendEcho()
method for example seems to be prioritizing hosts that "start" in the v1
location, as if 1
is always the value proposed by the transmitter. In the original paper, before the algorithm even starts, the transmitter (which is effectively the leader) is supposed to send out initial messages. In your TLA+ spec, these messages don't even exist. Why is this the case, and how do I convince myself that this simplification, or rewrite, is still safe and equivalent to the original algorithm?
My other concern is about the Byzantine processes. My intuition about this bit of your specification is that their behavior is "abstracted away", and that all the progress that the non-faulty hosts in the protocol are making is due to correct messages being sent and received. Although this makes sense to me on a high level, I'm still not seeing why the TLA+ spec is not encoding in some way the ability of faulty processes to send, for example, echo messages with differing values.
Here's an example entry in the manifest.json:
{
"specifications": [
{
"title": "Multi-Car Elevator System",
"description": "A simple multi-car elevator system servicing a multi-floor building",
"source": "https://groups.google.com/g/tlaplus/c/5Xd8kv288jE/m/IrliJIatBwAJ",
"authors": ["Andrew Helwer"],
"modules": [
{
"path": "specifications/MultiCarElevator/Elevator.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": [
{
"path": "specifications/MultiCarElevator/ElevatorLivenessSmall.cfg",
"runtime": "00:00:10",
"features": ["liveness"],
"result": "success"
},
So you have a specification (directory), with one or more modules (.tla files), where each module can have 0 or more models (.cfg files). Similar to the toolbox! I envision a number of interesting pieces of metadata associated with each of these entities that can be searched or filtered by a program consuming this repo:
I will write a CI script that runs to validate the following when a PR is open:
I agree it would not be useful to have this information duplicated in a manifest and a README, which could get out of sync. I will look into whether it's possible to pull this info into an HTML file and have it displayed or something of that sort. It does look like this work would resolve that issue you linked.
Originally posted by @ahelwer in #55 (comment)
https://github.com/tlaplus-community/tlauc should be installed as part of https://github.com/tlaplus/Examples/blob/master/.devcontainer/install.sh.
/cc @ahelwer
This is either a regression or actually a bug that was fixed - on nightly, running the specifications/ewd998/EWD998ChanID.cfg model (with -deadlock
flag) has TLC return the value success. But on an older version of nightly (downloaded probably a few months ago? I overwrote it sadly, didn't think to set it aside) it returns a liveness failure.
4686a0b adds rudimentary support for Github Codespaces.
TODOs:
## Waiting for a stable URL.
apt-get install libz3-java libz3-jni libz3-dev libz3-4
mkdir apalache && cd apalache
wget https://github.com/informalsystems/apalache/releases/latest/download/apalache-v0.15.1.tgz
tar xvfz apalache-v0.15.1.tgz
https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
I'm adding basic TLC models to a bunch of specs for #107 and ran into trouble with this spec, could you help? Tagging authors @konnov @josef-widder @banhday
I'm attempting to use this model:
CONSTANTS
N = 4
T = 1
F = 1
Values = {1, 2}
Bottom = 0
INVARIANTS TypeOK Validity Agreement
PROPERTIES Termination RealTermination
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
but I get this runtime error (subtract 2 from line numbers to get the current spec, I added a couple assumptions about the constant values in my branch):
TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 16 and seed -7656258344444481100 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [p
id: 136262] (Linux 6.6.10-arch1-1 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/cbc_max/cbc_max.tla
Parsing file /tmp/tlc-11021836222741093434/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-11021836222741093434/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla
)
Parsing file /tmp/tlc-11021836222741093434/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-11021836222741093434/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-11021836222741093434/Sequences.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module cbc_max
Starting... (2024-01-23 15:05:58)
Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Finished computing initial states: 81 distinct states generated at 2024-01-23 15:05:58.
Progress(5) at 2024-01-23 15:06:01: 52,442 states generated (52,442 s/min), 27,509 distinct states found (27,509 ds/min), 21,333 states left on queue.
Progress(7) at 2024-01-23 15:07:01: 2,164,207 states generated (2,111,765 s/min), 807,360 distinct states found (779,851 ds/min), 578,295 states left on q
ueue.
Progress(8) at 2024-01-23 15:08:01: 4,337,333 states generated (2,173,126 s/min), 1,525,842 distinct states found (718,482 ds/min), 1,074,077 states left
on queue.
Progress(8) at 2024-01-23 15:09:01: 6,493,247 states generated (2,155,914 s/min), 2,219,299 distinct states found (693,457 ds/min), 1,548,647 states left
on queue.
Progress(8) at 2024-01-23 15:10:01: 8,615,301 states generated (2,122,054 s/min), 2,904,446 distinct states found (685,147 ds/min), 2,017,726 states left
on queue.
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to compute the value of an expression of form
CHOOSE x \in S: P, but no element of S satisfied P.
line 44, col 13 to line 45, col 75 of module cbc_max
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ sntMsgs = {}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"BCAST1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {}, {}, {}>>
State 2: <BcastPhs1(1) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = {[type |-> "Phs1", value |-> 1, sndr |-> 1]}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {}, {}, {}>>
State 3: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = {[type |-> "Phs1", value |-> 1, sndr |-> 1]}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {[type |-> "Phs1", value |-> 1, sndr |-> 1]}, {}, {}>>
State 4: <BcastPhs1(3) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {[type |-> "Phs1", value |-> 1, sndr |-> 1]}, {}, {}>>
State 5: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
{ [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 3, sndr |-> 3] },
{},
{} >>
State 6: <BcastPhs1(4) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 2, sndr |-> 4],
[type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
{ [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 3, sndr |-> 3] },
{},
{} >>
State 7: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 2, sndr |-> 4],
[type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
{ [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 2, sndr |-> 4],
[type |-> "Phs1", value |-> 3, sndr |-> 3] },
{},
{} >>
State 8: <BcastPhs1(2) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 1, sndr |-> 2],
[type |-> "Phs1", value |-> 2, sndr |-> 4],
[type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "PHS1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
{ [type |-> "Phs1", value |-> 1, sndr |-> 1],
[type |-> "Phs1", value |-> 2, sndr |-> 4],
[type |-> "Phs1", value |-> 3, sndr |-> 3] },
{},
{} >>
Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 93, column 3 to line 97, column 58 in cbc_max
1. Line 93, column 6 to line 93, column 19 in cbc_max
2. Line 94, column 6 to line 94, column 40 in cbc_max
3. Line 95, column 6 to line 95, column 65 in cbc_max
4. Line 96, column 6 to line 96, column 39 in cbc_max
5. Line 96, column 11 to line 96, column 39 in cbc_max
6. Line 96, column 29 to line 96, column 37 in cbc_max
7. Line 44, column 13 to line 45, column 75 in cbc_max
9696693 states generated, 3251762 distinct states found, 2254468 states left on queue.
The depth of the complete state graph search is 9.
Finished in 04min 34s at (2024-01-23 15:10:33)
Recently learned about CHECK_DEADLOCK
being an option in model files. Currently whether to check deadlock for each model is defined in the manifest.json, for example:
{
"path": "specifications/Huang/Huang.cfg",
"runtime": "00:00:40",
"size": "medium",
"mode": "exhaustive search",
"config": [
"ignore deadlock"
],
"features": [
"alias",
"liveness",
"state constraint"
],
"result": "success"
}
which the Python script reads then passes on to the TLC command line flags. I think it would be better to remove this config item in favor of CHECK_DEADLOCK
in the model file.
Steps to reproduce:
./examples/.github/scripts/linux-setup.sh examples/.github/scripts examples/deps true
to install dependencies on Linux & macOSjava -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -XX:+UseParallelGC -cp examples/deps/tools/tla2tools.jar:examples/deps/community/modules.jar:examples/deps/tlapm/library tlc2.TLC examples/specifications/ewd998/EWD998ChanTrace.tla -config examples/specifications/ewd998/EWD998ChanTrace.cfg -workers auto -lncheck final -cleanup
Observe the following error:
TLC2 Version 2.18 of Day Month 20?? (rev: 23f7650)
Running breadth-first search Model-Checking with fp 125 and seed 7822221676660054780 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [pid: 34002] (Linux 6.8.2-arch2-1 amd64, N/A 22 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998ChanTrace.tla
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998Chan.tla
Parsing file /tmp/tlc-16960620422673853593/Json.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Json.tla)
Parsing file /tmp/tlc-16960620422673853593/TLC.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-16960620422673853593/IOUtils.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/IOUtils.tla)
Parsing file /tmp/tlc-16960620422673853593/VectorClocks.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/VectorClocks.tla)
Parsing file /tmp/tlc-16960620422673853593/_TLCTrace.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-16960620422673853593/Integers.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-16960620422673853593/Sequences.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-16960620422673853593/FiniteSets.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/Utils.tla
Parsing file /tmp/tlc-16960620422673853593/Naturals.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-16960620422673853593/Functions.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/Functions.tla)
Parsing file /tmp/tlc-16960620422673853593/SequencesExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/SequencesExt.tla)
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998.tla
Parsing file /tmp/tlc-16960620422673853593/Randomization.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Randomization.tla)
Parsing file /tmp/tlc-16960620422673853593/Folds.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/Folds.tla)
Parsing file /tmp/tlc-16960620422673853593/FiniteSetsExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/FiniteSetsExt.tla)
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/AsyncTerminationDetection.tla
Parsing file /tmp/tlc-16960620422673853593/TLCExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module Utils
Semantic processing of module Randomization
Semantic processing of module AsyncTerminationDetection
Semantic processing of module EWD998
Semantic processing of module EWD998Chan
Semantic processing of module Json
Semantic processing of module IOUtils
Semantic processing of module VectorClocks
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module EWD998ChanTrace
Starting... (2024-04-07 09:56:50)
Error: The configuration file substitutes constant N with non-constant TraceN - specifically: Attempted to apply the operator overridden by the Java method
public static tlc2.value.IValue tlc2.overrides.Json.ndDeserialize(tlc2.value.impl.StringValue) throws java.io.IOException,
but it produced the following error:
specifications/ewd998/EWD998ChanTrace.ndjson (No such file or directory)
Finished in 00s at (2024-04-07 09:56:50)
Found during execution of CI in tlaplus/tlaplus repo. It seems like a path is hardcoded somewhere assuming cwd is repo root.
As discussed on twitter.
As possibly encountered in #104, some bitrot could have set in for the gitpod and codespaces. This issue exists as a reminder to check that these still work.
This isn't work I'm planning to do anytime soon but it would be a nice little project if someone else wants to take it on. Markdown is a very difficult language to work with, tooling-wise, but there are nice full-featured parsers like goldmark (used by the Hugo static site generator, for example) which make it tractable. A CI script could parse the README.md file with goldmark, find the table & its entries, and check its correspondence to the manifest.json file. This would include not only the existence of specs in the table but also whether they are properly labeled as including proofs, pluscal, TLC models, and whatever other traits we care to define. This could also implement whatever clustering & categorization is desired in #15. This could all possibly be implemented as a goldmark extension. Alternatively, there are a number of python markdown parsers of varying quality levels that could be used.
The README table validation work reveals that a bit more than half the specs in this repo have a TLC model associated with them. Adding TLC models to the remainder (if viable) would be an easy way to have improved confidence that the specs in this repo are actually correct (in the sense of capable of being validated, not exhibiting simple type errors, etc.) and would expand the functional test suite for the TLA+ tools.
I've been using the example of concurrently incrementing a shared variable for demonstrating TLA+.
Since this can be split up into t = i
, and i = t + 1
actions, it demonstrates many of the interesting facets of TLA+ model checking while being a tiny example:
In specifications/SpanningTree/SpanTreeRandom.tla
, the model uses RandomElement
to generate a list of edges between nodes. This causes the properties Liveness
and Safety
to occasionally fail. Whether this is because of a flaw in the algorithm or by design is uncertain. Here is a model reproducing the failure:
CONSTANTS
Nodes = {n1, n2, n3, n4, n5, n6}
MaxCardinality = 6
Root = n1
INVARIANT TypeOK
PROPERTIES Liveness Safety
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
Here is a failure trace:
tlc SpanTreeRandom
TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 116 and seed 2350910532224203137 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [p
id: 187405] (Linux 6.6.10-arch1-1 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/SpanningTree/SpanTreeRandom.tla
Parsing file /tmp/tlc-9076410093698049487/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-9076410093698049487/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-9076410093698049487/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-9076410093698049487/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-9076410093698049487/Sequences.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module SpanTreeRandom
Starting... (2024-01-26 08:12:58)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-01-26 08:12:58.
Error: Invariant Safety is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ mom = (n1 :> n1 @@ n2 :> n2 @@ n3 :> n3 @@ n4 :> n4 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 6 @@ n3 :> 6 @@ n4 :> 6 @@ n5 :> 6 @@ n6 :> 6)
State 2: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n3 @@ n4 :> n4 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 6 @@ n5 :> 6 @@ n6 :> 6)
State 3: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n3 @@ n4 :> n2 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 2 @@ n5 :> 6 @@ n6 :> 6)
State 4: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n3 @@ n4 :> n2 @@ n5 :> n1 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 2 @@ n5 :> 1 @@ n6 :> 6)
State 5: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n5 @@ n4 :> n2 @@ n5 :> n1 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 2 @@ n5 :> 1 @@ n6 :> 6)
State 6: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n5 @@ n4 :> n2 @@ n5 :> n1 @@ n6 :> n2)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 2 @@ n4 :> 2 @@ n5 :> 1 @@ n6 :> 2)
21742 states generated, 4063 distinct states found, 2041 states left on queue.
The depth of the complete state graph search is 6.
Finished in 01s at (2024-01-26 08:12:59)
This came out of the work in #110.
(see personal email "RE: Github examples" dated 07/17/19 from LL)
And more explicit variant of how to specify logical and. It is broken when Len(by) # Len(bx)
LOCAL INSTANCE Sequences
LOCAL Max(n, m) == IF n < m THEN m ELSE n
RECURSIVE ToBase2(_, _)
ToBase2(d, b) == IF d > 0
THEN ToBase2(d \div 2, b) \o <<d % 2>>
ELSE b
ToBase10(b) == LET d[i \in DOMAIN b] == IF i = 1
THEN b[Len(b) + 1 - i] * (2^(i-1))
ELSE b[Len(b) + 1 - i] * (2^(i-1)) + d[i - 1]
IN d[Len(b)]
LOCAL And2(x,y) == LET bx == ToBase2(x, <<>>)
by == ToBase2(y, <<>>)
and == [ i \in DOMAIN bx \cup DOMAIN by |->
IF bx[i] = 1 /\ by[i] = 1 THEN 1 ELSE 0 ]
IN ToBase10(and)
@konnov @josef-widder Are the liveness properties Unforg_Ltl
and Corr_Ltl
supposed to only hold if all processes start in V0
or V1
, respectively? Should the properties be box-quantified?
Examples/specifications/aba-asyn-byz/aba_asyn_byz.tla
Lines 147 to 152 in 8cef3cf
The check_small_models.py script will then validate that TLC execution produces the expected values. This will significantly improve the value of these models as TLC regression tests, since this number should not ever change unless the spec or model changes.
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.
There are typos in the liveness properties in the folder to the chapter "Liveness" of "Specifying Systems". The ctl[p]
function value in the properties should equal "req"
. However, this is never the case as the function range is only {"rdy", "busy", "done"}
.
This occurs at least in the following lines:
IMHO "req"
was meant to be "busy"
.
The current README does not order examples that make it easy to pick beginner-friendly examples.
Math:
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/SimpleMath
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/MoreMath
https://github.com/tlaplus/Examples/tree/master/specifications/TransitiveClosure
https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla
#23
Logic Puzzles:
https://github.com/tlaplus/Examples/blob/master/specifications/Stones/
https://github.com/tlaplus/Examples/tree/master/specifications/DieHard (there are also PlusCal versions somewhere)
https://github.com/tlaplus/Examples/tree/master/specifications/CarTalkPuzzle
https://github.com/tlaplus/Examples/tree/master/specifications/MissionariesAndCannibals
https://github.com/tlaplus/Examples/tree/master/specifications/N-Queens
https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners
Beginner specs based on popular problems in CS:
https://github.com/tlaplus/Examples/tree/master/specifications/tower_of_hanoi
https://github.com/tlaplus/Examples/tree/master/specifications/GameOfLife
https://github.com/tlaplus/Examples/tree/master/specifications/CigaretteSmokers
https://github.com/tlaplus/Examples/tree/master/specifications/SlidingPuzzles
Non-common concepts in TLA+:
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/Syntax (BNF grammar)
Specs of basic concurrent/distributed systems:
https://github.com/tlaplus/Examples/tree/master/specifications/Chameneos
https://github.com/tlaplus/Examples/tree/master/specifications/echo (PlusCal)
https://github.com/tlaplus/Examples/tree/master/specifications/Tla-tortoise-hare (PlusCal)
https://github.com/lemmy/BlockingQueue/ (tutorial)
https://github.com/tlaplus/Examples/tree/master/specifications/dijkstra-mutex
https://github.com/tlaplus/Examples/tree/master/specifications/ewd840
https://github.com/tlaplus/Examples/tree/master/specifications/ewd998
TLAPS:
https://github.com/tlaplus/Examples/tree/master/specifications/sums_even
https://github.com/tlaplus/Examples/tree/master/specifications/LoopInvariance
https://github.com/tlaplus/Examples/tree/master/specifications/TeachingConcurrency
Currently we manually exclude specific modules from proof checking in the CI because they run too long. Given that proof checking time can have as high of variability as model checking, it makes sense to include data about proof check time in the manifest then use that to determine whether to check the proof in the CI. Possibly we could have a CI workflow scheduled to run weekly which checks these long-running proofs along with the macOS workflow.
Failing proofs can continue to be manually excluded because ideally this repo would not have or accept any specs with failing proofs.
@konnov Do you have a variant of raft.tla that has been annotated with types for Apalache?
We did it at least once. There was one issue with Raft, where they used a function as a sequence:
There is a simple fix for that: just use SubSeq
instead of this explicit construction. I cannot find an annotated version of raft on my laptop though. We could probably add one in tlaplus-examples.
Originally posted by @konnov in tlaplus/tlaplus#677 (comment)
Was briefly discussed earlier in the year but IMO it would be better to just copy the specs into the repo. Reasons:
Thoughts? I will say that adding the specs as submodules is preferable to them only existing as a hyperlink though. One of the submodules added exposed a bug in tree-sitter-tlaplus pluscal parsing!
I noticed that some examples have .cfg files. Does anyone knows how to create them?
I did find a .cfg file somewhere in the in the Model_* directories but those config files seem to have added numbers to variable names.
Can I generate a clean .cfg file somehow?
Example:
https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners
https://github.com/tlaplus/Examples/blob/master/specifications/Prisoners/Prisoners.cfg
Currently the macOS CI takes over twice as long to run as the linux and windows CI runs: https://github.com/tlaplus/Examples/actions/runs/7835386801
This got substantially worse after the work to add models to most of the specs, because macOS CI runners see a strange amount of overhead for each model (for example a model taking 1 second to run on the other runners takes 8 seconds to run on the macOS runner). Looking online it seems slow macOS CI runners is a common problem experienced by developers across github.
Ideally the CI would run for ten minutes at most, and I don't think the macOS runner is providing enough value (given the similarity to linux) to justify keeping it around. Perhaps we could add a scheduled CI run to test on macOS once per week.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.