TLCMC.tla

------------------------------- MODULE TLCMC -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC

(***************************************************************************)
(* Convertes the given Sequence seq into a Set of all the                  *) 
(* Sequence's elements. In other words, the image of the function          *)
(* that seq is.                                                            *)
(***************************************************************************)
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.                                               *)
(***************************************************************************)
SetToSeqs(set, Filter(_)) == UNION {{perm \in [1..Cardinality(set) -> set]: 
                            \* A filter applied on each permutation
                            \* generated by [S -> T]       
                            Filter(perm)}}

(***************************************************************************)
(* 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.                                                        *)
(***************************************************************************)
SetToDistSeqs(set) == SetToSeqs(set, 
                    LAMBDA p: Cardinality(SeqToSet(p)) = Cardinality(set))

(***************************************************************************)
(* A (state) graph G is a directed cyclic graph.                           *)
(*                                                                         *)
(* A graph G is represented by a record with 'states' and 'actions'        *)
(* components, where G.states is the set of states and G.actions[s] is the *)
(* set of transitions of s -- that is, all states t such that there is an  *)
(* action (arc) from s to t.                                               *)
(***************************************************************************)
IsGraph(G) == /\ {"states", "initials", "actions"} = DOMAIN G
              /\ G.actions \in [G.states -> SUBSET G.states]
              /\ G.initials \subseteq G.states

(***************************************************************************)
(* A Set of successor states state.                                        *)
(***************************************************************************)
SuccessorsOf(state, SG) == {successor \in SG.actions[state]:
                            successor \notin {state}}

(***************************************************************************)
(* The predecessor of v in a forest t is the first element of the pair     *)
(* <<predecessor, successor>> nested in a sequence of pairs. In an actual  *)
(* implementation such as TLC, pair[1] is rather an index into t than      *)
(* an id of an actual state.                                               *)
(***************************************************************************)
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.
         Counterexamples    \* Set of known counterexample sequences for the
                            \* current graph/violation pair.

(***************************************************************************)
(* 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 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 = {},
              \* The state currently being explored in scsr
              state = null,
              \* The set of state's successor states              
              successors = {},
              \* Counter
              i = 1,
              \* A path from some initial state ending in a
              \* state in violation.
              counterexample = <<>>,
              \* A sequence of pairs such that a pair is a
              \* sequence <<predecessor, successors>>.
              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
          of the second while loop. However, we then
          either check all states twice or add unchecked
          states to S. *)
       init: while (i \leq Len(S)) {
             \*  Bug in thesis: 
             \*state := Head(S);
             state := S[i]; 
             \* state is now fully explored,
             \* thus exclude it from any
             \* further exploration if graph
             \* exploration visits it again
             \* due to a cycle. 
             C := C \cup {state};
             L := (state :> 0) @@ L;
             i := i + 1;
             if (state \in ViolationStates) {
                     counterexample := <<state>>;
                     \* Terminate model checking
                     goto trc;
             };
       };
       \* Assert that all initial states have been explored.
       initPost: assert C = SeqToSet(S);

       (* Explores all successor states 
          until no new successors are found
          or a violation has been detected. *)
       scsr: while (Len(S) # 0) {
            \* 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;
            if (SuccessorsOf(state, StateGraph) = {}) {
                \* Iff there exists no successor besides
                \* the self-loop, the system has reached
                \* a deadlock state.
                counterexample := <<state>>;
                goto trc;
            };
            each: while (successors # {}) {
                with (succ \in successors) {
                     \* Exclude succ in this while loop.
                     successors := successors \ {succ};

                     if (Constraint(succ, L[state] + 1)) {
                         \* Mark successor globally visited.
                         C := C \cup {succ}; S := S \o <<succ>>;
                         \* 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 << <<state,succ>> >>;
                         L  := (succ :> (L[state] + 1)) @@ L;
                     };
                     
                     
                     \* Check state for violation of a
                     \* safety property (simplified 
                     \* to a check of set membership.
                     if (succ \in ViolationStates) {
                       counterexample := <<state, succ>>;
                       \* Terminate model checking
                       goto trc;
                     };
                };
            };
       };
       (* Model Checking terminated without finding
          a violation (or all violations were unreachable /
          pruned by Constraint). *)
       assert S = <<>>;
       goto Done;
       
       (* Create a counterexample, that is a path
          from some initial state to a state in
          ViolationStates. In the Java implementation
          of TLC, the path is a path of fingerprints. 
          Thus, a second, guided state exploration
          resolves fingerprints to actual states. *)
       trc : while (TRUE) {
                if (Head(counterexample) \notin StateGraph.initials) {
                   counterexample := <<Predecessor(T, Head(counterexample))>> \o counterexample;
                } else {
                   assert counterexample # <<>>;
                   goto Done;
                };
       };
    }        
}
 ***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "f48dc6da")
VARIABLES pc, S, C, state, successors, i, counterexample, T, L

vars == << pc, S, C, state, successors, i, counterexample, T, L >>

Init == (* Global variables *)
        /\ S \in SetOfAllPermutationsOfInitials(StateGraph)
        /\ C = {}
        /\ state = null
        /\ successors = {}
        /\ 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' = <<state'>>
                              /\ pc' = "trc"
                         ELSE /\ pc' = "init"
                              /\ UNCHANGED counterexample
              ELSE /\ pc' = "initPost"
                   /\ UNCHANGED << C, state, i, counterexample, L >>
        /\ UNCHANGED << S, successors, T >>

initPost == /\ pc = "initPost"
            /\ Assert(C = SeqToSet(S), 
                      "Failure of assertion at line 148, column 18.")
            /\ pc' = "scsr"
            /\ UNCHANGED << S, C, state, successors, i, counterexample, T, L >>

scsr == /\ pc = "scsr"
        /\ IF Len(S) # 0
              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' = <<state'>>
                              /\ pc' = "trc"
                         ELSE /\ pc' = "each"
                              /\ UNCHANGED counterexample
              ELSE /\ Assert(S = <<>>, 
                             "Failure of assertion at line 204, column 8.")
                   /\ pc' = "Done"
                   /\ UNCHANGED << S, state, successors, counterexample >>
        /\ UNCHANGED << C, i, T, L >>

each == /\ pc = "each"
        /\ IF successors # {}
              THEN /\ \E succ \in successors:
                        /\ successors' = successors \ {succ}
                        /\ IF Constraint(succ, L[state] + 1)
                              THEN /\ C' = (C \cup {succ})
                                   /\ S' = S \o <<succ>>
                                   /\ T' = T \o << <<state,succ>> >>
                                   /\ L' = (succ :> (L[state] + 1)) @@ L
                              ELSE /\ TRUE
                                   /\ UNCHANGED << S, C, T, L >>
                        /\ IF succ \in ViolationStates
                              THEN /\ counterexample' = <<state, succ>>
                                   /\ pc' = "trc"
                              ELSE /\ pc' = "each"
                                   /\ UNCHANGED counterexample
              ELSE /\ pc' = "scsr"
                   /\ UNCHANGED << S, C, successors, counterexample, T, L >>
        /\ UNCHANGED << state, i >>

trc == /\ pc = "trc"
       /\ IF Head(counterexample) \notin StateGraph.initials
             THEN /\ counterexample' = <<Predecessor(T, Head(counterexample))>> \o counterexample
                  /\ pc' = "trc"
             ELSE /\ Assert(counterexample # <<>>, 
                            "Failure of assertion at line 217, column 20.")
                  /\ pc' = "Done"
                  /\ UNCHANGED counterexample
       /\ UNCHANGED << S, C, state, successors, i, T, L >>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == init \/ initPost \/ scsr \/ each \/ trc
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION 

\* 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)

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

(***************************************************************************)
(* 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 {<<state, succ>> : 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  {<<lvl, s, state>> : s \in successors}

Refinement == MCR!Spec

=============================================================================