# Changeset 2613

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

...

File:
1 edited

### Legend:

Unmodified
 r2612 % a built-in definition. %\newtheorem{theorem}{Theorem} \newtheorem{condition}{Condition} \lstdefinelanguage{coq} 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 $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 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 to avoid collapsing two consecutive states that emit the same label to just one state, missing one of the two emissions. \begin{verbatim} definition status_simulation ≝ as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ ∃st2_after_call,st2'. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. as_execute … st2_pre_call st2_after_call ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2_after_call | cl_tailcall ⇒ ∀prf. (* st1' ------------S----------\ ↑ \                         \ st1 \--L--\                   \ |         \                   \ S         st2_after_call →taa→ st2' |             ↑ st2 →taa→ st2_pre_call *) ∃st2_pre_call. as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧ ∃st2_after_call,st2'. ∃taa2 : trace_any_any … st2 st2_pre_call. ]. \end{verbatim} \begin{comment} \begin{verbatim} definition status_simulation ≝ λS1 : abstract_status. λS2 : abstract_status. λsim_status_rel : status_rel S1 S2. ∀st1,st1',st2.as_execute S1 st1 st1' → sim_status_rel st1 st2 → match as_classify … st1 with [ None ⇒ True | Some cl ⇒ match cl with [ cl_call ⇒ ∀prf. (* st1' ------------S----------\ ↑ \                         \ st1 \--L--\                   \ | \       \                   \ S  \-C-\  st2_after_call →taa→ st2' |       \     ↑ st2 →taa→ st2_pre_call *) ∃st2_pre_call. as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ ∃st2_after_call,st2'. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. as_execute … st2_pre_call st2_after_call ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2_after_call | cl_return ⇒ (* st1 / ↓ | st1'----------S,L------------\ S   \                           \ \   \-----R-------\            | \                 |           | st2 →taa→ st2_ret |           | ↓   /            | st2_after_ret →taaf→ st2' we also ask that st2_after_ret be not labelled if the taaf tail is not empty *) ∃st2_ret,st2_after_ret,st2'. ∃taa2 : trace_any_any … st2 st2_ret. ∃taa2' : trace_any_any_free … st2_after_ret st2'. (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ as_classifier … st2_ret cl_return ∧ 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' ] ]. \end{verbatim} \end{comment} \begin{verbatim}