Difference between revisions of "Transition Systems"
From Termination-Portal.org
Jump to navigationJump to searchJ.waldmann (talk | contribs) (Created page with "Category: Categories") |
|||
| Line 1: | Line 1: | ||
[[Category: Categories]] | [[Category: Categories]] | ||
| + | |||
| + | === 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> | ||
Revision as of 09:03, 16 June 2014
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>
