Transition Systems

Semantics

We define a (global) transition relation <math>\mathit{next}</math> as follows: <math>

 \begin{array}[t]{@{}l@{}}
 ((x \cdot \mathit{xs}), (y \cdot \mathit{ys})) \in \mathit{next} \text{ iff } \\[\jot]
 \qquad\qquad
   \exists p \in \mathit{Proc} :  
   \begin{array}[t]{@{}r@{}l@{}}
     &\mathit{step}_p(x, y) \land \mathit{xs} = \mathit{ys}  \\[\jot]
     \mathrel{\lor}& \exists q \in \mathit{Proc}: 
     \begin{array}[t]{@{}r@{}l@{}}
       &\mathit{call}^p_q(x, y) \land (x \cdot \mathit{xs}) = \mathit{ys} \\[\jot]
       \mathrel{\lor} &\mathit{return}^p_q(x, z, y) \land \mathit{xs} = (z \cdot \mathit{ys})
     \end{array}
   \end{array}
\end{array}

</math>