Difference between revisions of "Transition Systems"

Latest revision as of 12:33, 9 May 2020

Syntax and semantics of the format are presented in [1].

@@ Line 1: / Line 1: @@
 [[Category: Categories]]
-=== Semantics ===
+Syntax and semantics of the format are presented in [https://www.microsoft.com/en-us/research/publication/termcomp-proposal-pushdown-systems-as-a-model-for-programs-with-procedures/].
-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>