diff --git a/specifications/TLC/MCReachability.tla b/specifications/TLC/MCReachability.tla new file mode 100644 index 00000000..a2cb22c7 --- /dev/null +++ b/specifications/TLC/MCReachability.tla @@ -0,0 +1,179 @@ +---------------------------- MODULE MCReachability ---------------------------- +EXTENDS Naturals, Sequences, TLC +(***************************************************************************) +(* High-level specification of a state-graph explorer that does NOT *) +(* enforce BFS ordering. The frontier S is a set and the next state *) +(* to explore is chosen non-deterministically from S. *) +(* *) +(* The working phase (init / explore / process-successors) is determined *) +(* entirely by the data variables: *) +(* *) +(* init phase: successors = {} /\ S \ C # {} *) +(* explore phase: successors = {} /\ S \subseteq C *) +(* each phase: successors # {} *) +(* *) +(* S \subseteq C is an invariant of the post-init phases (Each adds to *) +(* both S and C when Constraint holds; Explore only removes from S), so *) +(* S \ C # {} vs S \subseteq C cleanly separates init from exploration. *) +(* *) +(* The only "control" variable is the boolean 'done', which records *) +(* forced termination (violation or deadlock). Normal completion *) +(* (frontier exhausted) needs no flag: S = {} /\ successors = {} simply *) +(* disables every action. *) +(***************************************************************************) + +(***************************************************************************) +(* A (state) graph G is a directed graph represented by a record with *) +(* 'states', 'initials', and 'actions' components. *) +(* *) +(* The CommunityModules Graphs.tla module is not used here because its *) +(* representation [node, edge] differs from ours: we use an adjacency *) +(* function (actions \in [states -> SUBSET states]) rather than an *) +(* explicit edge set (edge \subseteq node \X node), and carry a *) +(* distinguished 'initials' component that Graphs.tla does not model. *) +(***************************************************************************) +IsGraph(G) == /\ {"states", "initials", "actions"} = DOMAIN G + /\ G.actions \in [G.states -> SUBSET G.states] + /\ G.initials \subseteq G.states + +(***************************************************************************) +(* Successor states of s, excluding self-loops. *) +(***************************************************************************) +SuccessorsOf(s, SG) == {t \in SG.actions[s] : t # s} + +(***************************************************************************) +(* The predecessor of v in a spanning tree t (a set of *) +(* <> pairs) is the first element of the *) +(* unique pair whose second element equals v. *) +(***************************************************************************) +Predecessor(t, v) == (CHOOSE pair \in t : pair[2] = v)[1] + +CONSTANT StateGraph, ViolationStates, + Constraint(_, _) \* Constraint(s,l) iff state s may be explored at BFS level l; + \* successors with FALSE are not added to S or C (but are + \* still recorded in T and in L). + +ASSUME /\ IsGraph(StateGraph) + /\ ViolationStates \subseteq StateGraph.states + /\ \A s \in StateGraph.states, l \in Nat : Constraint(s, l) \in BOOLEAN + +VARIABLES S, \* Frontier: set of states yet to explore + C, \* Set of visited states + successors, \* Subset of Nat \X StateGraph.states: pairs <> still to + \* process for the current Explore step (same lvl for all). + done, \* TRUE after violation or deadlock detected + T, \* Set of <> pairs (spanning tree) + counterexample, \* Path from initial state to violation/deadlock state + L \* BFS level of each state that has been assigned a level + +vars == <> + +Init == /\ S = StateGraph.initials + /\ C = {} + /\ successors = {} + /\ done = FALSE + /\ T = {} + /\ counterexample = <<>> + /\ L = [s \in {} |-> 0] + +--------------------------------------------------------------------------- + +(***************************************************************************) +(* Check an initial state for a safety violation. *) +(***************************************************************************) +InitCheck == + /\ ~done + /\ successors = {} + /\ \E s \in S \ C : + /\ C' = C \cup {s} + /\ L' = (s :> 0) @@ L + /\ done' = (s \in ViolationStates) + /\ counterexample' = IF s \in ViolationStates + THEN <> ELSE counterexample + /\ UNCHANGED <> + +--------------------------------------------------------------------------- + +(***************************************************************************) +(* Pick any state from the frontier S for exploration. The next state *) +(* is chosen non-deterministically (\E s \in S), so no ordering is *) +(* imposed on the exploration. The predecessor pairs for all new *) +(* successors are added to T here. *) +(***************************************************************************) +Explore == + /\ ~done + /\ successors = {} + /\ S \subseteq C + /\ S # {} + /\ \E s \in S : + LET succs == SuccessorsOf(s, StateGraph) \ C + lvl == L[s] + 1 + IN /\ S' = S \ {s} + /\ successors' = {<> : t \in succs} + /\ T' = T \cup {<> : t \in succs} + /\ done' = (SuccessorsOf(s, StateGraph) = {}) + /\ counterexample' = IF SuccessorsOf(s, StateGraph) = {} + THEN <> ELSE counterexample + /\ UNCHANGED <> + +--------------------------------------------------------------------------- + +(***************************************************************************) +(* Process one successor: mark visited, add to frontier, check violation. *) +(***************************************************************************) +Each == + /\ ~done + /\ successors # {} + /\ \E succ \in successors : + /\ successors' = successors \ {succ} + /\ IF Constraint(succ[2], succ[1]) + THEN /\ C' = C \cup {succ[2]} + /\ S' = S \cup {succ[2]} + ELSE UNCHANGED <> + /\ L' = (succ[2] :> succ[1]) @@ L + /\ done' = (succ[2] \in ViolationStates) + /\ counterexample' = IF succ[2] \in ViolationStates + THEN <> ELSE counterexample + /\ UNCHANGED T + +--------------------------------------------------------------------------- + +(***************************************************************************) +(* Trace reconstruction: walk backward through T, prepending *) +(* predecessors to the counterexample until an initial state is reached. *) +(***************************************************************************) +Trc == + /\ done + /\ counterexample # <<>> + /\ Head(counterexample) \notin StateGraph.initials + /\ counterexample' = <> + \o counterexample + /\ UNCHANGED <> + +--------------------------------------------------------------------------- + +Terminating == done /\ UNCHANGED vars + +Next == + \/ InitCheck + \/ Explore + \/ Each + \/ Trc + \/ Terminating + +Spec == + /\ Init /\ [][Next]_vars + /\ WF_vars(Next) + +Termination == <>(done \/ (S = {} /\ successors = {})) + +(***************************************************************************) +(* If violation states exist, the explorer eventually finds one and *) +(* constructs a valid counterexample path from an initial state to it. *) +(***************************************************************************) +Live == ViolationStates # {} => + <>[](/\ counterexample # <<>> + /\ counterexample[Len(counterexample)] \in ViolationStates + /\ counterexample[1] \in StateGraph.initials) + +============================================================================= diff --git a/specifications/TLC/StateGraphs.tla b/specifications/TLC/StateGraphs.tla new file mode 100644 index 00000000..88b1fdf1 --- /dev/null +++ b/specifications/TLC/StateGraphs.tla @@ -0,0 +1,118 @@ +---------------------------- MODULE StateGraphs ---------------------------- +EXTENDS Sequences, Integers, IOUtils +(***************************************************************************) +(* Definitions of directed state graphs and their violation sets, used *) +(* for testing model-checker specifications (TLCMC, MCReachability). *) +(***************************************************************************) + +\* 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 == {} + +----------------------------------------------------------------------------- + +GraphName == IF "GRAPH" \in DOMAIN IOEnv THEN IOEnv.GRAPH ELSE "7" + +TestCase == CASE GraphName = "1" -> [g |-> G1, v |-> V1] + [] GraphName = "1a" -> [g |-> G1a, v |-> V1a] + [] GraphName = "2" -> [g |-> G2, v |-> V2] + [] GraphName = "3" -> [g |-> G3, v |-> V3] + [] GraphName = "4" -> [g |-> G4, v |-> V4] + [] GraphName = "5" -> [g |-> G5, v |-> V5] + [] GraphName = "6" -> [g |-> G6, v |-> V6] + [] GraphName = "7" -> [g |-> G7, v |-> V7] + [] GraphName = "8" -> [g |-> G8, v |-> V8] + [] GraphName = "9" -> [g |-> G9, v |-> V9] + [] GraphName = "10" -> [g |-> G10, v |-> V10] + [] GraphName = "11" -> [g |-> G11, v |-> V11] + [] GraphName = "12" -> [g |-> G12, v |-> V12] + [] GraphName = "13" -> [g |-> G13, v |-> V13] + +============================================================================= diff --git a/specifications/TLC/TLCMC.tla b/specifications/TLC/TLCMC.tla index b81f1431..8788f4f0 100644 --- a/specifications/TLC/TLCMC.tla +++ b/specifications/TLC/TLCMC.tla @@ -8,6 +8,15 @@ EXTENDS Integers, Sequences, FiniteSets, TLC (***************************************************************************) SeqToSet(seq) == {seq[i] : i \in 1..Len(seq)} +\* Min is also defined in CommunityModules (Functions.tla); inlined here +\* to avoid that dependency. +Min(a, b) == IF a < b THEN a ELSE b + +\* Remove exactly the element at index idx (1..Len(s)). Value-based +\* removal would drop every copy of S[idx] and ignore idx, which breaks +\* non-strict BFS when the frontier sequence holds duplicate states. +RemoveAt(s, idx) == SubSeq(s, 1, idx-1) \o SubSeq(s, idx+1, Len(s)) + (***************************************************************************) (* Returns a Set of those permutations created out of the elements of Set *) (* set which satisfy Filter. *) @@ -18,7 +27,7 @@ SetToSeqs(set, Filter(_)) == UNION {{perm \in [1..Cardinality(set) -> set]: Filter(perm)}} (***************************************************************************) -(* Returns a Set of all possible permutations with distinct elements *) +(* 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. *) (***************************************************************************) @@ -38,7 +47,7 @@ IsGraph(G) == /\ {"states", "initials", "actions"} = DOMAIN G /\ G.initials \subseteq G.states (***************************************************************************) -(* A set of all permutations of the initial states of G. *) +(* A set of all permutations of the initial states of G. *) (***************************************************************************) SetOfAllPermutationsOfInitials(G) == SetToDistSeqs(G.initials) @@ -56,24 +65,37 @@ SuccessorsOf(state, SG) == {successor \in SG.actions[state]: (***************************************************************************) Predecessor(t, v) == SelectSeq(t, LAMBDA pair: pair[2] = v)[1][1] -CONSTANT StateGraph, ViolationStates, null +CONSTANT StateGraph, ViolationStates, null, + K, \* Number of workers: window size for non-strict BFS dequeue. + \* K = 1 is strict BFS; K > 1 models TLC's degraded BFS. + Constraint(_, _) \* State constraint predicate: Constraint(s, l) = TRUE + \* iff state s at BFS level l should be explored. + \* Successors for which Constraint is FALSE are not + \* added to C or S. -ASSUME \* The given StateGraph is actually a graph - \/ IsGraph(StateGraph) - \* The violating states are vertices in the state graph. - \/ ViolationStates \subseteq StateGraph.states +(***************************************************************************) +(* Constants are well-formed: StateGraph is a graph; ViolationStates is a *) +(* subset of its vertices; K is a positive natural; Constraint(s,l) is a *) +(* Boolean for every state s and level l. *) +(***************************************************************************) +ASSUME /\ IsGraph(StateGraph) + /\ ViolationStates \subseteq StateGraph.states + /\ K \in Nat \ {0} + /\ \A s \in StateGraph.states : \A l \in Nat : Constraint(s, l) \in BOOLEAN (*************************************************************************** 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. + \* A sequence of unexplored states used as a FIFO queue + \* for BFS exploration. With K = 1 (single worker), + \* strict BFS always dequeues Head(S). With K > 1, + \* any of the first Min(K, Len(S)) elements may be + \* dequeued, modeling TLC's degraded (non-strict) BFS + \* with multiple workers. + \* S is initialized with each possible permutation + \* of the initial states because there is no defined + \* order of initial states. S \in SetOfAllPermutationsOfInitials(StateGraph), \* A set of already explored states. C = {}, @@ -88,7 +110,11 @@ The PlusCal code of the model checker algorithm counterexample = <<>>, \* A sequence of pairs such that a pair is a \* sequence <>. - T = <<>>; + T = <<>>, + \* BFS level of each explored state: a function + \* from states to their distance from an initial + \* state. Initial states have level 0. + L = [s \in {} |-> 0]; { (* Check initial states for violations. We could be clever and check the initial states as part @@ -105,6 +131,7 @@ The PlusCal code of the model checker algorithm \* exploration visits it again \* due to a cycle. C := C \cup {state}; + L := (state :> 0) @@ L; i := i + 1; if (state \in ViolationStates) { counterexample := <>; @@ -119,12 +146,11 @@ The PlusCal code of the model checker algorithm 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); + \* Non-strict BFS: pick any of the first K elements. + with (idx \in 1..Min(K, Len(S))) { + state := S[idx]; + S := RemoveAt(S, idx); + }; \* For each unexplored successor 'succ' do: successors := SuccessorsOf(state, StateGraph) \ C; @@ -140,12 +166,15 @@ The PlusCal code of the model checker algorithm \* Exclude succ in this while loop. successors := successors \ {succ}; - \* Mark successor globally visited. - C := C \cup {succ}; S := S \o <>; + if (Constraint(succ, L[state] + 1)) { + \* Mark successor globally visited. + C := C \cup {succ}; S := S \o <>; + }; \* Append succ to T and add it \* to the list of unexplored states. T := T \o << <> >>; + L := (succ :> (L[state] + 1)) @@ L; \* Check state for violation of a \* safety property (simplified @@ -181,10 +210,10 @@ The PlusCal code of the model checker algorithm } } ***************************************************************************) -\* BEGIN TRANSLATION -VARIABLES S, C, state, successors, i, counterexample, T, pc +\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "95808c34") +VARIABLES pc, S, C, state, successors, i, counterexample, T, L -vars == << S, C, state, successors, i, counterexample, T, pc >> +vars == << pc, S, C, state, successors, i, counterexample, T, L >> Init == (* Global variables *) /\ S \in SetOfAllPermutationsOfInitials(StateGraph) @@ -194,12 +223,14 @@ Init == (* Global variables *) /\ i = 1 /\ counterexample = <<>> /\ T = <<>> + /\ L = [s \in {} |-> 0] /\ pc = "init" init == /\ pc = "init" /\ IF i \leq Len(S) THEN /\ state' = S[i] /\ C' = (C \cup {state'}) + /\ L' = (state' :> 0) @@ L /\ i' = i + 1 /\ IF state' \in ViolationStates THEN /\ counterexample' = <> @@ -207,19 +238,20 @@ init == /\ pc = "init" ELSE /\ pc' = "init" /\ UNCHANGED counterexample ELSE /\ pc' = "initPost" - /\ UNCHANGED << C, state, i, counterexample >> + /\ UNCHANGED << C, state, i, counterexample, L >> /\ UNCHANGED << S, successors, T >> initPost == /\ pc = "initPost" /\ Assert(C = SeqToSet(S), - "Failure of assertion at line 116, column 18.") + "Failure of assertion at line 143, column 18.") /\ pc' = "scsr" - /\ UNCHANGED << S, C, state, successors, i, counterexample, T >> + /\ UNCHANGED << S, C, state, successors, i, counterexample, T, L >> scsr == /\ pc = "scsr" /\ IF Len(S) # 0 - THEN /\ state' = Head(S) - /\ S' = Tail(S) + THEN /\ \E idx \in 1..Min(K, Len(S)): + /\ state' = S[idx] + /\ S' = RemoveAt(S, idx) /\ successors' = SuccessorsOf(state', StateGraph) \ C /\ IF SuccessorsOf(state', StateGraph) = {} THEN /\ counterexample' = <> @@ -227,25 +259,29 @@ scsr == /\ pc = "scsr" ELSE /\ pc' = "each" /\ UNCHANGED counterexample ELSE /\ Assert(S = <<>> /\ ViolationStates = {}, - "Failure of assertion at line 164, column 8.") + "Failure of assertion at line 193, column 8.") /\ pc' = "Done" /\ UNCHANGED << S, state, successors, counterexample >> - /\ UNCHANGED << C, i, T >> + /\ UNCHANGED << C, i, T, L >> each == /\ pc = "each" /\ IF successors # {} THEN /\ \E succ \in successors: /\ successors' = successors \ {succ} - /\ C' = (C \cup {succ}) - /\ S' = S \o <> + /\ IF Constraint(succ, L[state] + 1) + THEN /\ C' = (C \cup {succ}) + /\ S' = S \o <> + ELSE /\ TRUE + /\ UNCHANGED << S, C >> /\ T' = T \o << <> >> + /\ L' = (succ :> (L[state] + 1)) @@ L /\ IF succ \in ViolationStates THEN /\ counterexample' = <> /\ pc' = "trc" ELSE /\ pc' = "each" /\ UNCHANGED counterexample ELSE /\ pc' = "scsr" - /\ UNCHANGED << S, C, successors, counterexample, T >> + /\ UNCHANGED << S, C, successors, counterexample, T, L >> /\ UNCHANGED << state, i >> trc == /\ pc = "trc" @@ -253,10 +289,10 @@ trc == /\ pc = "trc" THEN /\ counterexample' = <> \o counterexample /\ pc' = "trc" ELSE /\ Assert(counterexample # <<>>, - "Failure of assertion at line 177, column 20.") + "Failure of assertion at line 206, column 20.") /\ pc' = "Done" /\ UNCHANGED counterexample - /\ UNCHANGED << S, C, state, successors, i, T >> + /\ UNCHANGED << S, C, state, successors, i, T, L >> (* Allow infinite stuttering to prevent deadlock on termination. *) Terminating == pc = "Done" /\ UNCHANGED vars @@ -269,10 +305,46 @@ Spec == /\ Init /\ [][Next]_vars Termination == <>(pc = "Done") -\* END TRANSLATION +\* END TRANSLATION Live == ViolationStates # {} => <>[](/\ Len(counterexample) > 0 /\ counterexample[Len(counterexample)] \in ViolationStates /\ counterexample[1] \in StateGraph.initials) +----------------------------------------------------------------------------- + +(***************************************************************************) +(* Refinement: TLCMC (non-strict BFS with S as a FIFO sequence) refines *) +(* MCReachability (non-deterministic exploration with S as a set). *) +(* *) +(* C, counterexample, L, and Constraint match directly. S maps from *) +(* sequence to set. TLCMC's successor set maps to <> pairs with *) +(* lvl = L[state]+1 (or 0 when idle: init/initPost or first scsr with *) +(* C = SeqToSet(S)). *) +(* *) +(* done is mapped to counterexample # <<>>: TRUE exactly when a *) +(* violation or deadlock has been found. Normal completion (frontier *) +(* exhausted, no violation) keeps counterexample = <<>>, so done stays *) +(* FALSE and the TLCMC termination step is a stutter in MCReachability. *) +(* *) +(* T is mapped as SeqToSet(T) plus the set of pairs {<> : s *) +(* in successors} that the each loop will move into T. This makes the *) +(* mapped T change atomically at the scsr boundary (matching Explore) *) +(* and stay invariant through the each loop (matching Each's UNCHANGED T). *) +(***************************************************************************) +MCR == INSTANCE MCReachability WITH + S <- SeqToSet(S), + done <- counterexample # <<>>, + T <- SeqToSet(T) \cup {<> : succ \in successors}, + Constraint <- Constraint, + L <- L, + successors <- LET lvl == IF pc \in {"init", "initPost"} + THEN 0 + ELSE IF pc = "scsr" /\ successors = {} /\ C = SeqToSet(S) + THEN 0 + ELSE L[state] + 1 + IN {<> : s \in successors} + +Refinement == MCR!Spec + ============================================================================= diff --git a/specifications/TLC/TestGraphs.cfg b/specifications/TLC/TestGraphs.cfg index 5d1cd290..cc9fad80 100644 --- a/specifications/TLC/TestGraphs.cfg +++ b/specifications/TLC/TestGraphs.cfg @@ -7,4 +7,5 @@ SPECIFICATION PROPERTIES Termination - Live \ No newline at end of file + Live + Refinement \ No newline at end of file diff --git a/specifications/TLC/TestGraphs.tla b/specifications/TLC/TestGraphs.tla index 7b6943f4..d4129dcd 100644 --- a/specifications/TLC/TestGraphs.tla +++ b/specifications/TLC/TestGraphs.tla @@ -1,106 +1,16 @@ ----------------------------- MODULE TestGraphs ----------------------------- -EXTENDS Sequences, Integers +EXTENDS StateGraphs (***************************************************************************) -(* The definitions of some graphs, paths, etc. used for testing the *) -(* definitions and the algorithm with the TLC model checker. *) +(* Test harness for TLCMC using graphs defined in StateGraphs. *) (***************************************************************************) -\* 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 == {} - ------------------------------------------------------------------------------ - CONSTANT null -VARIABLES S, C, state, successors, i, counterexample, T, pc +VARIABLES S, C, state, successors, i, counterexample, T, L, pc + +Workers == IF "K" \in DOMAIN IOEnv THEN atoi(IOEnv.K) ELSE 1 -INSTANCE TLCMC WITH StateGraph <- G7, ViolationStates <- V7 +INSTANCE TLCMC WITH StateGraph <- TestCase.g, ViolationStates <- TestCase.v, K <- Workers, Constraint <- LAMBDA s, l : TRUE ============================================================================= + +$ for g in 1 2 3 4 5 6 8 9 12 13; do for k in 1 2 3; do echo "=== Graph G$g, K=$k ==="; GRAPH=$g K=$k tlc -config TestGraphs.cfg TestGraphs.tla ; echo ""; done; done \ No newline at end of file diff --git a/specifications/TLC/TestMCReachability.cfg b/specifications/TLC/TestMCReachability.cfg new file mode 100644 index 00000000..af806502 --- /dev/null +++ b/specifications/TLC/TestMCReachability.cfg @@ -0,0 +1,6 @@ +SPECIFICATION + Spec + +PROPERTIES + Termination + Live diff --git a/specifications/TLC/TestMCReachability.tla b/specifications/TLC/TestMCReachability.tla new file mode 100644 index 00000000..3c452d48 --- /dev/null +++ b/specifications/TLC/TestMCReachability.tla @@ -0,0 +1,14 @@ +------------------------- MODULE TestMCReachability ------------------------- +EXTENDS StateGraphs +(***************************************************************************) +(* Test harness for MCReachability using graphs defined in StateGraphs. *) +(***************************************************************************) + +VARIABLES S, C, successors, done, T, counterexample, L + +INSTANCE MCReachability WITH + StateGraph <- TestCase.g, + ViolationStates <- TestCase.v, + Constraint <- LAMBDA s, l : TRUE + +============================================================================= diff --git a/specifications/TLC/manifest.json b/specifications/TLC/manifest.json index 30397093..3f02fb35 100644 --- a/specifications/TLC/manifest.json +++ b/specifications/TLC/manifest.json @@ -12,6 +12,16 @@ ], "models": [] }, + { + "path": "specifications/TLC/MCReachability.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/TLC/StateGraphs.tla", + "features": [], + "models": [] + }, { "path": "specifications/TLC/TestGraphs.tla", "features": [], @@ -26,6 +36,18 @@ "stateDepth": 52 } ] + }, + { + "path": "specifications/TLC/TestMCReachability.tla", + "features": [], + "models": [ + { + "path": "specifications/TLC/TestMCReachability.cfg", + "runtime": "unknown", + "mode": "exhaustive search", + "result": "success" + } + ] } ] } \ No newline at end of file