Changeset 2616

Timestamp:

Feb 6, 2013, 4:07:13 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Papers/itp-2013/ccexec.tex (modified) (2 diffs)

Papers/itp-2013/ccexec.tex

@@ -872 +872 @@
 \begin{condition}[Case \texttt{cl\_call}]
  For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
- $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taaf_1$ of type
-$(\texttt{trace\_any\_any\_free}~s_2~s_b)$, a $taaf_2$ of type
+ $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taa_1$ of type
+$(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type
 $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
 $s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
@@ -888 +888 @@
 as usual.
 
-\begin{verbatim}
-definition status_simulation ≝
-      | cl_return ⇒
-        (* 
-             st1
-            / ↓
-           | st1'----------S,L------------\
-           S   \                           \
-            \   \-----R-------\            |      
-             \                 |           |
-             st2 →taa→ st2_ret |           |
-                          ↓   /            |
-                     st2_after_ret →taaf→ st2'
-
-           we also ask that st2_after_ret be not labelled if the taaf tail is
-           not empty
-        *)
-        ∃st2_ret,st2_after_ret,st2'.
-        ∃taa2 : trace_any_any … st2 st2_ret.
-        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
-        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
-        as_classifier … st2_ret cl_return ∧
-        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
-        ret_rel … sim_status_rel st1' st2_after_ret ∧
-        label_rel … st1' st2'
-      ]
-    ].
-\end{verbatim}
+\begin{condition}[Case \texttt{cl\_return}]
+ For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
+ $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a $taa$ of type
+$(\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type
+$(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
+$s_a$ is classified as a \texttt{cl\_return},
+$s_1 \mathcal{C} s_b$, the predicate
+$(\texttt{as\_execute}~s_b~s_a)$ holds,
+$s_1' \mathcal{R} s_a$ and
+$s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
+$taaf$ is non empty, or $s_a$ is not \texttt{as\_costed}.
+\end{condition}
+
+Similarly to the call condition, to simulate a return we can perform a
+sequence of silent actions before and after the return statement itself.
+The old and the new statements after the return must be $\mathcal{R}$-related,
+to grant that they returned to corresponding calls.
+The two initial and final states must be $\mathcal{S}$-related
+as usual and, moreover, they must exhibit the same labels. Finally, when
+the suffix is non empty we must take care of not inserting a new
+unmatched cost emission statement just after the return statement.
+
 \begin{comment}
 \begin{verbatim}