Theory SetMark
section ‹Marking Using a Set›
theory SetMark
imports Graph DataRefinementIBP.DataRefinement
begin
text‹
We construct in this theory a diagram which computes all reachable nodes
from a given root node in a graph. The graph is defined in the theory
Graph and is given by a relation $next$ on the nodes of the graph.
The diagram has only three ordered situation
($\mathit{init} > \mathit{loop} > \mathit{final}$). The termination
variant is a pair of a situation and a natural number with the lexicographic
ordering. The idea of this ordering is that we can go from a bigger situation
to a smaller one, however if we stay in the same situation the second
component of the variant must decrease.
The idea of the algorithm is that it starts with a set $X$ containing the
root element and the root is marked. As long as $X$ is not empty, if $x\in X$
and $y$ is an unmarked sucessor of $x$ we add $y$ to $X$. If $x\in X$ has
no unmarked sucessors it is removed from $X$.
The algorithm terminates when $X$ is empty.
›