From c48a6ee48a71e0fe477ed2b648db50a2f950673e Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 1 Apr 2026 12:37:50 -0700 Subject: [PATCH] TLCMC: non-strict BFS, BFS level tracking, state constraints, and refinement to MCReachability. Parameterize TLCMC with constant K (number of workers): dequeue any of the first Min(K, Len(S)) elements from the frontier instead of always Head(S), modeling TLC's degraded BFS with multiple workers. Track BFS level of each explored state in new variable L (distance from an initial state). Add Constraint(s, l) predicate to prune successors from exploration based on state and level. Inline Min from CommunityModules to keep the spec/example self-contained. Introduce MCReachability, a high-level spec with set-based frontier S and non-deterministic exploration order. TLCMC refines MCReachability via a refinement mapping. Extract graph definitions into StateGraphs module; refactor TestGraphs and add TestMCReachability as test harnesses. Select graph and worker count via IOEnv to run all test configurations from a single .cfg file without per-graph TLC invocations. [Feature] Signed-off-by: Markus Alexander Kuppe --- specifications/TLC/MCReachability.tla | 179 ++++++++++++++++++++++ specifications/TLC/StateGraphs.tla | 118 ++++++++++++++ specifications/TLC/TLCMC.tla | 150 +++++++++++++----- specifications/TLC/TestGraphs.cfg | 3 +- specifications/TLC/TestGraphs.tla | 106 +------------ specifications/TLC/TestMCReachability.cfg | 6 + specifications/TLC/TestMCReachability.tla | 14 ++ specifications/TLC/manifest.json | 22 +++ 8 files changed, 460 insertions(+), 138 deletions(-) create mode 100644 specifications/TLC/MCReachability.tla create mode 100644 specifications/TLC/StateGraphs.tla create mode 100644 specifications/TLC/TestMCReachability.cfg create mode 100644 specifications/TLC/TestMCReachability.tla 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