\documentclass{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage[dvipsnames]{xcolor}

\setcounter{MaxMatrixCols}{10}

\font \aap cmmi10
\newcommand{\at}[1]{\mbox{\aap ,} #1}
\newcommand{\ap}{{:}}
\newcommand{\tuple}[1]{\ensuremath{\langle {#1} \rangle}}
\newcommand{\vars}{\mathit{vars}}
\newtheorem{theorem}{Theorem}
\newtheorem{acknowledgement}[theorem]{Acknowledgement}
\newtheorem{algorithm}[theorem]{Algorithm}
\newtheorem{axiom}[theorem]{Axiom}
\newtheorem{case}[theorem]{Case}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{conclusion}[theorem]{Conclusion}
\newtheorem{condition}[theorem]{Condition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{criterion}[theorem]{Criterion}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{solution}[theorem]{Solution}
\newtheorem{summary}[theorem]{Summary}
\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }{\ \rule{0.5em}{0.5em}}

\newcommand{\up}{\blacktriangle}
\newcommand{\down}{\blacktriangledown}

%--- pseudo code ---%
\newcommand{\Space}{\text{\ }}
\newcommand{\If}{\text{\textbf{if }}}
\newcommand{\Do}{\text{\textbf{ do }}}
\newcommand{\Then}{\text{\textbf{ then }}}
\newcommand{\Else}{\text{\textbf{else }}}
\newcommand{\For}{\text{\textbf{for }}}
\newcommand{\While}{\text{\textbf{while }}}
\newcommand{\Break}{\text{\textbf{break }}}
\newcommand{\Continue}{\text{\textbf{continue }}}
\newcommand{\Choose}{\text{\textbf{choose }}}
\newcommand{\Return}{\text{\textbf{return }}}
\newcommand{\With}{\text{\textbf{ with }}}

\begin{document}

\title{PBES Instantiation and Solving}
\author{<NAME>, <NAME>}
\maketitle

This document describes instantiation and solving algorithms for PBESs that
are used in the tools \texttt{pbesinst} and \texttt{pbessolve}.

\section{Finite algorithm}

In this section we describe an implementation of the finite instantiation
algorithm \textsc{PbesInstFinite} that eliminates data parameters with
finite sorts. It is implemented in the tool \texttt{pbesinst}. Let $\mathcal{%
E=(\sigma }_{1}X_{1}(d_{1}:D_{1},e_{1}:E_{1})=\varphi _{1})\cdots \mathcal{%
(\sigma }_{n}X_{n}(d_{n}:D_{n},e_{n}:E_{n})=\varphi _{n})$ be a PBES. We
assume that all data sorts $D_{i}$ are finite and all data sorts $E_{i}$ are
infinite. Let $r$ be a data rewriter, and let $\rho $ be an injective
function that creates a unique predicate variable from a predicate variable
name and a data value according to $\rho (X(d:D,e:E),d_{0})\rightarrow Y(e:E)
$, where $D$ is finite and $E$ is infinite and $d_{0}\in D$. Note that $D$
and $D_{i}$ may be multi-dimensional sorts.%
\begin{equation*}
\begin{array}{l}
\text{\textsc{PbesInstFinite(}}\mathcal{E}\text{, }r\text{, }\rho \text{%
\textsc{)}} \\
\For i:=1\cdots n\text{ \textbf{do}} \\
\qquad \mathcal{E}_{i}:=\{\mathcal{\sigma }_{i}\rho (X_{i},d)=R(\varphi
_{k}[d_{k}:=d])\ |\ d\in D_{i}\} \\
\Return \mathcal{E}_{1}\cdots \mathcal{E}_{n},%
\end{array}%
\end{equation*}%
with $R$ a rewriter on pbes expressions that is defined as follows:%
\begin{eqnarray*}
R(b) &=&b \\
R(\lnot \varphi ) &=&\lnot R(\varphi ) \\
R(\varphi \oplus \psi ) &=&R(\varphi )\oplus R(\psi ) \\
R(X_{i}(d,e)) &=&\left\{
\begin{array}{cc}
\rho (X_{i},r(d))(r(e)) & \text{if }FV(d)=\emptyset  \\
\bigvee\limits_{d_{i}\in D_{i}}r(d=d_{i})\wedge \rho (X_{i},d_{i})(r(e)) &
\text{if }FV(d)\neq \emptyset
\end{array}%
\right.  \\
R(\forall _{d:D}.\varphi ) &=&\forall _{d:D}.R(\varphi ) \\
R(\exists _{d:D}.\varphi ) &=&\exists _{d:D}.R(\varphi )
\end{eqnarray*}%
where $\oplus \in \{\vee ,\wedge ,\Rightarrow \}$, $b$ a data expression and
$\varphi $ and $\psi $ pbes expressions and $FV(d)$ is the set of free
variables appearing in $d$.\newpage

\section{Lazy algorithm}

In this section we describe an implementation of the lazy instantiation
algorithm \textsc{PbesInstLazy} that uses instantiation to compute a BES. It
is implemented in the tool \texttt{pbesinst}. It takes two extra parameters,
an injective function $\rho $ that renames proposition variables to
predicate variables, and a rewriter $R$ that eliminates quantifiers from
predicate formulae. Let $\mathcal{E=(\sigma }_{1}X_{1}(d_{1}:D_{1})=\varphi
_{1})\ldots \mathcal{(\sigma }_{n}X_{n}(d_{n}:D_{n})=\varphi _{n})$ be a
PBES, and $X_{init}(e_{init})$ an initial state.%
\begin{equation*}
\begin{array}{l}
\text{\textsc{PbesInstLazy(}}\mathcal{E}\text{, }X_{init}(e_{init})\text{, }R%
\text{, }\rho \text{\textsc{)}} \\
\For i:=1\cdots n\text{ \textbf{do }}\mathcal{E}%
_{i}:=\epsilon  \\
todo:=\{R(X_{init}(e_{init}))\} \\
done:=\emptyset  \\
\While todo\neq \emptyset \Do \\
\qquad \Choose X_{k}(e)\in todo \\
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\
\qquad done:=done\cup \{X_{k}(e)\} \\
\qquad X^{e}:=\rho (X_{k}(e)) \\
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\
\qquad \mathcal{E}_{k}:=\mathcal{E}_{k}(\mathcal{\sigma }_{k}X^{e}=\rho
(\psi ^{e})) \\
\qquad todo:=todo\cup \{Y(f)\in \mathsf{occ}(\psi ^{e})\ |\ Y(f)\notin done\}
\\
\Return \mathcal{E}_{1}\cdots \mathcal{E}_{n},%
\end{array}%
\end{equation*}%
where $\rho $ is extended from predicate variables to quantifier free
predicate formulae using

\begin{eqnarray*}
\rho (b) &=&b \\
\quad \rho (\varphi \oplus \psi ) &=&\rho (\varphi )\oplus \rho (\psi )
\end{eqnarray*}%
\newpage

\section{Generic lazy algorithms}

In this section two generic variants of lazy PBES instantiation are
described that report all discovered BES equations using a callback
function \textsc{ReportEquation}. These versions are later extended to compute
structure graphs.

The first version \textsc{PbesInstLazy1}
maintains a collection $done$, that contains all BES variables for
which an equation has been computed.%
\begin{equation*}
\begin{array}{l}
\text{\textsc{PbesInstLazy1(}}\mathcal{E}\text{, }X_{init}(e_{init})\text{, }%
R\text{\textsc{)}} \\
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
done:=\emptyset \\
\While todo\neq \emptyset \Do \\
\qquad \Choose X_{k}(e)\in todo \\
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\
\qquad done:=done\cup \{X_{k}(e)\} \\
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\
\qquad \text{\textsc{ReportEquation}}(X_{k}(e),\psi ^{e}) \\
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus done)
\end{array}
\end{equation*}

The second version \textsc{PbesInstLazy2} maintains a set $discovered$
instead of $done$. This set contains BES
variables that have been discovered, but for which the corresponding
equation may not have been computed yet. The sets are related via
$done = discovered \setminus todo$.

\begin{equation*}
\begin{array}{l}
\text{\textsc{PbesInstLazy2(}}\mathcal{E}\text{, }X_{init}(e_{init})\text{, } R\text{\textsc{)}} \\
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
\While todo\neq \emptyset \Do \\
\qquad \Choose X_{k}(e)\in todo \\
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\
\qquad \text{\textsc{ReportEquation}}(X_{k}(e),\psi ^{e}) \\
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e})
\end{array}
\end{equation*}

It turned out that the second version has slightly better performance for
some larger use cases, so the second version is implemented in the tool \texttt{pbessolve}.

To support breadth first and depth first search, the implementation stores the
set $todo$ as a double ended queue. New elements are always appended to $todo$.
In the case of breadth first search always the first element is chosen, and in the
case of depth first search the last element.

\section{Structure graphs}
A structure graph is a tuple $(V,E,d,r)$ with $V$ a set of nodes containing BES variables,
$E$ a set of edges, $r:V\rightarrow \mathbb{N}$ a partial function that assigns a rank to each node,
and $d:V\rightarrow \{\blacktriangle ,\blacktriangledown ,\top ,\bot \}$ a partial function that
assigns a decoration to each node. A structure graph is formally defined using the
following SOS rules:

\begin{equation*}
\frac{X\in bnd(\mathcal{E})}{r(X) = rank_{\mathcal{E}}(X)}
\end{equation*}

\begin{equation*}
\frac{{}}{d(true) = \top }\qquad \frac{{}}{d(false) = \bot }
\end{equation*}
\begin{equation*}
\frac{{}}{d(f \wedge f^{\prime}) = \blacktriangle } \qquad
\frac{{}}{d(f \vee f^{\prime}) = \blacktriangledown }
\end{equation*}
\begin{equation*}
\frac{f\blacktriangle \quad f\rightarrow g}{(f\wedge f^{\prime })\rightarrow g} \qquad
\frac{f\blacktriangle \quad f\rightarrow g}{(f^{\prime }\wedge f)\rightarrow g}
\end{equation*}%
\begin{equation*}
\frac{f\blacktriangledown \quad f\rightarrow g}{(f\vee f^{\prime })\rightarrow g} \qquad
\frac{f\blacktriangledown \quad f\rightarrow g}{(f^{\prime }\vee f)\rightarrow g}
\end{equation*}%
\begin{equation*}
\frac{\lnot f\blacktriangle }{f\wedge f^{\prime }\rightarrow f}\qquad \frac{%
\lnot f^{\prime }\blacktriangle }{f\wedge f^{\prime }\rightarrow f^{\prime }}
\end{equation*}%
\begin{equation*}
\frac{\lnot f\blacktriangledown }{f\vee f^{\prime }\rightarrow f}\qquad
\frac{\lnot f^{\prime }\blacktriangledown }{f\vee f^{\prime }\rightarrow
f^{\prime }}
\end{equation*}%
\begin{equation*}
\frac{{}}{X\wedge f\rightarrow X}\qquad \frac{{}}{f\wedge X\rightarrow X}
\end{equation*}%
\begin{equation*}
\frac{{}}{X\vee f\rightarrow X}\qquad \frac{{}}{f\vee X\rightarrow X}
\end{equation*}%
\begin{equation*}
\frac{\sigma X=f\wedge f^{\prime }\in \mathcal{E}}{d(X) = \blacktriangle }\qquad
\frac{\sigma X=f\vee f^{\prime }\in \mathcal{E}}{d(X) = \blacktriangledown }
\end{equation*}%
\begin{equation*}
\frac{\sigma X=Y\in \mathcal{E}}{X\rightarrow Y}\qquad \frac{\sigma X=\top
\in \mathcal{E}}{X\rightarrow \top }\qquad \frac{\sigma X=\bot \in \mathcal{E%
}}{X\rightarrow \bot }
\end{equation*}%
\begin{equation*}
\frac{\sigma X=f\wedge f^{\prime }\in \mathcal{E}\quad f\wedge f^{\prime
}\rightarrow g}{X\rightarrow g}
\end{equation*}%
\begin{equation*}
\frac{\sigma X=f\vee f^{\prime }\in \mathcal{E}\quad f\vee f^{\prime
}\rightarrow g}{X\rightarrow g}
\end{equation*}%
Note that in this definition separate nodes are created for the left hand
side $X$ and the right hand side $f$ of each equation $\sigma X=f$ . This is
undesirable, hence in implementations usually the nodes $X$ and $f$ are
merged into one node labeled with $X$.

\subsection{Attractor sets}
Let $A \subseteq V$ be a subset of vertices of a structure graph $G=(V,E,d,r)$. We
define the following algorithms for computing an attractor set of $A$. The value
$\alpha = 0$ corresponds with disjunction and $\alpha = 1$ with conjunction.

\begin{equation*}
\begin{array}{l}
\textsc{AttrDefault}(A,\alpha) \\ 
todo:=\bigcup\limits_{u\in A}\left( pred(u)\setminus A\right)  \\ 
\While todo\neq \emptyset \Do \\ 
\qquad \Choose u\in todo \\ 
\qquad todo:=todo\ \backslash \ \{u\} \\ 
\qquad \If d(u) = \alpha \vee succ(u)\subseteq A \Then \\ 
\qquad \qquad \colorbox{Apricot}{$ \If d(u) = \alpha \Then \tau
\lbrack u]:=v\With v\in A\cap succ(u) $}\\ 
\qquad \qquad A:=A\cup \{u\} \\ 
\qquad \qquad todo:=todo\cup \left( pred(u)\setminus A\right)  \\ 
\Return A
\end{array}
\end{equation*}
where
\begin{eqnarray*}
pred(v) &=&\{u\in V\mid (u,v)\in E\} \\
succ(u) &=&\{v\in V\mid (u,v)\in E\}
\end{eqnarray*}%

As a side effect a mapping $\tau$ is produced that corresponds to a winning
strategy. Assignments to $\tau$ are \colorbox{Apricot}{colored}.

A second version \textsc{AttrDefaultWithTau} is available, that in addition
sets the strategy in the mapping $\tau_\alpha$.

\begin{equation*}
\begin{array}{l}
\textsc{AttrDefaultWithTau}(A,\alpha,\tau_\alpha) \\ 
todo:=\bigcup\limits_{u\in A}\left( pred(u)\setminus A\right)  \\ 
\While todo\neq \emptyset \Do \\ 
\qquad \Choose u\in todo \\ 
\qquad todo:=todo\ \backslash \ \{u\} \\ 
\qquad \If d(u) = \alpha \vee succ(u)\subseteq A \Then \\ 
\qquad \qquad \colorbox{Apricot}{$ \If d(u) = \alpha \Then
\tau[u], \tau_\alpha[u] := v, v \With v\in A\cap succ(u) $}\\ 
\qquad \qquad A:=A\cup \{u\} \\ 
\qquad \qquad todo:=todo\cup \left( pred(u)\setminus A\right)  \\ 
\Return A, \tau_\alpha
\end{array}
\end{equation*}

Finally \textsc{AttrDefaultNoStrategy} does not set any strategy:

\begin{equation*}
\begin{array}{l}
\textsc{AttrDefaulNoStrategy}(A,\alpha) \\ 
todo:=\bigcup\limits_{u\in A}\left( pred(u)\setminus A\right)  \\ 
\While todo\neq \emptyset \Do \\ 
\qquad \Choose u\in todo \\ 
\qquad todo:=todo\ \backslash \ \{u\} \\ 
\qquad \If d(u) = \alpha \vee succ(u)\subseteq A \Then \\ 
\qquad \qquad A:=A\cup \{u\} \\ 
\qquad \qquad todo:=todo\cup \left( pred(u)\setminus A\right)  \\ 
\Return A
\end{array}
\end{equation*}


% A cheaper, less powerful attractor set computation is
%
% \begin{equation*}
% \begin{array}{l}
% \textsc{AttrCheap}(S,v,\alpha) \\ 
% todo := pred(v) \setminus S \\ 
% A := \{ v \} \\
% \While todo \neq \emptyset \Do \\ 
% \qquad \Choose u \in todo \\ 
% \qquad todo := todo\ \setminus \{ u \} \\ 
% \qquad \If (d(u) = \alpha \wedge succ(u) \cap A \neq \emptyset)
%           \vee (d(u) \neq \alpha \wedge succ(u) \subseteq A \cup S) \Then \\ 
% \qquad \qquad A := A \cup \{ u \} \\ 
% \qquad \qquad todo := todo \cup \left( pred(u) \setminus (A \cup S) \right)  \\ 
% \Return A \cup S
% \end{array}
% \end{equation*}

A second version of an attractor set computation is \textsc{AttrSimple}. It is used for pruning the todo list.

\begin{equation*}
\begin{array}{l}
\textsc{AttrSimple}(A) \\ 
todo:=\bigcup\limits_{u\in A}\left( pred(u)\setminus A\right)  \\ 
\While todo \neq \emptyset \Do \\ 
\qquad \Choose u \in todo \\ 
\qquad todo:=todo\ \backslash \ \{u\} \\ 
\qquad \If succ(u)\subseteq A \Then \\ 
\qquad \qquad A:=A\cup \{u\} \\ 
\qquad \qquad \colorbox{Apricot}{$ \If d(u) = \alpha \Then \tau
\lbrack u]:=v\With v\in A\cap succ(u) $}\\ 
\qquad \qquad todo:=todo\cup \left( pred(u)\setminus A\right)  \\ 
\Return A
\end{array}
\end{equation*}

\subsection{Recursive procedure for solving structure graphs}

Let $G=(V,E,d,r)$ be a structure graph. The following algorithm is used to compute
a partitioning of $V$ into $\left( W_{0},W_{1}\right) $ of vertices $W_{0}$ that
represent equations evaluating to true and vertices $W_{1}$ that represent equations
evaluating to false. A precondition of this algorithm is that it contains no nodes with
decoration $\top $ or $\bot$. This algorithm is based on Zielonka's recursive algorithm.
\begin{equation*}
\begin{array}{l}
\textsc{SolveRecursive}(V) \\ 
\If V=\emptyset \text{ \textbf{then return }}(\emptyset
,\emptyset ) \\ 
m:=\min (\{r(v)\mid v\in V\}) \\ 
\alpha := m \bmod 2 \\ 
U:=\{v\in V\mid r(v)=m\} \\ 
A:=\text{\textsc{AttrDefault}}\left( U,\alpha \right)  \\ 
W_{0}^{\prime },W_{1}^{\prime }:=\text{\textsc{SolveRecursive(}}V\setminus A%
\text{)} \\ 
\If W_{1-\alpha }^{\prime }= \emptyset \Then \\ 
\qquad W_{\alpha },W_{1-\alpha }:=A\cup W_{\alpha }^{\prime }, \emptyset \\ 
\Else \\ 
\qquad B:=\text{\textsc{AttrDefault}}\left( W_{1-\alpha }^{\prime },1-\alpha \right)  \\ 
\qquad W_{0},W_{1}:=\text{\textsc{SolveRecursive(}}V\setminus B\text{)} \\ 
\qquad W_{1-\alpha }:=W_{1-\alpha }\cup B \\ 
\Return W_{0},W_{1}%
\end{array}%
\end{equation*}%
where%
\begin{equation*}
succ(u,U)=\left\{ 
\begin{array}{ll}
succ(u)\cap U & \text{if }succ(u)\cap U\neq \emptyset  \\ 
succ(u) & \text{otherwise}%
\end{array}%
\right. 
\end{equation*}

<NAME> has introduced an optimization that may reduce the number of recursive calls. Note that this optimized version does not compute a complete strategy, so it
cannot be used for counter example generation(!)

\begin{equation*}
\begin{array}{l}
\textsc{SolveRecursive}(V) \\ 
precondition: V \subseteq dom(r) \cup dom(d) \\
\If V=\emptyset \text{ \textbf{then return }}(\emptyset
,\emptyset ) \\ 
m:=\min (\{r(v)\mid v\in V\}) \\ 
\alpha := m \bmod 2 \\ 
U:=\{v\in V\mid r(v)=m\} \\ 
\colorbox{Apricot}{$
\text{\textbf{for} }u\in U\text{ \textbf{if} }d(u)=\alpha \wedge succ(u)\neq
\emptyset \Then \tau \lbrack u]:=v\With v\in
succ(u) $}\\ 
A:=\text{\textsc{AttrDefault}}\left( U,\alpha \right)  \\ 
W_{0}^{\prime },W_{1}^{\prime }:=\text{\textsc{SolveRecursive(}}V\setminus A%
\text{)} \\
\colorbox{lightgray}{$
B:=\text{\textsc{AttrDefault}}\left( W_{1-\alpha }^{\prime },1-\alpha \right) $}\\ 
\colorbox{lightgray}{$
\If W_{1-\alpha }^{\prime }=B \Then $}\\ 
\colorbox{lightgray}{$
\qquad W_{\alpha },W_{1-\alpha }:=A\cup W_{\alpha }^{\prime },B $}\\ 
\colorbox{lightgray}{$
\Else $}\\ 
\colorbox{lightgray}{$
\qquad W_{0},W_{1}:=\textsc{SolveRecursive}(V \setminus B)$}\\ 
\colorbox{lightgray}{$
\qquad W_{1-\alpha }:=W_{1-\alpha }\cup B $}\\ 
\Return W_{0},W_{1}
\end{array}
\end{equation*}
The algorithm can be extended to sets $V$ containing nodes with decoration $%
\top $ or $\bot $ as follows:%
\begin{equation*}
\begin{array}{l}
\textsc{SolveRecursiveExtended}(V) \\ 
V_{1}:=\textsc{AttrDefault}\left( \{v\in V\mid d(v) = \bot \},1\right) \\ 
V_{0}:=\textsc{AttrDefault}\left( \{v\in V\mid d(v) = \top \},0\right) \\ 
\left( W_{0},W_{1}\right) :=\text{\textsc{SolveRecursive(}}V\setminus
(V_{0}\cup V_{1})\text{\textsc{)}} \\ 
\Return \left( W_{0}\cup V_{1},W_{0}\cup V_{1}\right)%
\end{array}
\end{equation*}
Another possible optimization of the \textsc{SolveRecursive} algorithm is to insert the
following shortcuts. This doesn't seem to have much effect in practice, so currently it
isn't enabled in the code.
\begin{equation*}
\begin{array}{l}
\textsc{SolveRecursive}(V) \\ 
\If V=\emptyset \text{ \textbf{then return }}(\emptyset
,\emptyset ) \\ 
m:=\min (\{r(v)\mid v\in V\}) \\ 
\alpha :=m \bmod 2 \\ 
U:=\{v\in V\mid r(v)=m\} \\ 
\colorbox{Apricot}{$
\text{\textbf{for} }u\in U\text{ \textbf{if} }d(u)=\alpha \wedge succ(u)\neq
\emptyset \Then \tau \lbrack u]:=v\With v\in
succ(u) $}\\ 
\colorbox{lightgray}{$
\If h=m\wedge even(m) \Then \Return (\emptyset,V) $}\\ 
\colorbox{lightgray}{$
\If h=m\wedge odd(m) \Then \Return (V,\emptyset) $}\\
A:=\text{\textsc{AttrDefault}}\left( U,\alpha \right)  \\ 
W_{0}^{\prime },W_{1}^{\prime }:=\text{\textsc{SolveRecursive(}}V\setminus A%
\text{)} \\ 
\If W_{1-\alpha }^{\prime }= \emptyset \Then \\ 
\qquad W_{\alpha },W_{1-\alpha }:=A\cup W_{\alpha }^{\prime }, \emptyset \\ 
\Else \\ 
\qquad B:=\text{\textsc{AttrDefault}}\left( W_{1-\alpha }^{\prime },1-\alpha \right)  \\ 
\qquad W_{0},W_{1}:=\text{\textsc{SolveRecursive(}}V\setminus B\text{)} \\ 
\qquad W_{1-\alpha }:=W_{1-\alpha }\cup B \\ 
\Return W_{0},W_{1}%
\end{array}%
\end{equation*}%

\newpage
\section{Structure graph based PBES instantiation}

In the tool \texttt{pbessolve} an extension called \textsc{%
PbesInstStructureGraph} of the \textsc{PbesInstLazy2} algorithm is
implemented that builds a structure graph from the reported equations. On
top of it several optimizations to this algorithm are defined. For
readability, we only present the full algorithms here, and highlight the
changes with respect to previous versions. A graph $G$ is
represented as a tuple $(V,E)$ with $V$ the set of vertices and $E$ the set
of edges.%
\begin{equation*}
\begin{array}{l}
\text{\textsc{PbesInstStructureGraph(}}\mathcal{E}\text{, }X_{init}(e_{init})%
\text{, }R\text{\textsc{)}} \\
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
\colorbox{lightgray}{$%
(V,E) :=(\emptyset ,\emptyset ) $}\\
\While todo\neq \emptyset \Do \\
\qquad \Choose X_{k}(e)\in todo \\
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\
\qquad \colorbox{lightgray}{$%
(V,E) := (V,E) \cup SG^{0}(X_{k}(e),\psi ^{e}) $}\\
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\Return (V, E)%
\end{array}%
\end{equation*}

where $SG^{0}$ and $SG^{1}$ are defined as%
\begin{equation*}
\begin{array}{|c|c|}
\hline
\psi  & SG^{0}(\varphi ,\psi ) \\ \hline\hline
true & (\{\varphi \},\emptyset ) \\ \hline
false & (\{\varphi \},\emptyset ) \\ \hline
Y & (\{\varphi ,\psi \},\{(\varphi ,\psi )\}) \\ \hline
\psi _{1}\wedge \cdots \wedge \psi _{n} & \left( \{\varphi ,\psi _{1},\cdots
,\psi _{n}\},\{(\varphi ,\psi _{1}),\cdots ,(\varphi ,\psi _{n})\}\right)
\cup \bigcup\limits_{i=1}^{n}SG^{1}(\psi _{i}) \\ \hline
\psi _{1}\vee \cdots \vee \psi _{n} & \left( \{\varphi ,\psi _{1},\cdots
,\psi _{n}\},\{(\varphi ,\psi _{1}),\cdots ,(\varphi ,\psi _{n})\}\right)
\cup \bigcup\limits_{i=1}^{n}SG^{1}(\psi _{i}) \\ \hline
\end{array}%
\end{equation*}%
\begin{equation*}
\begin{array}{|c|c|}
\hline
\psi  & SG^{1}(\varphi ) \\ \hline\hline
true & (\{\psi \},\emptyset ) \\ \hline
false & (\{\psi \},\emptyset ) \\ \hline
Y & (\{\psi \},\emptyset ) \\ \hline
\psi _{1}\wedge \cdots \wedge \psi _{n} & \left( \{\psi ,\psi _{1},\cdots
,\psi _{n}\},\{(\psi ,\psi _{1}),\cdots ,(\psi ,\psi _{n})\}\right) \cup
\bigcup\limits_{i=1}^{n}SG^{1}(\psi _{i}) \\ \hline
\psi _{1}\vee \cdots \vee \psi _{n} & \left( \{\psi ,\psi _{1},\cdots ,\psi
_{n}\},\{(\psi ,\psi _{1}),\cdots ,(\psi ,\psi _{n})\}\right) \cup
\bigcup\limits_{i=1}^{n}SG^{1}(\psi _{i}), \\ \hline
\end{array}%
\end{equation*}%
where we assume that in $\psi _{1}\wedge \cdots \wedge \psi _{n}$ none of
the $\psi _{i}$ is a conjunction, and in $\psi _{1}\vee \cdots \vee \psi _{n}
$ none of the $\psi _{i}$ is a disjunction. Note that both $SG^{0}(\varphi
,\psi )$ and $SG^{1}(\varphi ,\psi )$ are defined as a pair ($V$, $E$) of
nodes and edges.

\subsection{Optimisation~1}

The lemma below indicates that one can simplify the BES equation that is being created
without affecting the solution to the BES. 
\begin{lemma}
The solution to all variables in a BES $\mathcal{E} (\sigma X = f) \mathcal{E}'$ is 
equivalent to the solution to those variables in the BES
$\mathcal{E} (\sigma X = f[X := b_\sigma]) \mathcal{E}'$, where
$b_\sigma = true$ if $\sigma = \nu$ and $b_\sigma = false$ if $\sigma = \mu$.
\end{lemma}
Using this lemma, rather than creating a structure graph underlying the
equation $\sigma X_e = \psi^e$, we can create a structure graph
for $\sigma X_e = \psi^e[X^e := b_\sigma]$.
This can be done by adding the following assignment below the assignment
$\psi^e := R(\varphi_k[d_k := e])$:
\[
\psi^e := R(\psi^e[X^e := b_\sigma])
\]
This leads to the following adaptations in the code:

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_1$(}\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
\While todo\neq \emptyset \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \colorbox{lightgray}{$%
\psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false]) \Space \Else  R(\psi^e[X^e := true]) $}\\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\Return (V, E),%
\end{array}%
\end{equation*}%


\subsection{Optimisation~2}

Our second optimisation exploits the fact that some of the BES
equations that are generated while exploring the PBES are already
solved (possibly after using optimisation~1).  We first introduce
some additional notation. Let $(V,E)$ be a (partial) structure graph
underlying the PBES $\mathcal{E}$.  By $S_0$ we denote the set of
vertices that represent equations with solution $true$, whereas
$S_1$ denotes the set of vertices representing equations with
solution $false$. Along with these sets, we introduce strategies $\tau_0$ and
$\tau_1$ that explain why a vertex belongs to $S_0$ or $S_1$, respectively. Let $\pi$ be a partial
function that maps vertices to the propositional variables they
represent (and only those vertices that represent propositional variables). 
For a set of vertices $S \subseteq V$, we define
the substitution $\rho_i$ as follows for all $s \in S \cap \textsf{dom}(\pi)$: 
$\rho_i(\pi(s)) = true$ if $i = 0$ and $\rho_i(\pi(s)) = false$ if
$i = 1$. The union of two substitutions is again a substitution, provided
that the domain of variables these substitutions range over are disjoint.

The lemma below indicates how one can utilise such information to simplify the BES equation 
that is being created, again without affecting the solution to the BES.

\begin{lemma}
The solution to all variables in a BES $\mathcal{F} \equiv \mathcal{E} (\sigma X = f) \mathcal{E}'$ is 
equivalent to the solution to those variables in the BES
$\mathcal{F}' \equiv \mathcal{E} (\sigma X = f(\rho_0(S_0) \cup \rho_1(S_1))) \mathcal{E}'$, where
for all $S_0 \cup S_1 \subseteq \{v \in V \mid \forall \theta,\theta':
\lbrack \mathcal{F} \rbrack \theta(\pi(v) = 
\lbrack \mathcal{F} \rbrack \theta(\pi(v)\}$, where $\lbrack \mathcal{F} \rbrack \theta$
denotes the solution to $\mathcal{F}$ under environment $\theta$.
\end{lemma}
Using this lemma, rather than creating a structure graph underlying the
equation $\sigma X_e = \psi^e$, we can create a structure graph
for $\sigma X_e = \psi^e(\rho_0(S_0) \cup \rho_1(S_1))$, provided that
$S_0$ and $S_1$ contain vertices that represent solved equations. 
This leads to the following adaptations in the code: we maintain
two sets $S_0$ and $S_1$ for which we can (cheaply) establish that these
correspond to solved equations, and we add an assignment below the assignment
of optimisation~1.

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_{2a}$(}\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
\colorbox{lightgray}{$%
S_0:= \emptyset $}\\
\colorbox{lightgray}{$%
S_1:= \emptyset $}\\
\While todo\neq \emptyset \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad \colorbox{lightgray}{$%
\psi^{e} := R(\psi^e (\rho_0(S_0) \cup \rho_1(S_1) ) ) $}\\
\qquad \colorbox{lightgray}{$%
S_0 := S_0 \cup \{ X^e \mid \psi^e \equiv true \} $}\\
\qquad \colorbox{lightgray}{$%
S_1 := S_1 \cup \{ X^e \mid \psi^e \equiv false \} $}\\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\Return (V, E),%
\end{array}%
\end{equation*}%

Note that this version of the algorithm is not available in the tool \texttt{pbessolve}.

\paragraph{Note on computing winning strategies.} Rewriting the propositional formula
$\psi^e$ using $S_0$ and $S_1$ may result in a loss of information, preventing us from
constructing a winning strategy for both players. We can solve that by mimicking the
attractor set computation in our rewriting; that is, we implement $R(\psi^e(\rho_0(S_0) \cup \rho_1(S_1)))$
using a rewriter $R^+$ which takes a formula (and implicitly takes sets $S_0$ and $S_1$ into account. 
This leads to the following bottom-up
procedure in which $R^+(f)$ yields a tuple $(b, f',g_0,g_1)$, where $b$ is either a Boolean value,
or the value $\bot$, and $f'$ is a propositional formula that is equivalent to $f$ under
the assumption that $S_0$ and $S_1$ are solved, but the formula $f$ is not fully solved using that information. Propositional formula $g_0$ (resp.\ $g_1$) is a conjunctive (resp.\ disjunctive) formulae, representing $f$ in case $b$ is true (resp.\ false); in case $b$ is true, the conjunctive formula $g_0$ can be used to construct a witness, as it contains exactly all dependencies on $S_0$ that are needed to make formula $f$ hold. Dually for formula $g_1$.


\begin{itemize}
\item Case $f \equiv true$  then $R^+(f) = (f,f, true,false)$;

\item Case $f \equiv false$ then $R^+(f) = (f,f,true,false)$;

\item Case $f \equiv X$; then $R^+(f) =(true,X,X,false)$ when $X \in S_0$, $(false, X,true,X)$ when $X \in S_1$ and $(\bot, X,true,false)$ otherwise;

\item Case $f \equiv f_1 \wedge f_2$, assuming that $R^+(f_i) = (b_i,f'_i,g_0^i,g_1^i)$. \\
If $b_1 = true$ and $b_2 = true$, then $R^+(f) = (true, f_1' \wedge f_2',g_0^1 \wedge g_0^2,false)$. \\
If $b_1 = false$ and $b_2 \neq false$, then $R^+(f) = (false, f_1',true,g_1^1)$. \\
If $b_1 \neq false$ and $b_2 = false$ then $R^+(f) = (false,f_2',true,g_1^2)$. \\
If $b_1 = false$ and $b_2 = false$ then
$R^+(f) = (false, f_1',true,g_1^1)$ when $|g_1^1| < |g_1^2|$ and $(false,f_2',true,g_1^2)$ otherwise.

If $b_1 = \bot$ and $b_2 = \bot$ then $R^+(f) = (\bot, f_1' \wedge f_2',true,false)$;

\item Case $f \equiv f_1 \vee f_2$,  assuming that $R^+(f_i) = (b_i,f'_i,g_0^i,g_1^i)$.\\ 
If $b_1 = false$ and $b_2 = false$, then $R^+(f) = (false, f_1' \vee f_2',true,g_1^1\vee g_1^2)$.\\
If $b_1 = true$ and $b_2 \neq true$, then $R^+(f) = (true, f_1', g_0^1,false)$. \\
If $b_1 \neq true$ and $b_2 = true$ then $R^+(f) = (true,f_2',g_0^2,false)$. \\
If $b_1 = true$ and $b_2 = true$ then $R^+(f) = (true, f_1',g_0^1,false)$ when $|g_0^1| < |g_0^2|$ and $(true,f_2',g_0^2,false)$ otherwise. \\
If $b_1 = \bot$ and $b_2 = \bot$ then $R^+(f) = (\bot, f_1' \vee f_2',true,false)$.
\end{itemize}

The assignment $\psi^e := R(\psi^e(\rho_0(S_0) \cup \rho_1(S_1)))$ can be replaced by an assignment
$(b,\psi^e,g_0,g_1) := R^+(\psi^e)$, and the extension to $S_0$ and $S_1$ can then be replaced by the
following code:
\[
\begin{array}{l}
\If b = true \Then S_0 := S_0 \cup \{ X^e \} \\
\If b = false \Then S_1 := S_1 \cup \{ X^e \} \\
\end{array}
\]
Note that $R^+$ can probably also be implemented at the level of PBES expressions. This results in the following adapted version, which is the default in \texttt{pbessolve}.

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_2$}(\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
\colorbox{lightgray}{$%
S_0:= \emptyset $}\\
\colorbox{lightgray}{$%
S_1:= \emptyset $}\\
\While todo\neq \emptyset \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad \colorbox{lightgray}{$%
(b,\psi^e,g_0,g_1) := R^+(\psi^e) $}\\
\qquad \colorbox{lightgray}{$%
\If b = true \Then$}\\
\qquad \colorbox{lightgray}{$ \qquad S_0 := S_0 \cup \{ X^e \} $}\\
\qquad \colorbox{lightgray}{$ \qquad \psi^e := g_0 $}\\
\qquad \colorbox{lightgray}{$%
\If b = false \Then$}\\
\qquad \colorbox{lightgray}{$ \qquad S_1 := S_1 \cup \{ X^e \} $}\\
\qquad \colorbox{lightgray}{$ \qquad \psi^e := g_1 $}\\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\colorbox{lightgray}{$V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1)$} \\
\Return (V, E)
\end{array}%
\end{equation*}%

As a post-processing of the graph constructed by instantiation, the following procedure is used.
It returns a structure graph $(V,E)$ in which information regarding local winning strategies has been exploited to minimise the structure graph, preserving relevant counterexample information. Note: the strategies $\tau_0$ and $\tau_1$ are assumed to be consistent with the sets $S_0$ and $S_1$ (i.e., be a closed, winning strategy for the vertices in those sets).

\begin{equation*}
\begin{array}{l}
\textsc{ExtractMinimalStructureGraph}(V,init,S_0,S_1,\tau_0,\tau_1)\\
todo := \{ init \} \\
done := \emptyset \\
\While todo \neq \emptyset \Do \\
\qquad \Choose u \in todo \\
\qquad todo := todo \setminus \{ u \} \\
\qquad done := done \cup \{ u \} \\
\qquad \If (u \in S_0 \land d(u) = \blacktriangledown) \\
\qquad \qquad v := \tau_0(u) \\
\qquad \qquad \If v \notin done \Then \\
\qquad \qquad \qquad todo := todo \cup \{ v \} \\
\qquad \Else \If (u \in S_1 \land d(u) = \blacktriangle) \\
\qquad \qquad v := \tau_1(u) \\
\qquad \qquad \If v \notin done \Then \\
\qquad \qquad \qquad todo := todo \cup \{ v \} \\
\qquad \Else \\
\qquad \qquad \For v \in succ(u) \Do \\
\qquad \qquad \qquad \If v \notin done \Then \\
\qquad \qquad \qquad \qquad todo := todo \cup \{ v \} \\
\Return done
\end{array}
\end{equation*}

\subsection{Pruning the todo set}

During the execution of the algorithm, the set $todo$ may contain nodes that can be proven to
be irrelevant, in the sense that the solution of the PBES can already be computed without exploring the irrelevant nodes. To this end we partition the set $todo$ into the sets $todo$ and $irrelevant$ using the function $\textsc{PruneTodo}$. This function is applicable for optimisations 3 and higher. Note that elements from $irrelevant$ may be moved back to $todo$ when new elements are added to the $todo$ set.
The function $\textsc{PruneTodo}$ should be called periodically, not every iteration.

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraphPruneTodo}(\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
\colorbox{lightgray}{$irrelevant := \emptyset$} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
S_0:= \emptyset \\
S_1:= \emptyset \\
\While (\colorbox{lightgray}{$todo \setminus irrelevant$}) \neq \emptyset
\wedge X_{init}(e_{init}) \notin S_0 \cup S_1
\Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad (b,\psi^e) := R^+(\psi^e) \\
\qquad \If b = true \Then S_0 := S_0 \cup \{ X^e \} \\
\qquad \If b = false \Then S_1 := S_1 \cup \{ X^e \} \\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo := todo\cup (\mathrm{occ}(\psi ^{e})\setminus (\colorbox{lightgray}{$discovered \setminus irrelevant$})) \\
\qquad discovered := discovered\ \cup \mathrm{occ}(\psi^e) \\
\qquad \colorbox{lightgray}{$irrelevant := irrelevant \setminus \mathrm{occ}(\psi^e)$} \\
\qquad \colorbox{lightgray}{$irrelevant := \textsc{PruneTodo}(init, todo, irrelevant) $}\\
V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1) \\
\Return(V, E),
\end{array}
\end{equation*}

where \textsc{PruneTodo} is defined as

\begin{equation*}
\begin{array}{l}
\textsc{PruneTodo}(init, todo, irrelevant) \\ 
todo' := \{ init \} \\
done' := \{ init \} \\
new\_todo := \emptyset \\
\While todo' \neq \emptyset \Do \\
\qquad \Choose u \in todo' \\
\qquad todo' := todo' \setminus \{ u \} \\
\qquad done' := done' \cup \{ u \} \\
\qquad \If d(u) = \bot \land succ(u) = \emptyset \Then\\
\qquad \qquad new\_todo := new\_todo \cup \{ u \} \\
\qquad \Else \If u \notin S_0 \cup S_1 \Then \\ 
\qquad\qquad todo' := todo' \cup (succ(u) \setminus done') \\
new\_todo := new\_todo \cap (todo \cup irrelevant) \\
new\_irrelevant := (todo \cup irrelevant) \setminus new\_todo \\
\Return new\_todo, new\_irrelevant
\end{array}
\end{equation*}


\subsection{Optimisations 3 and higher}

When the computation of $SG^0(\varphi,\psi,r)$ finishes and the subgraph represented by $SG^0$ 
is effectively solved (which is the case if it represents $true$ or $false$), we can use these
results to solve other variables by propagating the information in $S_0$ and $S_1$ to
the structure graph constructed so far. The modification is minor, re-using the
attractor set computation (and setting of a winning strategy) that is also part of Zielonka's 
recursive algorithm. More
specifically, we can ensure that $S_0$ and $S_1$ are closed under the appropriate
attractor set computations. Furthermore, if the initial vertex belongs to either
$S_0$ or $S_1$, we can terminate the search. This leads to the following modified algorithm,
that is used as a basis for all further optimisations:

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraphEarlyTermination}(\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
S_0, \tau_0 := \emptyset, \emptyset \\
S_1, \tau_1 := \emptyset, \emptyset \\
\While todo\neq \emptyset
\colorbox{lightgray}{$\wedge X_{init}(e_{init}) \notin S_0 \cup S_1 $}
\Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad (b,\psi^e) := R^+(\psi^e) \\
\qquad \If b = true \Then S_0 := S_0 \cup \{ X^e \}\\
\qquad \If b = false \Then S_1 := S_1 \cup \{ X^e \}\\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\qquad \colorbox{lightgray}{$S_0, S_1, \tau_0, \tau_1 := apply\_attractor(S_0, S_1, \tau_0, \tau_1)$}  \text{(executed periodically)} \\
%\qquad \colorbox{lightgray}{$W_0, W_1 := apply\_attractor(S_0, S_1)$} \\
%\qquad \colorbox{Apricot}{$\For v \in (W_0 \cup W_1) \setminus (S_0 \cup S_1)$}\\
%\qquad \colorbox{Apricot}{$\qquad \If (v \in W_0 \wedge d(v) = \blacktriangledown) \Then \tau_0(v) := \tau(v)$}\\
%\qquad \colorbox{Apricot}{$\qquad \If (v \in W_1 \wedge d(v) = \blacktriangle) \Then \tau_1(v) := \tau(v)$}\\
%\qquad \colorbox{lightgray}{$S_0, S_1 := W_0, W_1$} \\
V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1) \\
\Return(V, E),
\end{array}
\end{equation*}

The optimizations 3 until 7 each use a different function for $apply\_attractor$. Attractor
computations are expensive operations, so in \texttt{pbessolve} the function $apply\_attractor$ is called only periodically.

\subsection{Optimisation~3}

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_{3}$(}\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
S_0:= \emptyset \\
S_1:= \emptyset \\
\While todo \neq \emptyset \wedge X_{init}(e_{init}) \notin S_0 \cup S_1 \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad (b,\psi^e) := R^+(\psi^e) \\
\qquad \If b = true \Then S_0 := S_0 \cup \{ X^e \}\\
\qquad \If b = false \Then S_1 := S_1 \cup \{ X^e \}\\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\qquad \colorbox{lightgray}{$S_0, \tau_0 := \textsc{AttrDefaultWithTau}(S_0, 0, \tau_0) $}
\text{(executed periodically)} \\
\qquad \colorbox{lightgray}{$S_1, \tau_1 := \textsc{AttrDefaultWithTau}(S_1, 1, \tau_1) $}
\text{(executed periodically)} \\
V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1) \\
\Return(V, E),
\end{array}
\end{equation*}

Further needless instantiation can be avoided by utilising the attractor
strategies that are set when extending $S_0$ and $S_1$ by, once in a while, computing
which vertices are still reachable from $X_\textit{init}(e_\textit{init})$, ignoring
edges emanating from a vertex that are not part of the strategy for that vertex (if the
strategy is set). This reachability analysis may be combined with a cheap algorithm that
detects whether the game can in fact already be solved (see e.g. optimisation 4). 

% The \textsc{AttrDefault} computations can be expensive. They can be optionally replaced by a
% cheaper, less powerful version:

% \begin{equation*}
% \begin{array}{l}
% \qquad \If b = true \Then S_0 := \colorbox{lightgray}{$
% \textsc{AttrCheap}(S_0, X^e, 0)$} \\
% \qquad \If b = false \Then S_1 := \colorbox{lightgray}{$
% \textsc{AttrCheap}(S_1, X^e, 1) $}\\
% \end{array}
% \end{equation*}

% Even this attractor set computation may dominate the runtime, since it may potentially
% be called every iteration of the while loop. Therefore this attractor set computation is
% exclusively enabled with optimization 3.

\paragraph{Note on computing winning strategies.} The winning strategy can be set by extending
it using the attractor strategy that is computed while
computing $Attr_0(S_0 \cup \{X^e\})$ and $Attr_1(S_1 \cup \{X^e\})$.

\subsection{Optimisation 4}
Several simple algorithms exist that can solve partial structure graphs. An example
algorithm is, for instance, the algorithm that computes whether is an
\emph{odd-rank} dominated conjunctive loop or an \emph{even-rank} dominated disjunctive loop.
The \texttt{pbes2bool} optimisation, implemented at the level of the structure graph is as
follows (it typically assumes that the set $U$ contains all fully explored vertices, $r$ is
the rank function, $\textsf{dom}(r)$ yields the set of vertices with a rank associated to
them; the function $\mathsf{parity}(p) = \up$ when $p$ is odd, and $\down$ otherwise).
%\begin{equation*}
%\begin{array}{l}
%\text{\textsc{FindLoop}}(U,v,w,p,\text{visited})\\  %w is reachable from v
%\If w = v \textbf{ then return } true \\
%\If v \text{ is underfined } \textbf{then } v := w \\
%\If d(w) \in\{\top,\bot\} \textbf{ then return } false \\
%\If w \in \mathsf{dom}(r) \text{ and } r(w) \neq p \textbf{ then return } false \\
%\If w \in \mathsf{keys}(\text{visited}) \textbf{ then return } \text{visited}(w) \\
%\If w \in U \Then \\
%\qquad \text{visited}(w) := false\\
%\qquad \If (w \in \mathsf{dom}(d) \Rightarrow d(w) = \textsf{parity}(p)) \Then \\
%\qquad \qquad b := \bigvee\limits_{u \in \{ u' \mid w \to u' \}} \textsc{FindLoop}(U,v, u, p, \text{visited}) \\
%\qquad \textbf{else } \\
%\qquad \qquad b := \bigwedge\limits_{u \in \{ u' \mid w \to u' \}} \textsc{FindLoop}(U,v, u, p, \text{visited}) \\
%\qquad \text{visited}(w) := b\\
%\qquad \Return b\\
%%\textbf{return $false$}
%\end{array}
%\end{equation*}

\begin{equation*}
\begin{array}{l}
\text{\textsc{FindLoop}}(U,v,w,p,\text{visited})\\  %w is reachable from v
\If d(w) \in\{\top,\bot\} \textbf{ then return } false \\
\If w \in \mathsf{dom}(r) \text{ and } r(w) \neq p \textbf{ then return } false \\
\If w \in \mathsf{keys}(\text{visited}) \textbf{ then return } \text{visited}(w) \\
\If w \in U \Then \\
\qquad \text{visited}(w) := false\\
\qquad \If d(w) = \bot \lor d(w) = p \bmod 2 \Then \\
\qquad \qquad \For u \in succ(w) \Do \\
\qquad \qquad \qquad \If u = v \lor \textsc{FindLoop}(U,v, u, p, \text{visited}) \Then \\
\qquad \qquad \qquad \qquad \colorbox{Apricot}{$ \If u = v \Then \tau(w) := v \Space \Else \tau(w) := u $} \\
\qquad \qquad \qquad \qquad visited(w) := true \\
\qquad \qquad \qquad \qquad \Return true \\
\qquad \textbf{else } \\
\qquad \qquad \Return false \\
%\qquad \qquad b := \bigwedge\limits_{u \in \{ u' \mid w \to u' \wedge u' \neq v \}} \textsc{FindLoop}(U,v, u, p, \text{visited}) \\
\textbf{return $false$}
\end{array}
\end{equation*}

The routine $\textsc{FindLoop}(U,v,w,r(v),\text{visited})$ finds a
$r(v)$-ranked (possibly tree-like) loop starting in $v$, within a set of vertices
$U$. Note that in the above routine, parameter $w$ represents the `current' vertex,
whereas $v$ represents the vertex from which the search was initiated.  Note that 
parameter $p$ fulfils the role
of the fixpoint sign $\sigma$ in the original algorithm, parameter $v$ fulfils
the role of $X_k(e)$ and $w$ fulfils the role of $\phi$. 

The procedure $\textsc{FindLoops}$ can be called from within the main algorithm; it searches for loops in the structure graph currently constructed.
\begin{equation*}
\begin{array}{l}
\text{\textsc{FindLoops}}(discovered, todo, S_0, S_1, \tau_0, \tau_1)\\  %w is reachable from v
done := discovered \setminus todo \\
\text{visited} := [] \\
b_0,b_1 := false,false \\
\textbf{for } u \in done \cap \textsf{dom}(r) \Do \\
\qquad \If u \notin \textsf{keys}(\text{visited}) \Then \text{visited}(u) := false\\
\qquad b := \textsc{FindLoop}(done, u, u, r(u), \text{visited}) \\
\qquad \text{visited}(u) := b\\
\qquad \If b \Then \\
\qquad \qquad \If r(u) \bmod 2 = 0 \Then S_0,b_0 := S_0 \cup \{u\}, true\\
\qquad\qquad \textbf{else } S_1,b_1 := S_1 \cup \{u\}, true\\
\If b_0 \Then S_0 := \textsc{AttrDefaultWithTau}(S_0, 0, \tau_0)\\ 
\If b_1 \Then S_1 := \textsc{AttrDefaultWithTau}(S_1, 1, \tau_1)\\ 
\Return S_0, S_1, \tau_0, \tau_1
\end{array}
\end{equation*}
The above optimisation can be integrated in the algorithm as follows.

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_{4}$(}\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
S_0:= \emptyset \\
S_1:= \emptyset \\
\While todo \neq \emptyset \wedge X_{init}(e_{init}) \notin S_0 \cup S_1 \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad (b,\psi^e) := R^+(\psi^e) \\
\qquad \If b = true \Then S_0 := S_0 \cup \{ X^e \} \\
\qquad \If b = false \Then S_1 := S_1 \cup \{ X^e \} \\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\qquad \colorbox{lightgray}{$%
S_0, S_1, \tau_0, \tau_1 := \text{\textsc{FindLoops}}(discovered, todo, S_0, S_1, \tau_0, \tau_1) $} \text{(executed periodically)} \\
V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1) \\
\Return (V, E)
\end{array}%
\end{equation*}%

Note that in the call to \textsc{FindLoops} we would like to pass the argument $done = discovered \setminus todo$.
However this set is not available, and it is too expensive to compute. So we pass the larger set $discovered$, and we use $discovered \cap dom(r) = discovered \setminus todo$.

\paragraph{Alternative implementation Optimisation 4}

Optimisation~4 searches for a dominion within the set of vertices with the same priority. That is, for rank $j$ and associated player $\alpha = j \mod 2$, one searches for the largest set of vertices $X_j \subseteq \{ v \in V \mid r(u) = j \vee u \notin dom(r)\}$ satisfying that player $\alpha$ has a winning strategy within $X_j$. That is, it is the largest fixed point of the following transformer (assuming $S_\alpha$ and $S_{1-\alpha}$ are attractor-maximal):
\[
\mathcal{C}_j(X) = 
\begin{array}[t]{ll}
\{ v \in V \setminus S_{1-\alpha} \mid & (r(u) = j \vee u \notin dom(r) ) \wedge {} \\
 & (d(v) = \blacktriangledown \wedge \alpha = 0 \Rightarrow ((X \cup S_\alpha) \cap \{u \in V \mid v \to u \} \neq \emptyset))\\
& \vee
(d(v) = \blacktriangledown \wedge \alpha = 1 \Rightarrow (\{u \in V \mid v \to u \} \subseteq X \cup S_\alpha))\\
& (d(v) = \blacktriangle \wedge \alpha = 1 \Rightarrow ((X \cup S_\alpha) \cap \{u \in V \mid v \to u \} \neq \emptyset))\\
& \vee
(d(v) = \blacktriangle \wedge \alpha = 0 \Rightarrow (\{u \in V \mid v \to u \} \subseteq X \cup S_\alpha))
\}
\end{array}
\]
A simple algorithm computing this is the following. It uses a modified
attractor computation.

\begin{equation*}
\begin{array}{l}
\text{\textsc{FindLoops}}_2(V, S_0, S_1, \tau_0, \tau_1)\\
J := \{ j \mid \exists u \in V \cap dom(r) : r(u) = j \} \\
\colorbox{Apricot}{$S_0, \tau_0 := \textsc{AttrDefaultWithTau}(S_0, 0, \tau_0)$} \\
\colorbox{Apricot}{$S_1, \tau_1 := \textsc{AttrDefaultWithTau}(S_1, 1, \tau_1)$} \\
\textbf{for } j \in J \\
\qquad \alpha := j \bmod 2\\
\qquad U_j := \{u \in V \mid r(u) = j \wedge (\alpha = 0 \Rightarrow d(u) \neq false) 
\wedge (\alpha = 1 \Rightarrow d(u) \neq true) \} \setminus S_{1 - \alpha} \\
\qquad U := U_j \cup S_\alpha\\
\qquad X := \textsc{AttrEqRank}(U, \alpha, V, j) \\
\qquad Y := V \setminus \textsc{AttrDefault}(V \setminus X, 1-\alpha) \\
\qquad \While X \neq Y \textbf{ do }\\
\qquad \qquad X := \textsc{AttrEqRank}(U \cap Y, \alpha, V, j) \\
\qquad \qquad Y := Y \setminus \textsc{AttrDefault}(Y \setminus X, 1-\alpha) \\
\qquad \colorbox{Apricot}{$ \For v \in X \setminus S_{\alpha} \Do $} \\
\qquad \colorbox{Apricot}{$ \qquad \If (\alpha = 0 \land d(u) = \blacktriangledown) \lor (\alpha = 1 \land d(u) = \blacktriangle) \Then $} \\
\qquad \colorbox{Apricot}{$ \qquad \qquad \If v \in U_j \Then \tau_{\alpha}(v) := w \textbf{ with } w \in succ(v) \cap Y $} \\
\qquad \colorbox{Apricot}{$ \qquad \qquad \Else \tau_{\alpha}(v) := \tau(v)$} \\
\qquad S_\alpha := S_\alpha \cup X \\
\qquad \colorbox{Apricot}{$ S_\alpha, \tau_\alpha := \textsc{AttrDefaultWithTau}(S_\alpha, \alpha, \tau_\alpha)$} \\
\Return S_0, S_1, \tau_0,\tau_1
\end{array}
\end{equation*}
where $\textsc{AttrEqRank}$ is a slightly modified version of the original attractor
set computation $\textsc{AttrDefault}$, where only predecessors in $U$ with a rank of 
$j$ are considered:
\begin{equation*}
\begin{array}{l}
\text{\textsc{AttrEqRank}}(A, \alpha, U, j) \\
todo := \bigcup_{u \in A} (%
\colorbox{lightgray}{$ pred^{= j}(u, U) $}%
\setminus A) \\
\While todo \neq \emptyset \Do \\
\qquad \textbf{choose } u \in todo \\
\qquad todo := todo \setminus \{u\} \\
\qquad \If d(u) = \alpha \vee succ(u) \subseteq A \\
\qquad \qquad \colorbox{Apricot}{$ \If d(u) = \alpha \Then \tau
\lbrack u]:=v\With v\in A\cap succ(u) $}\\ 
\qquad \qquad A := A \cup \{u \} \\
\qquad \qquad todo := todo \cup (%
\colorbox{lightgray}{$ pred^{= j}(u, U) $}%
\setminus A)  \\
\Return A
\end{array}
\end{equation*}

where
\begin{eqnarray*}
pred^{= j}(u, U) = \{v \in U \mid (v,u) \in E \wedge (r(v) = j \vee (v \notin dom(r) \wedge d(v) \in \{\blacktriangle,\blacktriangledown\}) \}
\end{eqnarray*}%

The above optimisation can be integrated in the algorithm as follows.

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_{4}$(}\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
S_0:= \emptyset \\
S_1:= \emptyset \\
\While todo \neq \emptyset \wedge X_{init}(e_{init}) \notin S_0 \cup S_1 \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad (b,\psi^e) := R^+(\psi^e) \\
\qquad \If b = true \Then S_0 := S_0 \cup \{ X^e \} \\
\qquad \If b = false \Then S_1 := S_1 \cup \{ X^e \} \\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\qquad \colorbox{lightgray}{$%
S_0, S_1,\tau_0,\tau_1 := \text{\textsc{FindLoops}}_2(V, S_0, S_1, \tau_0, \tau_1) $} \text{(executed periodically)} \\
V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1) \\
\Return (V, E)
\end{array}%
\end{equation*}%

\subsection{Optimisation 5} 

A generalisation of optimisation~4 utilises a so-called \emph{fatal attractor}. Fatal attractors are based on the
observation that those vertices with a dominant priority that are attracted into themselves are won by the player
with the parity of this dominant priority. A simple algorithm exploiting this is the following. It uses a modified
attractor computation.

\begin{equation*}
\begin{array}{l}
\text{\textsc{FatalAttractors}}(V, S_0, S_1, \tau_0, \tau_1)\\
J := \{ j \mid \exists u \in V \cap dom(r) : r(u) = j \} \\
\colorbox{Apricot}{$S_0, \tau_0 := \textsc{AttrDefaultWithTau}(S_0, 0, \tau_0)$} \\
\colorbox{Apricot}{$S_1, \tau_1 := \textsc{AttrDefaultWithTau}(S_1, 1, \tau_1)$} \\
\textbf{for } j \in J \\
\qquad \alpha := j \bmod 2\\
\qquad U_j := \{u \in V \mid r(u) = j \wedge (\alpha = 0 \Rightarrow d(u) \neq false) 
\wedge (\alpha = 1 \Rightarrow d(u) \neq true) \} \setminus S_{1 - \alpha} \\
\qquad U := U_j \cup S_\alpha\\
\qquad X := \textsc{AttrMinRank}(U, \alpha, V, j) \\
\qquad Y := V \setminus \textsc{AttrDefault}(V \setminus X, 1-\alpha) \\
\qquad \While X \neq Y \textbf{ do }\\
\qquad \qquad X := \textsc{AttrMinRank}(U \cap Y, \alpha, V, j) \\
\qquad \qquad Y := Y \setminus \textsc{AttrDefault}(Y \setminus X, 1-\alpha) \\
\qquad \colorbox{Apricot}{$ \For v \in X \setminus S_{\alpha} \Do $} \\
\qquad \colorbox{Apricot}{$ \qquad \If (\alpha = 0 \land d(u) = \blacktriangledown) \lor (\alpha = 1 \land d(u) = \blacktriangle) \Then $} \\
\qquad \colorbox{Apricot}{$ \qquad \qquad \If v \in U_j \Then \tau_{\alpha}(v) := w \textbf{ with } w \in succ(v) \cap Y $} \\
\qquad \colorbox{Apricot}{$ \qquad \qquad \Else \tau_{\alpha}(v) := \tau(v)$} \\
\qquad S_\alpha := S_\alpha \cup X \\
\qquad \colorbox{Apricot}{$ S_\alpha, \tau_\alpha := \textsc{AttrDefaultWithTau}(S_\alpha, \alpha, \tau_\alpha)$} \\
\Return S_0, S_1, \tau_0,\tau_1
\end{array}
\end{equation*}
where $\textsc{AttrMinRank}$ is a slightly modified version of the original attractor
set computation $\textsc{AttrDefault}$, where only predecessors in $U$ with a rank of at least
$j$ are considered:
\begin{equation*}
\begin{array}{l}
\text{\textsc{AttrMinRank}}(A, \alpha, U, j) \\
todo := \bigcup_{u \in A} (%
\colorbox{lightgray}{$ pred^{\geq j}(u, U) $}%
\setminus A) \\
\While todo \neq \emptyset \Do \\
\qquad \textbf{choose } u \in todo \\
\qquad todo := todo \setminus \{u\} \\
\qquad \If d(u) = \alpha \vee succ(u) \subseteq A \\
\qquad \qquad \colorbox{Apricot}{$ \If d(u) = \alpha \Then \tau
\lbrack u]:=v\With v\in A\cap succ(u) $}\\ 
\qquad \qquad A := A \cup \{u \} \\
\qquad \qquad todo := todo \cup (%
\colorbox{lightgray}{$ pred^{\geq j}(u, U) $}%
\setminus A)  \\
\Return A
\end{array}
\end{equation*}

where
\begin{eqnarray*}
pred^{\geq j}(u, U) = \{v \in U \mid (v,u) \in E \wedge (r(v) \ge j \vee (v \notin dom(r) \wedge d(v) \in \{\blacktriangle,\blacktriangledown\}) \}
\end{eqnarray*}%

The above optimisation can be integrated in the algorithm as follows.

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_{5}$(}\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
S_0:= \emptyset \\
S_1:= \emptyset \\
\While todo \neq \emptyset \wedge X_{init}(e_{init}) \notin S_0 \cup S_1 \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad (b,\psi^e) := R^+(\psi^e) \\
\qquad \If b = true \Then S_0 := S_0 \cup \{ X^e \} \\
\qquad \If b = false \Then S_1 := S_1 \cup \{ X^e \} \\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\qquad \colorbox{lightgray}{$%
S_0, S_1,\tau_0,\tau_1 := \text{\textsc{FatalAttractors}}(V, S_0, S_1, \tau_0, \tau_1) $} \text{(executed periodically)} \\
V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1) \\
\Return (V, E)
\end{array}%
\end{equation*}%

\subsection{Optimisation 6}
Optimisation 6 is a slightly different fatal attractor computation that is very close to the
original one by <NAME>, <NAME>-<NAME>, and <NAME>.

\begin{equation*}
\begin{array}{l}
\text{\textsc{AttrMinRankOriginal}}(A, \alpha, U, j) \\
\{\textit{compute the $\alpha$-min attractor into the set $A$, restricted to vertices in $U$}\}\\
todo := \bigcup_{u \in A} (%
pred^{\geq j}(u, U) ) \\
X := \{ u \in todo \cap A \mid d(u) = \alpha \vee succ(u) \subseteq A \} \\
\While todo \neq \emptyset \Do \\
\qquad \textbf{choose } u \in todo \\
\qquad todo := todo \setminus \{u\} \\
\qquad \If d(u) = \alpha \vee succ(u) \subseteq A \cup X \\
\qquad \qquad \colorbox{Apricot}{$ \If d(u) = \alpha \Then \tau
\lbrack u]:=v\With v\in (A \cup X) \cap succ(u) $}\\ 
\qquad \qquad X := X \cup \{u \} \\
\qquad \qquad todo := todo \cup (%
pred^{\geq j}(u, U) \setminus X)  \\
\Return X
\end{array}
\end{equation*}

\begin{equation*}
\begin{array}{l}
\textsc{FatalAttractorsOriginal}(V, S_0, S_1, \tau_0, \tau_1)\\
J := \{ j \mid \exists u \in V : r(u) = j \} \\
\colorbox{Apricot}{$S_0, \tau_0 := \textsc{AttrDefaultWithTau}(S_0, 0, \tau_0)$} \\
\colorbox{Apricot}{$S_1, \tau_1 := \textsc{AttrDefaultWithTau}(S_1, 1, \tau_1)$} \\
\textbf{for } j \in J \\
\qquad \alpha := j \bmod 2\\
\qquad U_j := \{u \in V \mid r(u) = j \wedge (\alpha = 0 \Rightarrow d(u) \neq false) 
\wedge (\alpha = 1 \Rightarrow d(u) \neq true) \} \setminus S_{1-\alpha} \\
\qquad X := \emptyset \\
\qquad \While U_j \neq \emptyset \wedge U_j \neq X \\ 
\qquad \qquad X := U_j\\
\qquad \qquad Y := \textsc{AttrMinRankOriginal}(X \cup S_\alpha, \alpha, V, j) \\
\qquad \qquad \If U_j \subseteq Y \\
\qquad \qquad \qquad \colorbox{Apricot}{$ \For v \in Y \setminus S_{\alpha} \Do $} \\
\qquad \qquad \qquad \colorbox{Apricot}{$ \qquad \If (\alpha = 0 \land d(u) = \blacktriangledown) \lor (\alpha = 1 \land d(u) = \blacktriangle) \Then $} \\
\qquad \qquad \qquad \colorbox{Apricot}{$ \qquad \qquad \If v \in U_j \Then \tau_{\alpha}(v) := w \textbf{ with } w \in succ(v) \cap Y $} \\
\qquad \qquad \qquad \colorbox{Apricot}{$ \qquad \qquad \Else \tau_{\alpha}(v) := \tau(v) $} \\
\qquad \qquad \qquad S_\alpha := S_\alpha \cup Y \\

\qquad\qquad\qquad \colorbox{Apricot}{$S_\alpha, \tau_\alpha := \textsc{AttrDefaultWithTau}(S_\alpha, \alpha, \tau_\alpha)$} \\
\qquad \qquad \qquad \textbf{break} \\
\qquad \qquad \textbf{else }\\
\qquad \qquad \qquad U_j := U_j \cap Y\\
\Return S_0, S_1, \tau_0,\tau_1
\end{array}
\end{equation*}

Note for setting strategy: when $U_j \subseteq Y$, we should set a strategy for all vertices $v \in U_j \setminus S_\alpha$ as follows: for each $v \in V_\alpha \cap (U_j \setminus S_\alpha)$, define $\tau(v) :\in \{ u \in Y \mid v \to u \}$.

\subsection{Optimisation 7}
In optimisation 7 the sets $S_0$ and $S_1$ are extended by solving a partial game.

\begin{equation*}
\begin{array}{l}
\textsc{PbesinstStructureGraph$_{7}$(}\mathcal{E}, X_{init}(e_{init}), R) \\ 
init:=R(X_{init}(e_{init})) \\
todo:=\{init\} \\
discovered:=\{init\} \\
(V,E) :=(\emptyset ,\emptyset ) \\ 
S_0:= \emptyset \\
S_1:= \emptyset \\
\While todo \neq \emptyset \wedge X_{init}(e_{init}) \notin S_0 \cup S_1 \Do \\ 
\qquad \Choose X_{k}(e)\in todo \\ 
\qquad todo:=todo\ \backslash \ \{X_{k}(e)\} \\ 
\qquad \psi ^{e}:=R(\varphi _{k}[d_{k}:=e]) \\ 
\qquad \psi^e := \Space \If \sigma_k = \mu \Then R(\psi^e[X^e := false])
\Space \Else R(\psi^e[X^e := true]) \\
\qquad (b,\psi^e) := R^+(\psi^e) \\
\qquad \If b = true \Then S_0 := S_0 \cup \{ X^e \} \\
\qquad \If b = false \Then S_1 := S_1 \cup \{ X^e \} \\
\qquad (V,E) := (V,E) \cup SG^{0}(X^{e},\psi ^{e}) \\ 
\qquad todo:=todo\cup (\mathrm{occ}(\psi ^{e})\setminus discovered) \\
\qquad discovered:=discovered\ \cup \mathrm{occ}(\psi ^{e}) \\
\qquad \colorbox{lightgray}{$
S_0, S_1,\tau_0,\tau_1 := \textsc{PartialSolve}(V,todo,S_0,S_1, \tau_0, \tau_1) $} \text{(executed periodically)} \\
V := \textsc{ExtractMinimalStructureGraph}(V, init, S_0, S_1, \tau_0, \tau_1) \\
\Return (V, E)
\end{array}
\end{equation*}
where \textsc{PartialSolve} is defined as

\begin{equation*}
\begin{array}{l}
\textsc{PartialSolve}(V,todo,S_0,S_1, \tau_0, \tau_1)\\
\{\textit{use the solver to compute an over and underapproaximation}\}\\
\colorbox{Apricot}{$S_0, \tau_0 := \textsc{AttrDefaultWithTau}(S_0, 0, \tau_0)$} \\
\colorbox{Apricot}{$S_1, \tau_1 := \textsc{AttrDefaultWithTau}(S_1, 1, \tau_1)$} \\
(W_0,W_1) := \textsc{SolveRecursive}(V \setminus (S_1 \cup \textsc{AttrDefaultNoStrategy}(S_0 \cup todo,0)))\\

\colorbox{Apricot}{$ \For v \in W_1 \setminus S_{1} \Do $} \\
\colorbox{Apricot}{$ \qquad \If d(u) = \blacktriangle \Then \tau_{1}(v) := \tau(v) $} \\
S_1 := S_1 \cup W_1\\

(W_0,W_1) := \textsc{SolveRecursive}(V \setminus (S_0 \cup \textsc{AttrDefaultNoStrategy}(S_1 \cup todo,1)))\\
\colorbox{Apricot}{$ \For v \in W_0 \setminus S_{0} \Do $} \\
\colorbox{Apricot}{$ \qquad \If d(u) = \blacktriangledown \Then \tau_{0}(v) := \tau(v) $} \\
S_0 := S_0 \cup W_0 \\
\Return S_0, S_1, \tau_0,\tau_1
\end{array}
\end{equation*}

\end{document}
