Changeset 2627

Timestamp:

Feb 6, 2013, 10:06:05 PM (7 years ago)

Author:

sacerdot

Message:

...

File:

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

Papers/itp-2013/ccexec.tex

@@ -1000 +1000 @@
 \end{comment}
 
+\begin{theorem}[\texttt{status\_simulation\_produce\_tlr}]
+For every $s_1,s_1',s_{2_b},s_2$ s.t.
+there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and a
+$\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and
+$s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t.
+there is a $\texttt{trace\_label\_return}~s_{2_b}~s_{2_m}$ called $tlr_2$ and
+there is a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$
+s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$,
+and $\texttt{tlr\_rel}~tlr_1~tlr_2$
+and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
+$s_1' \mathcal{R} s_{2_m}$.
+\end{theorem}
+\begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
+For every $s_1,s_1',s_{2_b},s_2$ s.t.
+there is a $\texttt{trace\_label\_label}~f~s_1~s_1'$ called $tll_1$ and a
+$\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and
+$s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t.
+\begin{itemize}
+ \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
+       and a trace $\texttt{trace\_label\_label}~b~s_{2_b}~s_{2_m}$ called $tll_2$
+       and a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t.
+       $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
+       $s_1' \mathcal{R} s_{2_m}$ and
+       $\texttt{tll\_rel}~tll_1~tll_2$ and
+       if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$
+ \item else there exists $s_2'$ and a 
+       $\texttt{trace\_label\_label}~b~s_{2_b}~s_2'$ called $tll_2$ such that
+       $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
+       $\texttt{tll\_rel}~tll_1~tll_2$.
+\end{itemize}
+\end{theorem}
+
+\begin{corollary}
+For every $s_1,s_1',s_2$ s.t.
+there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and
+$s_1 (\mathcal{L} \cap \mathcal{S}) s_2$
+there exists $s_{2_m},s_2'$ s.t.
+there is a $\texttt{trace\_label\_return}~s_2~s_{2_m}$ called $tlr_2$ and
+there is a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$
+s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$,
+and $\texttt{tlr\_rel}~tlr_1~tlr_2$
+and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
+$s_1' \mathcal{R} s_{2_m}$.
+\end{corollary}
+
+\begin{comment}
 \begin{verbatim}
 status_simulation_produce_tlr S1 S2 R
@@ -1029 +1075 @@
   tlr_rel … tlr1 tlr2
 \end{verbatim}
+\end{comment}
 
 \section{Conclusions and future works}