doc folder + exploration doc added

doc/exploration/explore.aux

@@ -0,0 +1,2 @@
+\relax 
+\gdef \@abspage@last{2}

doc/exploration/explore.tex

@@ -0,0 +1,73 @@
+\documentclass{article}
+\usepackage{preamble}
+\begin{document}
+\title{Fundamentals of exploration in \GROOVE}
+\author{Arend Rensink}
+\date{August 2024}
+\maketitle
+
+\medskip\noindent
+We globally assume a set of labels $A$.
+
+\medskip\noindent 
+A state space is a tuple $\tupof{S,{\ra},{\up},\Tdepth}$ with
+\begin{itemize}
+\item $S$ a set of states;
+\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}.
+
+\medskip\noindent
+A pseudo-state space is a tuple $\tupof{P,{\mapsto},{\goesto},{\up},\Tdepth}$ with
+\begin{itemize}
+\item $P$ a finite set of pseudo-states;
+\item ${\step{}}\subseteq P\times A\times P$ a step relation;
+\item ${\goesto}: P\times P$ a partial, acyclic evolution relation;
+\item ${\up} \subseteq P$ a termination predicate;
+\item ${\Tdepth}:S\to \natN$ a \emph{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.
+%
+A pseudo-state space is \emph{well-formed} if it satisfies the following additional properties:
+\begin{itemize}
+\item Stepping is deterministic; i.e., $\step{}$ is a partial function from $P$ to $A\times P$;
+\item Evolution is deterministic; i.e., $\goesto$ is a partial function from $P$ to $P$;
+\item Evolution is injective; i.e., $\comesfrom$ is a partial function from $P$ to $P$;
+\item All steps go from open to prime pseudo-states; i.e., $p\step{}q$ implies $\Open(p)$ and $\Prime(q)$;
+\item All final pseudo-states are stable and closed; i.e., $p\up$ implies $\Stable(p)$ and $\Closed(p)$;
+\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.
+\end{align*}
+%
+Note that these are well-defined because $P$ is finite and $\goesto$ is acyclic, deterministic and injective.
+
+\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
+%
+\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}
+%
+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
+%
+\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}
+\end{document}

doc/exploration/preamble.sty

@@ -0,0 +1,68 @@
+\usepackage{xspace}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{MnSymbol}
+%\usepackage{stmaryrd}
+\usepackage[inline]{enumitem}
+\setlist{itemsep=0pt}
+
+\newcommand{\GROOVE}{GROOVE}
+
+\newcommand{\cls}[1]{{#1}\mskip1mu\triangleright}
+\newcommand{\prm}[1]{\triangleleft\mskip1mu{#1}}
+
+\newcommand{\dom}{\mathop{\mathrm{dom}}}
+
+\newcommand{\Prime}{\ensuremath{\mathit{prime}}}
+\newcommand{\Done}{\ensuremath{\mathit{done}}}
+\newcommand{\Open}{\ensuremath{\mathit{open}}}
+\newcommand{\Closed}{\ensuremath{\mathit{closed}}}
+\newcommand{\Trnt}{\ensuremath{\mathit{trnt}}}
+\newcommand{\Abs}{\ensuremath{\mathit{abs}}}
+\newcommand{\Stable}{\ensuremath{\mathit{stable}}}
+\newcommand{\Tdepth}{\ensuremath{\mathit{tdp}}}
+
+\newcommand{\cC}{\mathcal{C}}
+\newcommand{\natN}{\mathbb{N}}
+
+\newcommand{\setof}[1]{\{{#1}\}}
+\newcommand{\gensetof}[2]{\setof{{#1}\mid{#2}}}
+\newcommand{\tupof}[1]{\langle{#1}\rangle}
+\newcommand{\iffdef}{:\Leftrightarrow}
+
+% Special arrows
+\newcommand{\pto}{\lhook\joinrel\to}
+\newcommand{\goesto}{\rightarrowtail}
+\newcommand{\ngoesto}{\arrownot\rightarrowtail}
+\newcommand{\comesfrom}{\leftarrowtail}
+\newcommand{\ncomesfrom}{\arrownot\leftarrowtail}
+\newcommand{\ra}{\rightarrow}
+\newcommand{\up}{{\uparrow}}
+\newcommand{\Up}{{\Uparrow}}
+
+
+%%%% definition of extensible "transition arrows"
+%
+% auxiliaries
+\newcommand{\linefill}{%
+	\cleaders
+	\hbox{$\smash{\mkern-2mu\mathord-\mkern-2mu}$}%
+	\hfill
+	\vphantom{\lower1pt\hbox{$\rightarrow$}}%
+}
+\newcommand{\Linefill}{%
+	\cleaders
+	\hbox{$\smash{\mkern-2mu\mathord=\mkern-2mu}$}%
+	\hfill
+	\vphantom{\hbox{$\Rightarrow$}}%
+}
+
+% single-arrow transition
+\newcommand{\trans}[1]{\xrightarrow{#1}}%
+% negative single-arrow transition
+\newcommand{\ntrans}[1]{\not\xrightarrow{#1}}
+
+% mapsto-like transition
+\newcommand{\step}[1]{\mapstochar\xrightarrow{#1}}
+% negative mapsto-like transition
+\newcommand{\nstep}[1]{\not\mapstochar\joinrel\xrightarrow{#1}}

doc/exploration/texput.log

@@ -0,0 +1,21 @@
+This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024) (preloaded format=pdflatex 2024.7.9)  27 AUG 2024 16:15
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**preamble.tex
+
+! Emergency stop.
+<*> preamble.tex
+
+*** (job aborted, file error in nonstop mode)
+
+
+Here is how much of TeX's memory you used:
+ 3 strings out of 473584
+ 104 string characters out of 5732364
+ 1925908 words of memory out of 5000000
+ 22997 multiletter control sequences out of 15000+600000
+ 558069 words of font info for 36 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 0i,0n,0p,1b,6s stack positions out of 10000i,1000n,20000p,200000b,200000s
+!  ==> Fatal error occurred, no output PDF file produced!