Changeset 2627
- Timestamp:
- Feb 6, 2013, 10:06:05 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/itp-2013/ccexec.tex
r2626 r2627 1000 1000 \end{comment} 1001 1001 1002 \begin{theorem}[\texttt{status\_simulation\_produce\_tlr}] 1003 For every $s_1,s_1',s_{2_b},s_2$ s.t. 1004 there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and a 1005 $\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and 1006 $s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t. 1007 there is a $\texttt{trace\_label\_return}~s_{2_b}~s_{2_m}$ called $tlr_2$ and 1008 there is a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$ 1009 s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$, 1010 and $\texttt{tlr\_rel}~tlr_1~tlr_2$ 1011 and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and 1012 $s_1' \mathcal{R} s_{2_m}$. 1013 \end{theorem} 1014 \begin{theorem}[\texttt{status\_simulation\_produce\_tll}] 1015 For every $s_1,s_1',s_{2_b},s_2$ s.t. 1016 there is a $\texttt{trace\_label\_label}~f~s_1~s_1'$ called $tll_1$ and a 1017 $\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and 1018 $s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t. 1019 \begin{itemize} 1020 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ 1021 and a trace $\texttt{trace\_label\_label}~b~s_{2_b}~s_{2_m}$ called $tll_2$ 1022 and a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t. 1023 $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and 1024 $s_1' \mathcal{R} s_{2_m}$ and 1025 $\texttt{tll\_rel}~tll_1~tll_2$ and 1026 if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$ 1027 \item else there exists $s_2'$ and a 1028 $\texttt{trace\_label\_label}~b~s_{2_b}~s_2'$ called $tll_2$ such that 1029 $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and 1030 $\texttt{tll\_rel}~tll_1~tll_2$. 1031 \end{itemize} 1032 \end{theorem} 1033 1034 \begin{corollary} 1035 For every $s_1,s_1',s_2$ s.t. 1036 there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and 1037 $s_1 (\mathcal{L} \cap \mathcal{S}) s_2$ 1038 there exists $s_{2_m},s_2'$ s.t. 1039 there is a $\texttt{trace\_label\_return}~s_2~s_{2_m}$ called $tlr_2$ and 1040 there is a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$ 1041 s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$, 1042 and $\texttt{tlr\_rel}~tlr_1~tlr_2$ 1043 and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and 1044 $s_1' \mathcal{R} s_{2_m}$. 1045 \end{corollary} 1046 1047 \begin{comment} 1002 1048 \begin{verbatim} 1003 1049 status_simulation_produce_tlr S1 S2 R … … 1029 1075 tlr_rel … tlr1 tlr2 1030 1076 \end{verbatim} 1077 \end{comment} 1031 1078 1032 1079 \section{Conclusions and future works}
Note: See TracChangeset
for help on using the changeset viewer.