Refactoring to increase understandability of exploration (in line with

documentation)

doc/exploration/explore.tex

@@ -10,26 +10,30 @@
 We globally assume a set of labels $A$.
 
 \medskip\noindent 
-A state space is a tuple $\tupof{S,{\ra},{\up},\Tdepth}$ with
+A state space is a tuple $\cS=\tupof{S,\iota,{\ra},{\up},\Tdepth}$ with
 \begin{itemize}
 \item $S$ a set of states;
+\item $\iota\in S$ the initial state;
 \item ${\ra}\subseteq S\times A\times S$ a transition relation;
 \item ${\up}\subseteq S$ a termination predicate;
 \item ${\Tdepth}:S\to \natN$ a \emph{transient depth} (or \emph{transience}) function.
 \end{itemize}
 %
-State $s\in S$ is called \emph{final} if $p\up$, \emph{transient} (denoted $\Trnt(s)$) if $\Tdepth(s)>0$ and \emph{stable} (denoted $\Stable(s)$) if $\Tdepth(s)=0$.
-
-\medskip\noindent State spaces are generated from a \emph{pseudo-state spaces}.
+State $s\in S$ is called \emph{final} if $p\up$, \emph{transient} (denoted $\Trnt(s)$) if $\Tdepth(s)>0$ and \emph{stable} (denoted $\Stable(s)$) if $\Tdepth(s)=0$. There is a derived \emph{transaction relation}:
+%
+\[ s\ttrans s' \enspace\iffdef\enspace \Stable(s) \wedge \Stable(s') \wedge s\trans{}^+ s' \enspace. \]
+%
+State spaces are generated from a \emph{pseudo-state spaces}.
 
 \medskip\noindent
-A pseudo-state space is a tuple $\tupof{P,{\mapsto},{\goesto},{\up},\Tdepth}$ with
+A pseudo-state space is a tuple $\cP=\tupof{P,\iota,{\mapsto},{\goesto},{\up},\Tdepth}$ with
 \begin{itemize}
 \item $P$ a finite set of pseudo-states;
+\item $\iota\in P$ the initial pseudo-state;
 \item ${\step{}}\subseteq P\times A\times P$ a step relation;
-\item ${\goesto}: P\times P$ a partial, acyclic evolution relation;
+\item ${\goesto}: P\times P$ an acyclic evolution relation;
 \item ${\up} \subseteq P$ a termination predicate;
-\item ${\Tdepth}:S\to \natN$ a \emph{transient depth} function.
+\item ${\Tdepth}:P\to \natN$ a transient depth function.
 \end{itemize}
 %
 Pseudo-state $p\in P$ is called \emph{prime} (denoted $\Prime(p)$) if $p\ncomesfrom$, \emph{closed} (denoted $\Closed(p)$) if $p\ngoesto$ and \emph{open} (denoted $\Open(p)$) if it is not closed.
@@ -44,31 +48,63 @@
 \item Stepping cannot decrease transience; i.e., $p\step{}q$ implies $\Tdepth(q)\geq \Tdepth(p)$;
 \item Evolution cannot increase transience; i.e., $p\goesto q$ implies $\Tdepth(q)\leq \Tdepth(p)$.
 \end{itemize}
+%
 From now on, we only deal with well-formed pseudo-states spaces. The \emph{prime of} and \emph{closure of} a pseudo-state $p$ are defined as
+%
 \begin{align*}
 	\prm p & = q \quad \text{where $\Prime (q)$ and $q\goesto^* p$} \\
-	\cls p & = q \quad \text{where $\Closed(q)$ and $p\comesfrom^* q$} \enspace.
+	\cls p & = q \quad \text{where $p\goesto^* q$ and $\Closed(q)$} \enspace.
 \end{align*}
 %
-Note that these are well-defined because $P$ is finite and $\goesto$ is acyclic, deterministic and injective.
+Note that these are well-defined because $P$ is finite and $\goesto$ is acyclic, deterministic and injective (implying that it is a union of finite chains of pseudo-states). A pseudo-state space effectively represents a state space in which the states are $\goesto$-related sets of pseudo-states --- which, as remarked above, are actually chains. Rather than formalising the relation in this way, however, we let a state be represented by the initial element of such a chain, i.e., by the (unique) prime pseudo-state.
 
 \medskip\noindent
-A pseudo-state space $\tupof{P,{\mapsto},{\goesto},{\up},\Tdepth}$ gives rise to a state space $\tupof{S,\trans{},\up,\Tdepth_S}$ where
+Given a pseudo-state space $\cP$ as above, a \emph{configuration} is a $\goesto$-left-closed set $C\subseteq P$ of pseudo-states such that, moreover, $\iota\in C$ and if $p\comesfrom\:\step q$ then $p\in C$ implies $q\in C$. (It follows that $P$ is itself a configuration of $\cP$.) Given a configuration $C$, we define $\cS_C= \tupof{S_C,\iota_C,\trans{}_C, \up_C, \Tdepth_C}$ as follows:
 %
-\begin{itemize}
-\item $s\in S$ if $s$ is a closed pseudo-state; i.e., $S=\cls P$;
-\item $\cls p\trans a \cls{p'}$ for all $p\step a p'$; i.e., $s\trans a s'$ if $s\comesfrom^*\step a \goesto^* s'$;
-\item $\up$ remains unchanged (noting that $p\up$ implies $\Closed(p)$ and hence $p\in S$);
-\item $\Tdepth_S$ restricts $\Tdepth$ to $S$; i.e., $\Tdepth_S=\gensetof{(p,\Tdepth(p))}{p\in S}$.
-\end{itemize}
+\begin{align*}
+S_C & = \gensetof{\prm p}{p\in C} \\
+\iota_C & = \iota \\
+{\trans{}_C} & = \gensetof{(\prm p,a,q)}{p,q\in C, p\step a q} \\
+\up_C & = \gensetof{\prm p}{p\in C, p\up} \\
+\Tdepth_C & : p \mapsto \min \gensetof{\Tdepth(q)}{q\in C,p=\prm q} \enspace \text{for all $p\in S_C$} \enspace.
+\end{align*}
+%
+The notion of closedness and stability are also extended to configurations (so as to coincide with their counterparts for $S_C$):
+\begin{align*}
+\Closed_C & = \gensetof{\prm p}{p\in C, p\ngoesto} \\
+\Stable_C & = \gensetof{\prm p}{p\in C, \Tdepth(p)=0} \enspace.
+\end{align*}
 %
-Given a pseudo-state space $P$, a \emph{configuration} is a partial function $C:\cls P\pto P$. $C$ gives rise to a state space $\tupof{S_C,\trans{}_C,\up_C,\Tdepth_C}$ where
+We define some further auxiliary notions.
 %
 \begin{itemize}
-\item $S_C=\dom C$;
-\item For all $s,s'\in S_C$, $s\trans a s'$ if $C(s)\comesfrom^*\step a \goesto^* C(s')$;
-\item For all $s\in S_C$, $s\up_C$ if $C(s)\up$;
-\item For all $s\in S_C$, $\Tdepth_C(s)=\Tdepth(C(s))$.
-\end{itemize}
+\item $\Done_C(s)$ for $s\in S_C$ expresses that $s$ as well as all its discovered $\trans{}_C$-successors are closed, up to and including the first stable state. It is defined as the smallest set such that
+\[ \Done_C = \Closed_C\cap \bigl(\Stable_C \cup \gensetof{p\in S_C}{\forall p\trans{}_C q.\, q\in \Done_C}\bigr) \enspace.
+\]
+
+\item $\ETdepth_C(s)$ for $s\in S_C$ is the \emph{eventual transient depth} in $C$, meaning the minimum transient depth of $s$ and all its $\trans{}_C$-successors. It is defined by
+%
+\[ \ETdepth_C: p\mapsto \min\gensetof{\Tdepth(q)}{p\trans{}_C^* q} \text{ for all $p\in S_C$} \enspace. \]
+
+\item $\EStable_C(s)$ for $s\in S_C$ expresses that $s$ is \emph{eventually stable} in $C$, meaning that it or one of its discovered $\trans{}_C$-successors is stable (i.e., has transient depth 0). It is defined by
+%
+\[ \EStable_C=\gensetof{p\in S_C}{\ETdepth_C(p)=0} \enspace. \]
 
+\item $\Abs_C(s)$ for $s\in S_C$ expresses that $s$ is \emph{absent} in $C$, which is the case if it is done (all reachable stable states have been discovered) but not eventually stable (no reachable stable state has been discovered). It is defined by
+\[ \Abs_C=\Done_C\setminus \EStable_C \enspace. \]
+\end{itemize}
+%
+We want to construct $S_P$ incrementally by approaching $P$ through a sequence of configurations, starting with $\setof{\iota}$ and adding, at each iteration, an evolution $p\goesto p'$ with $p\in C$ and $p'\notin C$. The latter is defined by 
+\[ C\oplus(p\goesto p') = C\cup \setof{p'} \cup \gensetof{q}{p\step a q} \enspace. \]
+Incremental construction means that, if $D=C\oplus(p\goesto p')$, all components of $S_D$ can be constructed from $S_C$ and $\cP$. Indeed, we have
+%
+\begin{align*}
+\trans{}_D & = {\trans{}_C} \cup\gensetof{(\prm p,a,q)}{p\step a q} \\
+\up_D & = \up_C \cup \gensetof{p'}{p'\up} \\
+\Tdepth_D & : s\mapsto\begin{cases}
+\Tdepth(p') & \text{if $s=\prm p$} \\
+\Tdepth(q) & \text{if $s=q\notin S_C$} \\
+\Tdepth_C(s) & \text{otherwise.}
+\end{cases}
+\end{align*}
 \end{document}

doc/exploration/preamble.sty

@@ -8,8 +8,10 @@
 
 \newcommand{\GROOVE}{GROOVE}
 
-\newcommand{\cls}[1]{{#1}\mskip1mu\triangleright}
-\newcommand{\prm}[1]{\triangleleft\mskip1mu{#1}}
+% Closure of a pseudo-state
+\newcommand{\cls}[1]{{#1}{\triangleright}}
+% Prime of a pseudo-state
+\newcommand{\prm}[1]{{\triangleleft}\mskip-2mu{#1}}
 
 \newcommand{\dom}{\mathop{\mathrm{dom}}}
 
@@ -18,27 +20,39 @@
 \newcommand{\Open}{\ensuremath{\mathit{open}}}
 \newcommand{\Closed}{\ensuremath{\mathit{closed}}}
 \newcommand{\Trnt}{\ensuremath{\mathit{trnt}}}
+% Absence
 \newcommand{\Abs}{\ensuremath{\mathit{abs}}}
+% Stability
 \newcommand{\Stable}{\ensuremath{\mathit{stable}}}
-\newcommand{\Tdepth}{\ensuremath{\mathit{tdp}}}
+% Eventual stability
+\newcommand{\EStable}{\Stable^\diamond}
+% Transient depth
+\newcommand{\Tdepth}{\ensuremath{\mathit{trdp}}}
+% Eventual transient depth
+\newcommand{\ETdepth}{\Tdepth^\diamond}
 
 \newcommand{\cC}{\mathcal{C}}
+\newcommand{\cP}{\mathcal{P}}
+\newcommand{\cS}{\mathcal{S}}
+
 \newcommand{\natN}{\mathbb{N}}
 
 \newcommand{\setof}[1]{\{{#1}\}}
 \newcommand{\gensetof}[2]{\setof{{#1}\mid{#2}}}
 \newcommand{\tupof}[1]{\langle{#1}\rangle}
 \newcommand{\iffdef}{:\Leftrightarrow}
+% Partial function
+\newcommand{\pto}{\hookrightarrow}
 
 % Special arrows
-\newcommand{\pto}{\hookrightarrow}
+
 \newcommand{\goesto}{\rightarrowtail}
 \newcommand{\ngoesto}{\arrownot\rightarrowtail}
+
 \newcommand{\comesfrom}{\leftarrowtail}
 \newcommand{\ncomesfrom}{\arrownot\leftarrowtail}
 \newcommand{\ra}{\rightarrow}
 \newcommand{\up}{{\uparrow}}
-\newcommand{\Up}{{\Uparrow}}
 
 % Typeset the label of an extensible arrow
 \newcommand{\xlabel}[1]{\smash{\mathchoice
@@ -49,16 +63,21 @@
 }}
 % Prepend a negation to an extensible arrow
 \newcommand{\xarrownot}{\mathrel{\arrownot-}\mskip-7mu}
+
 % single-arrow transition
 \newcommand{\trans}[1]{\xrightarrow{\xlabel{#1}}}
 % negative single-arrow transition
 \newcommand{\ntrans}[1]{\mathrel{\xarrownot\trans{#1}}}
 
 % mapsto-like transition
 \newcommand{\step}[1]{\mapstochar\xrightarrow{\xlabel{#1}}}
-% negative mapsto-like transition
+% negated mapsto-like transition
 \newcommand{\nstep}[1]{\mapstochar\joinrel\xarrownot\xrightarrow{\xlabel{#1}}}
 
+% Transactional transition
+\newcommand{\ttrans}{\twoheadrightarrow}
+% Negated transactional transition
+\newcommand{\nttrans}{\arrownot\ttrans}
 
 %%%% Recapture the mapstochar, which is set to undefined by MnSymbol
 \usepackage{trimclip}

src/main/java/nl/utwente/groove/lts/AbstractGraphState.java

@@ -245,7 +245,7 @@ public boolean setClosed(boolean complete) {
             //            setStatus(Flag.INTERNAL, getActualFrame().isInternal());
             //            setStatus(Flag.ERROR, getActualFrame().isError());
             //            setStatus(Flag.ABSENT, getActualFrame().isRemoved());
-            getCache().notifyClosed();
+            getCache().notifyClosure();
         }
         return result;
     }
@@ -276,7 +276,7 @@ public int getAbsence() {
         if (isDone()) {
             return Status.getAbsence(getStatus());
         } else {
-            return getCache().getAbsence();
+            return getCache().getEventualTransience();
         }
     }
 

src/main/java/nl/utwente/groove/lts/ExploreData.java

@@ -48,7 +48,7 @@ class ExploreData {
     ExploreData(StateCache cache) {
         this.cache = cache;
         GraphState state = this.state = cache.getState();
-        this.transience = state.getActualFrame().getTransience();
+        this.eventualTransience = state.getActualFrame().getTransience();
         var internal = this.internal = state.getPrimeFrame().isInternal();
         this.inRecipeInits = internal
             ? new ArrayList<>()
@@ -99,7 +99,7 @@ void notifyOutPartial(RuleTransition partial) {
             return;
         }
         ExploreData succData = succ.getCache().getExploreData();
-        this.transience = Math.min(this.transience, succData.transience);
+        this.eventualTransience = Math.min(this.eventualTransience, succData.eventualTransience);
         if (getState().isTransient()) {
             addReachable(partial);
             if (succ.isTransient()) {
@@ -131,7 +131,7 @@ void notifyOutPartial(RuleTransition partial) {
     /**
      * Callback method invoked when the state has been closed.
      */
-    void notifyClosed() {
+    void notifyClosure() {
         if (DEBUG) {
             System.out.printf("State closed: %s%n", getState());
         }
@@ -145,16 +145,19 @@ void notifyClosed() {
     }
 
     /** Notifies the cache of a decrease in transient depth of the control frame. */
-    final void notifyDepth(int transience) {
+    final void notifyTransience(int transience) {
         if (DEBUG) {
             System.out.printf("Transient depth of %s set to %s%n", getState(), transience);
         }
-        if (transience < this.transience) {
-            this.transience = transience;
+        if (transience < this.eventualTransience) {
+            this.eventualTransience = transience;
         }
-        Change change = Change.TRANSIENCE;
-        if (isInternal() && !getState().isInternalState()) {
-            change = Change.TOP_LEVEL;
+        Change change = isInternal() && transience == 0
+            ? Change.STABILIZED
+            : Change.TRANSIENCE;
+        if (isInternal() && transience == 0) {
+            assert transience == 0;
+            change = Change.STABILIZED;
         }
         fireChanged(getState(), change);
     }
@@ -169,7 +172,7 @@ private void fireChanged(GraphState child, Change change) {
             assert parent != this;
             parent.notifyChildChanged(child, change);
         }
-        if (getState().getPrimeFrame().isInternal() && change == Change.TOP_LEVEL) {
+        if (isInternal() && change == Change.STABILIZED) {
             if (DEBUG) {
                 System.out
                     .printf("Top-level reachables of %s augmented by %s%n", getState(), child);
@@ -186,8 +189,8 @@ private void notifyChildChanged(GraphState child, Change change) {
         if ((!child.isTransient() || child.isClosed()) && this.reachableTransients.remove(child)
             || this.reachableTransients.contains(child)) {
             int childAbsence = child.getAbsence();
-            if (childAbsence < this.transience) {
-                this.transience = childAbsence;
+            if (childAbsence < this.eventualTransience) {
+                this.eventualTransience = childAbsence;
             }
             fireChanged(child, change);
             if (this.reachableTransients.isEmpty() && getState().isClosed()) {
@@ -205,7 +208,7 @@ private void addReachable(RuleTransition partial) {
         var target = partial.target();
         // add the partial if it was not already known
         if (this.reachablePartials.add(partial)) {
-            this.transience = Math.min(this.transience, target.getAbsence());
+            this.eventualTransience = Math.min(this.eventualTransience, target.getAbsence());
             // notify all parents of the new partial
             for (ExploreData parent : this.parentTransients) {
                 parent.addReachable(partial);
@@ -220,13 +223,13 @@ private void addReachable(RuleTransition partial) {
     }
 
     private void setStateDone() {
-        getState().setDone(this.transience);
+        getState().setDone(this.eventualTransience);
         this.parentTransients.clear();
     }
 
     /** Adds recipe transitions from the known recipe sources to a given recipe target. */
     private void addRecipeTarget(RecipeTarget target) {
-        assert getState().getPrimeFrame().isInternal() && !target.state().isInternalState();
+        assert isInternal() && !target.state().isInternalState();
         if (DEBUG) {
             System.out.printf("Recipe targets of %s augmented by %s%n", getState(), target);
         }
@@ -263,26 +266,26 @@ private void addRecipeTransition(RuleTransition partial, RecipeTarget target) {
     }
 
     /**
-     * Returns the absence level of the state.
+     * Returns the (known) eventual transience of the state.
      * This is {@link Status#MAX_ABSENCE} if the state is erroneous,
      * otherwise it is the minimum transient depth of the reachable states.
      */
-    final int getAbsence() {
-        return this.transience;
+    final int getEventualTransience() {
+        return this.eventualTransience;
     }
 
     /**
-     * Known absence level of the state.
-     * The absence level is the minimum transient depth of the known reachable states.
+     * Known eventual transience of the state.
+     * The eventual transience is the minimum transient depth of the reachable states.
      */
-    private int transience;
+    private int eventualTransience;
 
-    /** Indicates whether this state is internal to a recipe. */
+    /** Indicates whether (the prime frame of) this state is internal to a recipe. */
     private boolean isInternal() {
         return this.internal;
     }
 
-    /** Flag indicating if the prime frame is internal. */
+    /** Flag indicating if (the prime frame of) this state is internal. */
     private final boolean internal;
 
     /**
@@ -435,12 +438,12 @@ private void fill() {
 
     /** Type of propagated change. */
     enum Change {
-        /** The transient depth decreased because an atomic block was exited. */
+        /** The transient depth decreased (but not to 0) because an atomic block was exited. */
         TRANSIENCE,
         /** The state closed. */
         CLOSURE,
-        /** The state became top-level. */
-        TOP_LEVEL,;
+        /** The state went from internal to stable. */
+        STABILIZED,;
     }
 
     /** Combination of target state and out-parameter values. */

src/main/java/nl/utwente/groove/lts/StateCache.java

@@ -97,8 +97,8 @@ public boolean approves(Object obj) {
     /**
      * Callback method invoked when the state has been closed.
      */
-    void notifyClosed() {
-        getExploreData().notifyClosed();
+    void notifyClosure() {
+        getExploreData().notifyClosure();
     }
 
     final AbstractGraphState getState() {
@@ -144,17 +144,17 @@ final ExploreData getExploreData() {
     private ExploreData exploreData;
 
     /**
-     * Returns the lowest known absence depth of the state.
+     * Returns the known eventual transient depth of the state.
      * This is {@link Integer#MAX_VALUE} if the state is erroneous,
      * otherwise it is the minimum transient depth of the reachable states.
      */
-    final int getAbsence() {
-        return getExploreData().getAbsence();
+    final int getEventualTransience() {
+        return getExploreData().getEventualTransience();
     }
 
     /** Notifies the cache of a decrease in transient depth of the control frame. */
-    final void notifyDepth(int depth) {
-        getExploreData().notifyDepth(depth);
+    final void notifyTransience(int depth) {
+        getExploreData().notifyTransience(depth);
     }
 
     /**