During a normal execution a program visits one location after another and
changes state with every transition. The configruation at a given point of the
execution  can be described by tuple of location and assignment. Simulating
every possible run of a program from every possible starting state is
impossible: First, the number of starting states is infinte; second the
program is not guaranteed to terminate and hence the simulation of a specific
run might not terminate either. 
For non-deterministic and probabilistic programs, the problem get's even more
complex, since the transition taken does not only depend on the current state
but also on the answer of some oracle, determining possibly the transition or the
value variables after the transition.
So, instead of simulating every single possible run, it would be nice to treat
\enquote{similar} states as one, for sake of execution. Instead of processing a
single assignment, the space of all possible assignments at a location is
described by a set of constraints (polyhedron).
This approach is very similar to the computation of invariants, where the set of
possible assignment each location in a given program is iteratively updated by
propagating the transition constraints throught the program until a fixpoint is
found. \todo{citation} However, during evaluation one starts at a specific
configuration and \textit{unfolds} transitions recursively, without influency
neighboring paths. The result is a (possibly still infinite) tree, representing
all possible runs.
This tree was formalized as an evaluation tree for \gls{chc} by \todo{citation}.
In this thesis the evaluation tree is defined for \gls{pip} instead, giving the
opportunity to explicitly handle costs, and probability and staying closer to
KoAT's formalisms. 
\begin{definition}[Evaluation Tree]
\end{definition}
\begin{example}
    \todo{picture of an evaluation tree for a chosen example program.}
\end{example}
As already stated above, the evaluation tree is possibly infinite and computing
the whole evaluation tree would be very inefficient. For example versions can
repeat and it would be better to loop back to the already existing version
instead of continuing the evaluation. This by it self is unfortunaetly not
enough. 
Comparing set's of constraints for equality is hard \todo{citation} and hence
detecting repetitions impossible to do efficiently. One could recur to
structural equality instead, and just accept the impreciseness, but even then,
nothing guarantees that the infinite paths in the evaluation tree have repeating
versions. 
\begin{example}
    \todo{example of loop incrementing the bound by one in every step.}
\end{example}
Instead a version is abstracted to a less tight but easy to compare
representation. Choosing only a finite number of abstractions and guaranteeing
that every infinite path is abstracted at some point, will guarantee the
termination of the evaluation. 
\begin{definition}[Abstraction]
\todo{definition}
\end{definition}
In general, the abstraction can be arbitrary as long as the properties above are
satisfied. One possible abstraction, the so called property-based abstraction, 
described in \Sref{sec:property-based-abstraction}. For now, the exact details
of abstraction will be omitten. Just know that altough necessary for the
construction to work, they are expensive and loose precision.
As stated above, it must be guaranteed that every infinite path is abstracted
often enough, so that it collapses onto itself\todo{rewrite}. The easiest way
would be to just abstract at every location. This however would result in a very
imprecise evaluation and be very expensive, since the abstraction is called after
every unfolding step.
\todo{loop head abstraction}
\subsection{Property based abstraction}
\label{sec:property-based-abstraction}
\citeauthor{Domenech19} described the property based abstraction that
will be used for this algorithm. The idea is the following: the solution space
is cut into pieces by a finite number of constraints, the so called properties. 
Then the abstraction computes which of those properties, are entailed by the
version. Those are chosen as abstract representation for the version. Since the
number of properties is finite, the powerset of properties is finite as well and
hence the number of all possible abstractions is too. 
Also the abstraction is entailed by the version. \todo{rewrite}
\begin{definition}[Property based abstraction].
    \todo{definition}
\end{definition}
\begin{example}
    \todo{picture with properties}
\end{example}
Every abstraction is expensive, because it requires numerous entailement checks
(depending on the number of properties), wich require each a call to a
SAT-checker. The more properties are chose the more precise the abstraction
get's but the more expensive the computation is. Choosing the relevant
properties for the loops is done heuristically and will be described in the
following subsection. 
\subsection{Choosing properties heuristically}
\todo{describe the original heuristic}
\todo{find a better heuristic?}