Skip to content

TLCMC: non-strict BFS, BFS level tracking, state constraints, and refinement to MCReachability. #204

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
lemmy wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

TLCMC: non-strict BFS, BFS level tracking, state constraints, and refinement to MCReachability. #204

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
179 changes: 179 additions & 0 deletions specifications/TLC/MCReachability.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 *)
(* <<predecessor, successor>> 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 <<lvl,t>> still to
\* process for the current Explore step (same lvl for all).
done, \* TRUE after violation or deadlock detected
T, \* Set of <<predecessor, successor>> 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 == <<S, C, successors, done, T, counterexample, L>>

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 <<s>> ELSE counterexample
/\ UNCHANGED <<S, successors, T>>

---------------------------------------------------------------------------

(***************************************************************************)
(* 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' = {<<lvl, t>> : t \in succs}
/\ T' = T \cup {<<s, t>> : t \in succs}
/\ done' = (SuccessorsOf(s, StateGraph) = {})
/\ counterexample' = IF SuccessorsOf(s, StateGraph) = {}
THEN <<s>> ELSE counterexample
/\ UNCHANGED <<C, L>>

---------------------------------------------------------------------------

(***************************************************************************)
(* 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 <<C, S>>
/\ L' = (succ[2] :> succ[1]) @@ L
/\ done' = (succ[2] \in ViolationStates)
/\ counterexample' = IF succ[2] \in ViolationStates
THEN <<succ[2]>> 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' = <<Predecessor(T, Head(counterexample))>>
\o counterexample
/\ UNCHANGED <<S, C, successors, done, T, L>>

---------------------------------------------------------------------------

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)

=============================================================================
118 changes: 118 additions & 0 deletions specifications/TLC/StateGraphs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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]

=============================================================================
Loading
Loading