Changeset 2627 for Papers/itp-2013


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2626 r2627  
    10001000\end{comment}
    10011001
     1002\begin{theorem}[\texttt{status\_simulation\_produce\_tlr}]
     1003For every $s_1,s_1',s_{2_b},s_2$ s.t.
     1004there 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.
     1007there is a $\texttt{trace\_label\_return}~s_{2_b}~s_{2_m}$ called $tlr_2$ and
     1008there is a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$
     1009s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$,
     1010and $\texttt{tlr\_rel}~tlr_1~tlr_2$
     1011and $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}]
     1015For every $s_1,s_1',s_{2_b},s_2$ s.t.
     1016there 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}
     1035For every $s_1,s_1',s_2$ s.t.
     1036there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and
     1037$s_1 (\mathcal{L} \cap \mathcal{S}) s_2$
     1038there exists $s_{2_m},s_2'$ s.t.
     1039there is a $\texttt{trace\_label\_return}~s_2~s_{2_m}$ called $tlr_2$ and
     1040there is a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taaf$
     1041s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$,
     1042and $\texttt{tlr\_rel}~tlr_1~tlr_2$
     1043and $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}
    10021048\begin{verbatim}
    10031049status_simulation_produce_tlr S1 S2 R
     
    10291075  tlr_rel … tlr1 tlr2
    10301076\end{verbatim}
     1077\end{comment}
    10311078
    10321079\section{Conclusions and future works}
Note: See TracChangeset for help on using the changeset viewer.