Changeset 3383


Ignore:
Timestamp:
Jul 4, 2013, 5:59:22 PM (4 years ago)
Author:
sacerdot
Message:

Simple simulation conditions and statements added.

The complex ones would allow the code to tunnel away labels by
returning an initial label that has not been emitted and that must be
emitted by the predecessor code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3382 r3383  
    11include "Common.ma".
    22
    3 replace_last x
    4    epsilon ⇒ epsilon, Some x
    5  | hd::[
     3record relations: Type[0] ≝
     4 { Srel: status → status → Prop
     5 ; Crel: status → status → Prop
     6 }.
     7
     8definition Rrel ≝ λs,s'.
     9 ∀s1,s1'. succ s1 s → Crel s1 s1' → succ s1' s'.
     10
     11record simulation_conditions: Type[0] ≝
     12 { simulate_tau:
     13     ∀s1,s2,s1'.
     14      as_execute s1 s2 (cost_act []) →
     15      Srel s1 s1' →
     16      ∃s2'. ∃t: raw_trace s1' s2'.
     17        Srel s2 s2' ∧ silent t
     18 ; simulate_label:
     19     ∀s1,s2,l,s1'.
     20      as_execute s1 s2 (cost_act [l]) →
     21      Srel s1 s1' →
     22      ∃s2',s2'',s2'''.
     23       ∃t1: raw_trace s1' s2'.
     24       as_execute s2' s2'' (cost_act [l]) ∧
     25       ∃t3: raw_trace s2'' s2'''.
     26        Srel s2 s2''' ∧ silent t1 ∧ silent t3
     27 ; simulate_call_pl:
     28     ∀s1,s2,l,s1'.
     29      post_labelled s1 →
     30      as_execute s1 s2 (call_act l) →
     31      Srel s1 s1' →
     32      ∃s2',s2'',s2'''.
     33       ∃t1: raw_trace s1' s2'.
     34       as_execute s2' s2'' (call_act l) ∧
     35       ∃t3: raw_trace s2'' s2'''.
     36        Srel s2 s2''' ∧ silent t1 ∧ silent t3
     37 ; simulate_ret_l:
     38     ∀s1,s2,l,s1'.
     39      as_execute s1 s2 (ret_act (Some l)) →
     40      Srel s1 s1' →
     41      ∃s2',s2'',s2'''.
     42       ∃t1: raw_trace s1' s2'.
     43       as_execute s2' s2'' (ret_act (Some l)) ∧
     44       ∃t3: raw_trace s2'' s2'''.
     45        Srel s2 s2''' ∧ silent t1 ∧ silent t3
     46 ; simulate_call_n:
     47     ∀s1,s2,l,s1'.
     48      as_execute s1 s2 (call_act l) →
     49      Srel s1 s1' →
     50      ∃s2',s2'',s2'''.
     51       ∃t1: raw_trace s1' s2'.
     52       as_execute s2' s2'' (ret_act None) ∧
     53       ∃t3: raw_trace s2'' s2'''.
     54        Srel s2 s2''' ∧ silent t1 ∧ silent t3 ∧ Rrel s2 s2'' ∧ Crel s1 s2'
     55 ; simulate_ret_n:
     56     ∀s1,s2,l,s1'.
     57      as_execute s1 s2 (ret_act None) →
     58      Srel s1 s1' →
     59      ∃s2',s2'',s2'''.
     60       ∃t1: raw_trace s1' s2'.
     61       as_execute s2' s2'' (ret_act None) ∧
     62       ∃t3: raw_trace s2'' s2'''.
     63        Srel s2 s2''' ∧ silent t1 ∧ silent t3 ∧ Rrel s2 s2''
     64 }.
     65
     66theorem simulates:
     67 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
     68  pre_measurable_trace … t1 →
     69  well_formed_trace … t1.
     70 ∀s1'.
     71   S s1 s1' →
     72   ∃s2'. ∃t2: raw_trace … s1' s2'.
     73    pre_mesurable_trace … t2 ∧
     74    well_formed_trace … t2 ∧
     75    |t1| = |t2| ∧
     76    S s2 s2.
     77
     78(*********************************************************************)
     79
     80replace_last x : weak_trace → weak_trace
     81   [] ⇒ [], Some x
     82 | l::t ⇒
     83     let 〈t',x'〉 ≝ replace_last x t in
     84     match x' with
     85     [ None ⇒ l::t', None
     86     | Some x'' ⇒ [], Some x''
    687
    788theorem simulates:
     
    1293 ∀s1'.
    1394   S s1 s1' →
     95   ∃dead_labels.
    1496   ∃s2'. ∃t2: raw_trace … s1' s2'.
    1597    pre_mesurable_trace … t2 ∧
     
    22104       | Some l2' ⇒ |t1| = l2'::|t2| ]
    23105    | Some l1' ⇒
    24        let 〈t1',x〉 ≝ replace_last l1' t1 in
    25        match x with
    26        [ None
    27           match l2 with
    28           [ None ⇒ |t1'| = |t2|
    29           | Some l2' ⇒ |t1'| = l2'::|t2| ]
    30        | Some x ⇒ l2 = x ]
     106       match l2 with
     107       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
     108       | Some l2'
     109          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
     110          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
     111       ]
     112    ]
Note: See TracChangeset for help on using the changeset viewer.