with integer values. Many equivalent mathematical structures have been
developed over the year to formalize integer program. The one used in this
thesis is the integer transition system.

with integer values. Many similar mathematical structures have been developed
over the years to formalize integer program. The one used in this thesis is the
integer transition system.

between those locations. A run inside the the transiton system is a sequence of
configurations -- that is a location and a variable assignment --
where every configuration is reachable via a transition from the previous
configuration. 

between those locations. A run of the program is a sequence of configurations --
that is a location and a state -- where every configuration is reachable via a
transition from the previous configuration. 

same location. Hence it is unclear which transition is taken at a possible
runtime. In order to simulate the program, one must take all possible
transitions into account. 

same location. Hence it is unclear which transition is taken at runtime. The
decision is made by a scheduler. Also guards and assignments of the transition 
might depend on temporary variables that are not set by the state. 
\todo
\example{}

Let's recap the semantics of a probabilistic integer program. 

\subsection{Non-deterministic and probabilistic branching and assignments}
\begin{comment}
    - Probabilistic branching
    - Non-determinstic branching
    - probabilistic assignments (via branching)
    - non-deterministic assignments (via temporary variables)
\end{comment}