# Changeset 2627 for Papers/itp-2013

Ignore:
Timestamp:
Feb 6, 2013, 10:06:05 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2626 \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 tlr_rel … tlr1 tlr2 \end{verbatim} \end{comment} \section{Conclusions and future works}