---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Reachable.tla
---
------------------------------- MODULE Reachable -------------------------------
(***************************************************************************)
(* This module specifies an algorithm for computing the set of nodes in a *)
(* directed graph that are reachable from a given node called Root. The *)
(* algorithm is due to Jayadev Misra. It is, to my knowledge, a new *)
(* variant of a fairly obvious breadth-first search for reachable nodes. *)
(* I find this algorithm interesting because it is easier to implement *)
(* using multiple processors than the obvious algorithm. Module ParReach *)
(* describes such an implementation. You may want to read it after *)
(* reading this module. *)
(* *)
(* Module ReachableProofs contains a TLA+ proof of the algorithm's safety *)
(* property--that is, partial correctness, which means that if the *)
(* algorithm terminates then it produces the correct answer. That proof *)
(* has been checked by TLAPS, the TLA+ proof system. The proof is based *)
(* on ideas from an informal correctness proof by Misra. *)
(* *)
(* In this module, reachability is expressed in terms of the operator *)
(* ReachableFrom, where ReachableFrom(S) is the set of nodes reachable *)
(* from the nodes in the set S of nodes. This operator is defined in *)
(* module Reachability. That module describes a directed graph in terms *)
(* of the constants Nodes and Succ, where Nodes is the set of nodes and *)
(* Succ is a function with domain Nodes such that Succ[m] is the set of *)
(* all nodes n such that there is an edge from m to n. If you are not *)
(* familiar with directed graphs, you should read at least the opening *)
(* comments in module Reachability. *)
(***************************************************************************)
EXTENDS Reachability, Integers, FiniteSets
CONSTANT Root
ASSUME RootAssump == Root \in Nodes
(***************************************************************************)
(* Reachable is defined to be the set of notes reachable from Root. The *)
(* purpose of the algorithm is to compute Reachable. *)
(***************************************************************************)
Reachable == ReachableFrom({Root})
--------------------------------------------------------------------------------
(***************************************************************************
The obvious algorithm for computing Reachable({Root}) is as follows.
There are two variables which, following Misra, we call `marked' and
vroot. Each variable holds a set of nodes that are reachable from
Root. Initially, marked = {} and vroot = {Root}. While vroot is
non-empty, the obvious algorithm removed an arbitrary node v from
vroot, adds v to `marked', and adds to vroot all nodes in Succ[v] that
are not in `marked'. The algorithm terminates when vroot is empty,
which will eventually be the case if and only if Reachable({Root}) is a
finite set. When it terminates, `marked' equals Reachable({Root}).
In the obvious algorithm, `marked' and vroot are always disjoint sets of
nodes. Misra's variant differs in that `marked' and vroot are not
necessarily disjoint. While vroot is nonempty, it chooses an arbitrary
node and does the following:
IF v is not in in `marked'
THEN it performs the same action as the obvious algorithm except:
(1) it doesn't remove v from vroot, and
(2) it adds all nodes in Succ[v] to vroot, not just the ones
not in `marked'.
ELSE it removes v from vroot
Here is the algorithm's PlusCal code.
--fair algorithm Reachable {
variables marked = {}, vroot = {Root};
{ a: while (vroot /= {})
{ with (v \in vroot)
{ if (v \notin marked)
{ marked := marked \cup {v};
vroot := vroot \cup Succ[v] }
else { vroot := vroot \ {v} }
}
}
}
}
***************************************************************************)
\* BEGIN TRANSLATION Here is the TLA+ translation of the PlusCal code.
VARIABLES marked, vroot, pc
vars == << marked, vroot, pc >>
Init == (* Global variables *)
/\ marked = {}
/\ vroot = {Root}
/\ pc = "a"
a ==
/\ pc = "a"
/\ IF vroot /= {}
THEN
/\ \E v \in vroot:
IF v \notin marked
THEN
/\ marked' = (marked \union {v})
/\ vroot' = (vroot \union Succ[v])
ELSE
/\ vroot' = vroot \ {v}
/\ UNCHANGED marked
/\ pc' = "a"
ELSE
/\ pc' = "Done"
/\ UNCHANGED << marked, vroot >>
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == a
\/ Terminating
Spec ==
/\ Init /\ [][Next]_vars
/\ WF_vars(Next)
Termination == <>(pc = "Done")
\* END TRANSLATION
--------------------------------------------------------------------------------
(***************************************************************************)
(* Partial correctness is based on the invariance of the following four *)
(* state predicates. I have sketched very informal proofs of their *)
(* invariance, as well of proofs of the the two theorems that assert *)
(* correctness of the algorithm. The module ReachableProofs contains *)
(* rigorous, TLAPS checked TLA+ proofs of all except the last theorem. *)
(* The last theorem asserts termination, which is a liveness property, and *)
(* TLAPS is not yet capable of proving liveness properties. *)
(***************************************************************************)
TypeOK ==
/\ marked \in SUBSET Nodes
/\ vroot \in SUBSET Nodes
/\ pc \in {"a", "Done"}
/\ (pc = "Done") => (vroot = {})
(*************************************************************************)
(* The invariance of TypeOK is obvious. (I decided to make the obvious *)
(* fact that pc equals "Done" only if vroot is empty part of the *)
(* type-correctness invariant.) *)
(*************************************************************************)
Inv1 ==
/\ TypeOK
/\ \A n \in marked: Succ[n] \subseteq (marked \union vroot)
(*************************************************************************)
(* The second conjunct of Inv1 is invariant because each element of *)
(* Succ[n] is added to vroot when n is added to `marked', and it remains *)
(* in vroot at least until it's added to `marked'. I made TypeOK a *)
(* conjunct of Inv1 to make Inv1 an inductive invariant, which made the *)
(* TLA+ proof of its invariance a tiny bit easier to read. *)
(*************************************************************************)
Inv2 == (marked \union ReachableFrom(vroot)) = ReachableFrom(marked \union vroot)
(*************************************************************************)
(* Since ReachableFrom(marked \cup vroot) is the union of *)
(* ReachableFrom(marked) and ReachableFrom(vroot), to prove that Inv2 is *)
(* invariant we must show ReachableFrom(marked) is a subset of *)
(* marked \cup ReachabledFrom(vroot). For this, we assume that m is in *)
(* ReachableFrom(marked) and show that it either is in `marked' or is *)
(* reachable from a node in vroot. *)
(* *)
(* Since m is in ReachableFrom(marked), there is a path with nodes *)
(* p_1, p_2, ... , p_j such that p_1 is in `marked' and p_j = m. If *)
(* all the p_i are in `marked', then m is in `marked' and we're done. *)
(* Otherwise, choose i such that p_1, ... , p_i are in `marked', but *)
(* p_(i+1) isn't in `marked'. Then p_(i+1) is in succ[p_i], which by *)
(* Inv1 implies that it's in marked \cup vroot. Since it isn't in *)
(* `marked', it must be in vroot. The path with nodes *)
(* p_(i+1), ... , p_j shows that p_j, which equals m, is in *)
(* ReachableFrom(vroot). This completes the proof that m is in `marked' *)
(* or ReachableFrom(vroot). *)
(*************************************************************************)
Inv3 == Reachable = marked \union ReachableFrom(vroot)
(*************************************************************************)
(* For convenience, let R equal marked \cup ReachableFrom(vroot). In *)
(* the initial state, marked = {} and vroot = {Root}, so R equals *)
(* Reachable and Inv3 is true. We have to show that each action `a' *)
(* step leaves R unchanged. There are two cases: *)
(* *)
(* Case1: The `a' step adds an element v of vroot to `marked' and adds *)
(* to vroot the nodes in Succ[v], which are all in ReachableFrom(vroot). *)
(* Since v itself is also in ReachableFrom(vroot), the step leaves R *)
(* unchanged. *)
(* *)
(* Case 2: The `a' step removes from vroot an element v of `marked'. *)
(* Since Inv1 implies that every node in Succ[v] is in vroot, the only *)
(* element that this step removes from ReachableFrom(vroot) is v, which *)
(* the step adds to `marked'. Hence R is unchanged. *)
(*************************************************************************)
(***************************************************************************)
(* It is straightforward to use TLC to check that Inv1-Inv3 are invariants *)
(* of the algorithm for small graphs. *)
(***************************************************************************)
(***************************************************************************)
(* Partial correctness of the algorithm means that if it has terminated, *)
(* then `marked' equals Reachable. The algorithm has terminated when pc *)
(* equals "Done", so this theorem asserts partial correctness. *)
(***************************************************************************)
PartialCorrectness == (pc = "Done") => (marked = Reachable)
THEOREM Spec => []PartialCorrectness
(*************************************************************************)
(* TypeOK implies (pc = "Done") => (vroot = {}). Since, *)
(* ReachableFrom({}) equals {}, Inv3 implies *)
(* (vroot = {}) => (marked = Reachable). Hence the theorem follows from *)
(* the invariance of TypeOK and Inv3. *)
(*************************************************************************)
(***************************************************************************)
(* The following theorem asserts that if the set of nodes reachable from *)
(* Root is finite, then the algorithm eventually terminates. Of course, *)
(* this liveness property can be true only because Spec implies weak *)
(* fairness of Next, which equals action `a'. *)
(***************************************************************************)
THEOREM ASSUME IsFiniteSet(Reachable)
PROVE Spec => <>(pc = "Done")
(*************************************************************************)
(* To prove the theorem, we assume a behavior satisfies Spec and prove *)
(* that it satisfies <>(pc = "Done"). If pc = "a" and vroot = {}, then *)
(* an `a' step sets pc to "Done". Since invariance of TypeOK implies *)
(* [](pc \in {"a", "Done"}), weak fairness of `a' implies that to prove *)
(* <>(pc = "Done"), it suffices to prove <>(vroot = {}). *)
(* *)
(* We prove <>(root = {}) by contradiction. We assume it's false, which *)
(* means that [](root /= {}) is true, and obtain a contradiction. From *)
(* []TypeOK, we infer that [](root /= {}) implies [](pc = "a"). By weak *)
(* fairness of action `a', [](root /= {}) implies that there are an *)
(* infinite number of `a' steps. The assumption that Reachable is *)
(* finite and []Inv3 imply that `marked' and vroot are always finite. *)
(* Since vroot is always finite and nonempty, from any state there can *)
(* be only a finite number of `a' steps that remove an element from *)
(* vroot until there is an `a' step that adds a new element to `marked'. *)
(* Since there are an infinite number of `a' steps, there must be an *)
(* infinite number of steps that add new elements to `marked'. This is *)
(* impossible because `marked' is a finite set. Hence, we have the *)
(* required contradiction. *)
(*************************************************************************)
(**************************************************************************)
(* TLC can quickly check these two theorems on models containing a half *)
(* dozen nodes. *)
(**************************************************************************)
================================================================================
\* Modification History
\* Last modified Tue Aug 27 14:46:36 PDT 2019 by loki
\* Last modified Wed Apr 17 12:21:22 PDT 2019 by lamport
\* Created Thu Apr 04 10:11:51 PDT 2019 by lamport