|
| 1 | +---------------------------- MODULE MCReachability ---------------------------- |
| 2 | +EXTENDS Naturals, Sequences, TLC |
| 3 | +(***************************************************************************) |
| 4 | +(* High-level specification of a state-graph explorer that does NOT *) |
| 5 | +(* enforce BFS ordering. The frontier S is a set and the next state *) |
| 6 | +(* to explore is chosen non-deterministically from S. *) |
| 7 | +(* *) |
| 8 | +(* The working phase (init / explore / process-successors) is determined *) |
| 9 | +(* entirely by the data variables: *) |
| 10 | +(* *) |
| 11 | +(* init phase: successors = {} /\ S \ C # {} *) |
| 12 | +(* explore phase: successors = {} /\ S \subseteq C *) |
| 13 | +(* each phase: successors # {} *) |
| 14 | +(* *) |
| 15 | +(* S \subseteq C is an invariant of the post-init phases (Each adds to *) |
| 16 | +(* both S and C when Constraint holds; Explore only removes from S), so *) |
| 17 | +(* S \ C # {} vs S \subseteq C cleanly separates init from exploration. *) |
| 18 | +(* *) |
| 19 | +(* The only "control" variable is the boolean 'done', which records *) |
| 20 | +(* forced termination (violation or deadlock). Normal completion *) |
| 21 | +(* (frontier exhausted) needs no flag: S = {} /\ successors = {} simply *) |
| 22 | +(* disables every action. *) |
| 23 | +(***************************************************************************) |
| 24 | + |
| 25 | +(***************************************************************************) |
| 26 | +(* A (state) graph G is a directed graph represented by a record with *) |
| 27 | +(* 'states', 'initials', and 'actions' components. *) |
| 28 | +(* *) |
| 29 | +(* The CommunityModules Graphs.tla module is not used here because its *) |
| 30 | +(* representation [node, edge] differs from ours: we use an adjacency *) |
| 31 | +(* function (actions \in [states -> SUBSET states]) rather than an *) |
| 32 | +(* explicit edge set (edge \subseteq node \X node), and carry a *) |
| 33 | +(* distinguished 'initials' component that Graphs.tla does not model. *) |
| 34 | +(***************************************************************************) |
| 35 | +IsGraph(G) == /\ {"states", "initials", "actions"} = DOMAIN G |
| 36 | + /\ G.actions \in [G.states -> SUBSET G.states] |
| 37 | + /\ G.initials \subseteq G.states |
| 38 | + |
| 39 | +(***************************************************************************) |
| 40 | +(* Successor states of s, excluding self-loops. *) |
| 41 | +(***************************************************************************) |
| 42 | +SuccessorsOf(s, SG) == {t \in SG.actions[s] : t # s} |
| 43 | + |
| 44 | +(***************************************************************************) |
| 45 | +(* The predecessor of v in a spanning tree t (a set of *) |
| 46 | +(* <<predecessor, successor>> pairs) is the first element of the *) |
| 47 | +(* unique pair whose second element equals v. *) |
| 48 | +(***************************************************************************) |
| 49 | +Predecessor(t, v) == (CHOOSE pair \in t : pair[2] = v)[1] |
| 50 | + |
| 51 | +CONSTANT StateGraph, ViolationStates, |
| 52 | + Constraint(_, _) \* Constraint(s,l) iff state s may be explored at BFS level l; |
| 53 | + \* successors with FALSE are not added to S or C (but are |
| 54 | + \* still recorded in T and in L). |
| 55 | + |
| 56 | +ASSUME /\ IsGraph(StateGraph) |
| 57 | + /\ ViolationStates \subseteq StateGraph.states |
| 58 | + /\ \A s \in StateGraph.states, l \in Nat : Constraint(s, l) \in BOOLEAN |
| 59 | + |
| 60 | +VARIABLES S, \* Frontier: set of states yet to explore |
| 61 | + C, \* Set of visited states |
| 62 | + successors, \* Subset of Nat \X StateGraph.states: pairs <<lvl,t>> still to |
| 63 | + \* process for the current Explore step (same lvl for all). |
| 64 | + done, \* TRUE after violation or deadlock detected |
| 65 | + T, \* Set of <<predecessor, successor>> pairs (spanning tree) |
| 66 | + counterexample, \* Path from initial state to violation/deadlock state |
| 67 | + L \* BFS level of each state that has been assigned a level |
| 68 | + |
| 69 | +vars == <<S, C, successors, done, T, counterexample, L>> |
| 70 | + |
| 71 | +Init == /\ S = StateGraph.initials |
| 72 | + /\ C = {} |
| 73 | + /\ successors = {} |
| 74 | + /\ done = FALSE |
| 75 | + /\ T = {} |
| 76 | + /\ counterexample = <<>> |
| 77 | + /\ L = [s \in {} |-> 0] |
| 78 | + |
| 79 | +--------------------------------------------------------------------------- |
| 80 | + |
| 81 | +(***************************************************************************) |
| 82 | +(* Check an initial state for a safety violation. *) |
| 83 | +(***************************************************************************) |
| 84 | +InitCheck == |
| 85 | + /\ ~done |
| 86 | + /\ successors = {} |
| 87 | + /\ \E s \in S \ C : |
| 88 | + /\ C' = C \cup {s} |
| 89 | + /\ L' = (s :> 0) @@ L |
| 90 | + /\ done' = (s \in ViolationStates) |
| 91 | + /\ counterexample' = IF s \in ViolationStates |
| 92 | + THEN <<s>> ELSE counterexample |
| 93 | + /\ UNCHANGED <<S, successors, T>> |
| 94 | + |
| 95 | +--------------------------------------------------------------------------- |
| 96 | + |
| 97 | +(***************************************************************************) |
| 98 | +(* Pick any state from the frontier S for exploration. The next state *) |
| 99 | +(* is chosen non-deterministically (\E s \in S), so no ordering is *) |
| 100 | +(* imposed on the exploration. The predecessor pairs for all new *) |
| 101 | +(* successors are added to T here. *) |
| 102 | +(***************************************************************************) |
| 103 | +Explore == |
| 104 | + /\ ~done |
| 105 | + /\ successors = {} |
| 106 | + /\ S \subseteq C |
| 107 | + /\ S # {} |
| 108 | + /\ \E s \in S : |
| 109 | + LET succs == SuccessorsOf(s, StateGraph) \ C |
| 110 | + lvl == L[s] + 1 |
| 111 | + IN /\ S' = S \ {s} |
| 112 | + /\ successors' = {<<lvl, t>> : t \in succs} |
| 113 | + /\ T' = T \cup {<<s, t>> : t \in succs} |
| 114 | + /\ done' = (SuccessorsOf(s, StateGraph) = {}) |
| 115 | + /\ counterexample' = IF SuccessorsOf(s, StateGraph) = {} |
| 116 | + THEN <<s>> ELSE counterexample |
| 117 | + /\ UNCHANGED <<C, L>> |
| 118 | + |
| 119 | +--------------------------------------------------------------------------- |
| 120 | + |
| 121 | +(***************************************************************************) |
| 122 | +(* Process one successor: mark visited, add to frontier, check violation. *) |
| 123 | +(***************************************************************************) |
| 124 | +Each == |
| 125 | + /\ ~done |
| 126 | + /\ successors # {} |
| 127 | + /\ \E succ \in successors : |
| 128 | + /\ successors' = successors \ {succ} |
| 129 | + /\ IF Constraint(succ[2], succ[1]) |
| 130 | + THEN /\ C' = C \cup {succ[2]} |
| 131 | + /\ S' = S \cup {succ[2]} |
| 132 | + ELSE UNCHANGED <<C, S>> |
| 133 | + /\ L' = (succ[2] :> succ[1]) @@ L |
| 134 | + /\ done' = (succ[2] \in ViolationStates) |
| 135 | + /\ counterexample' = IF succ[2] \in ViolationStates |
| 136 | + THEN <<succ[2]>> ELSE counterexample |
| 137 | + /\ UNCHANGED T |
| 138 | + |
| 139 | +--------------------------------------------------------------------------- |
| 140 | + |
| 141 | +(***************************************************************************) |
| 142 | +(* Trace reconstruction: walk backward through T, prepending *) |
| 143 | +(* predecessors to the counterexample until an initial state is reached. *) |
| 144 | +(***************************************************************************) |
| 145 | +Trc == |
| 146 | + /\ done |
| 147 | + /\ counterexample # <<>> |
| 148 | + /\ Head(counterexample) \notin StateGraph.initials |
| 149 | + /\ counterexample' = <<Predecessor(T, Head(counterexample))>> |
| 150 | + \o counterexample |
| 151 | + /\ UNCHANGED <<S, C, successors, done, T, L>> |
| 152 | + |
| 153 | +--------------------------------------------------------------------------- |
| 154 | + |
| 155 | +Terminating == done /\ UNCHANGED vars |
| 156 | + |
| 157 | +Next == |
| 158 | + \/ InitCheck |
| 159 | + \/ Explore |
| 160 | + \/ Each |
| 161 | + \/ Trc |
| 162 | + \/ Terminating |
| 163 | + |
| 164 | +Spec == |
| 165 | + /\ Init /\ [][Next]_vars |
| 166 | + /\ WF_vars(Next) |
| 167 | + |
| 168 | +Termination == <>(done \/ (S = {} /\ successors = {})) |
| 169 | + |
| 170 | +(***************************************************************************) |
| 171 | +(* If violation states exist, the explorer eventually finds one and *) |
| 172 | +(* constructs a valid counterexample path from an initial state to it. *) |
| 173 | +(***************************************************************************) |
| 174 | +Live == ViolationStates # {} => |
| 175 | + <>[](/\ counterexample # <<>> |
| 176 | + /\ counterexample[Len(counterexample)] \in ViolationStates |
| 177 | + /\ counterexample[1] \in StateGraph.initials) |
| 178 | + |
| 179 | +============================================================================= |
0 commit comments