From cfcf174c253b7240ae372c25b92a390bb3d4c17c Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 1 Apr 2026 12:37:50 -0700 Subject: [PATCH 1/3] 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 | 158 +++++++++++++++++++ specifications/TLC/StateGraphs.tla | 118 +++++++++++++++ specifications/TLC/TLCMC.tla | 176 +++++++++++++++------- specifications/TLC/TestGraphs.cfg | 3 +- specifications/TLC/TestGraphs.tla | 106 +------------ specifications/TLC/TestMCReachability.cfg | 6 + specifications/TLC/TestMCReachability.tla | 13 ++ specifications/TLC/manifest.json | 28 +++- 8 files changed, 453 insertions(+), 155 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..b19f5be3 --- /dev/null +++ b/specifications/TLC/MCReachability.tla @@ -0,0 +1,158 @@ +---------------------------- 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. *) +(***************************************************************************) + +(***************************************************************************) +(* 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 + +ASSUME /\ IsGraph(StateGraph) + /\ ViolationStates \subseteq StateGraph.states + +VARIABLES S, \* Frontier: set of states yet to explore + C, \* Set of visited states + T, \* Set of <> pairs (spanning tree) + L, \* BFS level of each state that has been assigned a level + successors, \* Triples <> still to process for the current + \* Explore step: t is the successor at BFS level lvl, + \* s is the predecessor that generated it. + done, \* TRUE after violation or deadlock detected + counterexample \* Path from initial state to violation/deadlock state + +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. 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} + /\ C' = C \cup {succ[2]} + /\ S' = S \cup {succ[2]} + /\ 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..84a86128 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. *) (***************************************************************************) @@ -37,11 +46,6 @@ 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. *) (***************************************************************************) @@ -56,24 +60,45 @@ 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 + +(***************************************************************************) +(* A set of all permutations of the initial states of G that satisfy the *) +(* state constraint at BFS level 0. *) +(***************************************************************************) +SetOfAllPermutationsOfInitials(G) == + SetToDistSeqs({s \in G.initials : Constraint(s, 0)}) (*************************************************************************** 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 that satisfy the state + \* constraint at BFS level 0, because there is no + \* defined order of initial states. S \in SetOfAllPermutationsOfInitials(StateGraph), \* A set of already explored states. C = {}, @@ -88,7 +113,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 +134,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 +149,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,18 +169,27 @@ 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 <>; + \* T and L are inside the Constraint guard to + \* match TLC, which never records constrained- + \* away states. Moving them outside is legal + \* but keeps those states out of C, so + \* SuccessorsOf(state, StateGraph) \ C stays + \* larger, increasing nondeterminism in each + \* and causing TLC to explore *more* distinct + \* states. + T := T \o << <> >>; + L := (succ :> (L[state] + 1)) @@ L; + }; - \* Append succ to T and add it - \* to the list of unexplored states. - T := T \o << <> >>; \* Check state for violation of a \* safety property (simplified \* to a check of set membership. if (succ \in ViolationStates) { - counterexample := <>; + counterexample := <>; \* Terminate model checking goto trc; }; @@ -159,9 +197,9 @@ The PlusCal code of the model checker algorithm }; }; (* Model Checking terminated without finding - a violation. *) - \* No states left unexplored and no ViolationState given. - assert S = <<>> /\ ViolationStates = {}; + a violation (or all violations were unreachable / + pruned by Constraint). *) + assert S = <<>>; goto Done; (* Create a counterexample, that is a path @@ -181,10 +219,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) = "f48dc6da") +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 +232,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,45 +247,50 @@ 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 148, 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' = <> /\ pc' = "trc" ELSE /\ pc' = "each" /\ UNCHANGED counterexample - ELSE /\ Assert(S = <<>> /\ ViolationStates = {}, - "Failure of assertion at line 164, column 8.") + ELSE /\ Assert(S = <<>>, + "Failure of assertion at line 204, 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 <> - /\ T' = T \o << <> >> + /\ IF Constraint(succ, L[state] + 1) + THEN /\ C' = (C \cup {succ}) + /\ S' = S \o <> + /\ T' = T \o << <> >> + /\ L' = (succ :> (L[state] + 1)) @@ L + ELSE /\ TRUE + /\ UNCHANGED << S, C, T, L >> /\ IF succ \in ViolationStates - THEN /\ counterexample' = <> + 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 +298,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 217, 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 +314,35 @@ 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). *) +(* *) +(* NOTE: MCReachability does not model state constraints. The refinement *) +(* therefore only holds when Constraint is trivially TRUE (the default). *) +(* With a non-trivial Constraint, TLCMC may prune successors that *) +(* MCReachability explores, breaking the simulation. *) +(***************************************************************************) +MCR == INSTANCE MCReachability WITH + S <- SeqToSet(S), + done <- counterexample # <<>>, + T <- SeqToSet(T) \cup {<> : succ \in successors}, + 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..1f9069b7 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 7 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 || break 2; 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..92f1e196 --- /dev/null +++ b/specifications/TLC/TestMCReachability.tla @@ -0,0 +1,13 @@ +------------------------- 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 + +============================================================================= diff --git a/specifications/TLC/manifest.json b/specifications/TLC/manifest.json index 30397093..384180ed 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": [], @@ -21,9 +31,21 @@ "runtime": "00:00:05", "mode": "exhaustive search", "result": "success", - "distinctStates": 2790, - "totalStates": 2990, - "stateDepth": 52 + "distinctStates": 2590, + "totalStates": 2790, + "stateDepth": 51 + } + ] + }, + { + "path": "specifications/TLC/TestMCReachability.tla", + "features": [], + "models": [ + { + "path": "specifications/TLC/TestMCReachability.cfg", + "runtime": "unknown", + "mode": "exhaustive search", + "result": "success" } ] } From cc539cf65bc016a4872fa6663be62ec3c977039c Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 3 Apr 2026 17:02:39 -0700 Subject: [PATCH 2/3] Strengthen Live property. Strengthen the Live property by asserting over entire traces rather than only the final state. For K = 1, further restrict the property to require that the trace belongs to the subset of shortest traces. [Feature] Signed-off-by: Markus Alexander Kuppe --- specifications/TLC/StateGraphs.tla | 47 +++++++++++++++++++----------- specifications/TLC/TLCMC.tla | 25 +++++++++++----- specifications/TLC/TestGraphs.tla | 4 +-- 3 files changed, 50 insertions(+), 26 deletions(-) diff --git a/specifications/TLC/StateGraphs.tla b/specifications/TLC/StateGraphs.tla index 88b1fdf1..cc34b5c0 100644 --- a/specifications/TLC/StateGraphs.tla +++ b/specifications/TLC/StateGraphs.tla @@ -11,6 +11,7 @@ G1 == [states |-> 1..4, actions |-> << {1,2}, {1,3}, {4}, {3} >> ] V1 == {4} +CX1 == {<<2, 3, 4>>} \* Graph 1a. G1a == [states |-> 1..4, @@ -24,31 +25,36 @@ V1a == {1} G2 == [states |-> 1..5, initials |-> {1,3}, actions |-> << {1, 2}, {1}, {4, 5}, {}, {} >> ] -V2 == {2,5} +V2 == {2,5} +CX2 == {<<1, 2>>, <<3, 5>>} \* Graph 3. G3 == [states |-> 1..4, initials |-> {2}, actions |-> << {1,2}, {2,3}, {3,4}, {1,4} >> ] V3 == {1} - +CX3 == {<<2, 3, 4, 1>>} + \* Graph 4. G4 == [states |-> 1..9, initials |-> {1,2,3}, actions |-> << {3}, {4}, {5}, {6}, {7}, {7}, {8, 9}, {}, {4} >> ] V4 == {8} - +CX4 == {<<3, 5, 7, 8>>, <<2, 4, 6, 7, 8>>} + \* Graph 5. G5 == [states |-> 1..9, initials |-> {9}, actions |-> << {4,2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {2} >> ] V5 == {8} +CX5 == {<<9, 2, 3, 4, 5, 6, 7, 8>>} \* Graph 6. G6 == [states |-> 1..5, initials |-> {5}, actions |-> << {2,4,5}, {2}, {1}, {4}, {3} >> ] V6 == {2} +CX6 == {<<5, 3, 1, 2>>} \* Graph Medium (node 22 is a sink) G7 == [states |-> 1..50, @@ -59,60 +65,67 @@ G7 == [states |-> 1..50, {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} +CX7 == {<<1,35,20,16,50>>, <<1,35,41,16,50>>, <<1,8,42,29,30,50>>, <<1,8,45,40,19,29,30,50>>} \* Graph 8. G8 == [states |-> 1..4, initials |-> {1}, actions |-> <<{1,2},{2,3},{3,4},{4}>>] V8 == {} +CX8 == {<<1, 2, 3, 4>>} \* Graph 9. G9 == [states |-> {1}, initials |-> {1}, actions |-> <<{1}>>] V9 == {1} +CX9 == {<<1>>} \* Graph 10. G10 == [states |-> {}, initials |-> {}, actions |-> <<>>] V10 == {} +CX10 == {} \* Graph 11. G11 == [states |-> 1..10, initials |-> {}, actions |-> << {}, {}, {}, {}, {}, {}, {}, {}, {}, {} >>] V11 == {} +CX11 == {} \* Graph 12. G12 == [states |-> 1..3, initials |-> {1,2,3}, actions |-> <<{},{},{}>>] V12 == {1} +CX12 == {<<1>>} \* Graph 13 (simple sequence). G13 == [states |-> 1..3, initials |-> {1}, actions |-> <<{2},{3},{}>>] V13 == {} +CX13 == {<<1, 2, 3>>} ----------------------------------------------------------------------------- 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] +TestCase == CASE GraphName = "1" -> [g |-> G1, v |-> V1, cx |-> CX1] + [] GraphName = "1a" -> [g |-> G1a, v |-> V1a, cx |-> {}] + [] GraphName = "2" -> [g |-> G2, v |-> V2, cx |-> CX2] + [] GraphName = "3" -> [g |-> G3, v |-> V3, cx |-> CX3] + [] GraphName = "4" -> [g |-> G4, v |-> V4, cx |-> CX4] + [] GraphName = "5" -> [g |-> G5, v |-> V5, cx |-> CX5] + [] GraphName = "6" -> [g |-> G6, v |-> V6, cx |-> CX6] + [] GraphName = "7" -> [g |-> G7, v |-> V7, cx |-> CX7] + [] GraphName = "8" -> [g |-> G8, v |-> V8, cx |-> CX8] + [] GraphName = "9" -> [g |-> G9, v |-> V9, cx |-> CX9] + [] GraphName = "10" -> [g |-> G10, v |-> V10, cx |-> CX10] + [] GraphName = "11" -> [g |-> G11, v |-> V11, cx |-> CX11] + [] GraphName = "12" -> [g |-> G12, v |-> V12, cx |-> CX12] + [] GraphName = "13" -> [g |-> G13, v |-> V13, cx |-> CX13] ============================================================================= diff --git a/specifications/TLC/TLCMC.tla b/specifications/TLC/TLCMC.tla index 84a86128..89cd1750 100644 --- a/specifications/TLC/TLCMC.tla +++ b/specifications/TLC/TLCMC.tla @@ -63,10 +63,12 @@ Predecessor(t, v) == SelectSeq(t, LAMBDA pair: pair[2] = v)[1][1] 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. + 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. + Counterexamples \* Set of known counterexample sequences for the + \* current graph/violation pair. (***************************************************************************) (* Constants are well-formed: StateGraph is a graph; ViolationStates is a *) @@ -316,9 +318,18 @@ Termination == <>(pc = "Done") \* END TRANSLATION -Live == ViolationStates # {} => <>[](/\ Len(counterexample) > 0 - /\ counterexample[Len(counterexample)] \in ViolationStates - /\ counterexample[1] \in StateGraph.initials) +\* NOTE: The minimality conjunct (Len = minLen) for K = 1 assumes the +\* Constraint does not prune any intermediate state on a shortest +\* counterexample path. If Constraint(s, l) = FALSE for some state s +\* on such a path at its BFS level l, strict BFS can only reach the +\* violation through a longer route and the conjunct will not hold. +Live == ViolationStates # {} => + <>[](/\ counterexample \in Counterexamples + /\ IF K = 1 + THEN LET lens == {Len(cx) : cx \in Counterexamples} + minLen == CHOOSE m \in lens : \A n \in lens : m <= n + IN Len(counterexample) = minLen + ELSE TRUE) ----------------------------------------------------------------------------- diff --git a/specifications/TLC/TestGraphs.tla b/specifications/TLC/TestGraphs.tla index 1f9069b7..e414863d 100644 --- a/specifications/TLC/TestGraphs.tla +++ b/specifications/TLC/TestGraphs.tla @@ -9,8 +9,8 @@ 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 <- TestCase.g, ViolationStates <- TestCase.v, K <- Workers, Constraint <- LAMBDA s, l : TRUE +INSTANCE TLCMC WITH StateGraph <- TestCase.g, ViolationStates <- TestCase.v, K <- Workers, Constraint <- LAMBDA s, l : TRUE, Counterexamples <- TestCase.cx ============================================================================= -$ for g in 1 2 3 4 5 6 7 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 || break 2; done; done \ No newline at end of file +$ for g in 1 2 3 4 5 6 7 8 9 10 11 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 || break 2; done; done \ No newline at end of file From 6fc4463615b401e403464ebfb063c9089a66183e Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 3 Apr 2026 17:31:52 -0700 Subject: [PATCH 3/3] Add DieHard graph Introduce a new graph definition for the DieHard puzzle, including 101 states, initial states, actions, and counterexamples. Update the TestCase to support this new graph configuration. [Feature] Signed-off-by: Markus Alexander Kuppe --- specifications/TLC/StateGraphs.tla | 131 +++++++++++++++++++++++++++++ 1 file changed, 131 insertions(+) diff --git a/specifications/TLC/StateGraphs.tla b/specifications/TLC/StateGraphs.tla index cc34b5c0..ae53c7a6 100644 --- a/specifications/TLC/StateGraphs.tla +++ b/specifications/TLC/StateGraphs.tla @@ -109,6 +109,136 @@ G13 == [states |-> 1..3, V13 == {} CX13 == {<<1, 2, 3>>} +\* Graph DH (101 states, DieHard puzzle (tlatools/org.lamport.tlatools/test-model/DieHard.tla), bigBucket # 4, -fp 1). +GDH == + [ states |-> 1 .. 101, + initials |-> { 69 }, + actions |-> + << { 1, 15, 35, 49, 70, 86 }, + { 2, 16, 36, 50, 70, 86 }, + { 3, 17, 37, 51, 70, 86 }, + { 4, 18, 38, 52, 70, 86 }, + { 5, 15, 39, 49, 71, 88 }, + { 6, 16, 40, 50, 71, 88 }, + { 7, 17, 41, 51, 71, 88 }, + { 8, 15, 42, 49, 73, 90 }, + { 9, 16, 43, 50, 73, 90 }, + { 10, 17, 44, 51, 73, 90 }, + { 11, 15, 45, 49, 75, 92 }, + { 12, 16, 46, 50, 75, 92 }, + { 13, 17, 47, 51, 75, 92 }, + { 14, 18, 48, 52, 75, 92 }, + { 1, 15, 35, 49, 70, 86 }, + { 2, 16, 36, 50, 70, 86 }, + { 3, 17, 37, 51, 70, 86 }, + { 4, 18, 38, 52, 70, 86 }, + { 1, 19, 35, 53, 72, 87 }, + { 2, 20, 36, 54, 72, 87 }, + { 4, 21, 38, 55, 72, 87 }, + { 1, 22, 35, 56, 74, 89 }, + { 3, 23, 37, 57, 74, 89 }, + { 4, 24, 38, 58, 74, 89 }, + { 1, 25, 35, 59, 76, 91 }, + { 3, 26, 37, 60, 76, 91 }, + { 4, 27, 38, 61, 76, 91 }, + { 1, 28, 35, 62, 78, 93 }, + { 2, 29, 36, 63, 78, 93 }, + { 4, 30, 38, 64, 78, 93 }, + { 1, 31, 35, 65, 80, 95 }, + { 2, 32, 36, 66, 80, 95 }, + { 3, 33, 37, 67, 80, 95 }, + { 4, 34, 38, 68, 80, 95 }, + { 1, 31, 35, 65, 80, 95 }, + { 2, 32, 36, 66, 80, 95 }, + { 3, 33, 37, 67, 80, 95 }, + { 4, 34, 38, 68, 80, 95 }, + { 5, 31, 39, 65, 82, 97 }, + { 6, 32, 40, 66, 82, 97 }, + { 7, 33, 41, 67, 82, 97 }, + { 8, 31, 42, 65, 84, 99 }, + { 9, 32, 43, 66, 84, 99 }, + { 10, 33, 44, 67, 84, 99 }, + { 11, 31, 45, 65, 85, 101 }, + { 12, 32, 46, 66, 85, 101 }, + { 13, 33, 47, 67, 85, 101 }, + { 14, 34, 48, 68, 85, 101 }, + { 11, 15, 45, 49, 75, 92 }, + { 12, 16, 46, 50, 75, 92 }, + { 13, 17, 47, 51, 75, 92 }, + { 14, 18, 48, 52, 75, 92 }, + { 11, 19, 45, 53, 77, 94 }, + { 12, 20, 46, 54, 77, 94 }, + { 14, 21, 48, 55, 77, 94 }, + { 11, 22, 45, 56, 79, 96 }, + { 13, 23, 47, 57, 79, 96 }, + { 14, 24, 48, 58, 79, 96 }, + { 11, 25, 45, 59, 81, 98 }, + { 13, 26, 47, 60, 81, 98 }, + { 14, 27, 48, 61, 81, 98 }, + { 11, 28, 45, 62, 83, 100 }, + { 12, 29, 46, 63, 83, 100 }, + { 14, 30, 48, 64, 83, 100 }, + { 11, 31, 45, 65, 85, 101 }, + { 12, 32, 46, 66, 85, 101 }, + { 13, 33, 47, 67, 85, 101 }, + { 14, 34, 48, 68, 85, 101 }, + { 1, 15, 35, 49, 70, 86 }, + { 1, 15, 35, 49, 70, 86 }, + { 5, 15, 39, 49, 71, 88 }, + { 6, 16, 40, 50, 71, 88 }, + { 8, 15, 42, 49, 73, 90 }, + { 10, 17, 44, 51, 73, 90 }, + { 11, 15, 45, 49, 75, 92 }, + { 14, 18, 48, 52, 75, 92 }, + { 11, 19, 45, 53, 77, 94 }, + { 14, 21, 48, 55, 77, 94 }, + { 11, 22, 45, 56, 79, 96 }, + { 14, 24, 48, 58, 79, 96 }, + { 11, 25, 45, 59, 81, 98 }, + { 13, 26, 47, 60, 81, 98 }, + { 11, 28, 45, 62, 83, 100 }, + { 12, 29, 46, 63, 83, 100 }, + { 11, 31, 45, 65, 85, 101 }, + { 1, 15, 35, 49, 70, 86 }, + { 1, 19, 35, 53, 72, 87 }, + { 2, 20, 36, 54, 72, 87 }, + { 1, 22, 35, 56, 74, 89 }, + { 3, 23, 37, 57, 74, 89 }, + { 1, 25, 35, 59, 76, 91 }, + { 4, 27, 38, 61, 76, 91 }, + { 1, 28, 35, 62, 78, 93 }, + { 4, 30, 38, 64, 78, 93 }, + { 1, 31, 35, 65, 80, 95 }, + { 4, 34, 38, 68, 80, 95 }, + { 5, 31, 39, 65, 82, 97 }, + { 7, 33, 41, 67, 82, 97 }, + { 8, 31, 42, 65, 84, 99 }, + { 9, 32, 43, 66, 84, 99 }, + { 11, 31, 45, 65, 85, 101 } + >> + ] +VDH == { 28, 29, 30, 62, 63, 64, 83, 84, 93, 94 } + +CXDH == + { << 69, 35, 31, 80, 24, 74, 10, 73, 42, 84 >>, + << 69, 35, 31, 80, 24, 74, 44, 84 >>, + << 69, 35, 31, 80, 24, 74, 73, 42, 84 >>, + << 69, 35, 31, 80, 58, 24, 74, 44, 84 >>, + << 69, 35, 31, 80, 58, 79, 22, 74, 44, 84 >>, + << 69, 35, 31, 80, 58, 79, 22, 74, 73, 42, 84 >>, + << 69, 35, 31, 80, 79, 22, 74, 44, 84 >>, + << 69, 35, 65, 11, 92, 61, 98, 7, 88, 54, 94 >>, + << 69, 35, 80, 24, 74, 44, 84 >>, + << 69, 35, 80, 24, 74, 73, 42, 84 >>, + << 69, 35, 80, 58, 79, 22, 74, 44, 84 >>, + << 69, 35, 80, 79, 22, 74, 44, 84 >>, + << 69, 49, 11, 92, 61, 98, 7, 88, 54, 94 >>, + << 69, 49, 45, 31, 80, 24, 74, 44, 84 >>, + << 69, 49, 92, 38, 80, 24, 74, 44, 84 >>, + << 69, 49, 92, 61, 98, 41, 7, 88, 54, 94 >>, + << 69, 49, 92, 61, 98, 7, 88, 54, 94 >> + } + ----------------------------------------------------------------------------- GraphName == IF "GRAPH" \in DOMAIN IOEnv THEN IOEnv.GRAPH ELSE "7" @@ -127,5 +257,6 @@ TestCase == CASE GraphName = "1" -> [g |-> G1, v |-> V1, cx |-> CX1] [] GraphName = "11" -> [g |-> G11, v |-> V11, cx |-> CX11] [] GraphName = "12" -> [g |-> G12, v |-> V12, cx |-> CX12] [] GraphName = "13" -> [g |-> G13, v |-> V13, cx |-> CX13] + [] GraphName = "DH" -> [g |-> GDH, v |-> VDH, cx |-> CXDH] =============================================================================