# Changeset 2614

Ignore:
Timestamp:
Feb 6, 2013, 3:39:17 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2613 put the labelling approach in motion. \begin{condition}[Case \texttt{cl\_other}] 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\_other}$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either \begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}] 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\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and $(\texttt{as\_costed}~s_1')$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}. \end{condition} The intuition is that one step can be replaced with zero or more steps if it In the above condition, a $(\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an inductive type of structured traces that do not contain function calls or cost emission statements. Differently from a \texttt{trace\_any\_any}, the instruction to be executed in the lookahead state $s_2$ may be a cost emission statement. The intuition of the condition is that one step can be replaced with zero or more steps if it preserves the relation between the data and if the two final statuses are labelled in the same way. Moreover, we must take special care of the empty case 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' | cl_other ⇒ (* st1 → st1' |      \ S      S,L |        \ st2 →taaf→ st2' the taaf can be empty (e.g. tunneling) but we ask it must not be the case when both st1 and st1' are labelled (we would be able to collapse labels otherwise) *) ∃st2'. ∃taa2 : trace_any_any_free … st2 st2'. (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2' | cl_jump ⇒ (* just like cl_other, but with a hypothesis more *) as_costed … st1' → ∃st2'. ∃taa2 : trace_any_any_free … st2 st2'. (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2' ]