Changeset 3387 for LTS/Simulation.ma


Ignore:
Timestamp:
Jul 23, 2013, 4:33:51 PM (6 years ago)
Author:
piccolo
Message:

unified notation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3386 r3387  
    11include "Common.ma".
    2 
    3 record relations: Type[0] ≝
    4  { Srel: status → status → Prop
    5  ; Crel: status → status → Prop
     2include "Traces.ma".
     3
     4record relations (S : abstract_status) : Type[0] ≝
     5 { Srel: S → S → Prop
     6 ; Crel: S → S → Prop
    67 }.
    78
    8 definition Rrel ≝ λs,s'.
    9  ∀s1,s1'. succ s1 s → Crel s1 s1' → succ s1' s'.
    10 
    11 record simulation_conditions: Type[0] ≝
     9definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S.
     10 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'.
     11
     12record simulation_conditions (S : abstract_status) (rel : relations S) : Type[0] ≝
    1213 { 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
     14     ∀s1,s2,s1' : S.
     15      as_execute … (cost_act (None ?))  s1 s1'
     16      Srel … rel s1 s2
     17      ∃s2'. ∃t: raw_trace S s2 s2'.
     18        Srel … rel s2 s2' ∧ silent_trace … t
    1819 ; simulate_label:
    1920     ∀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
     21      as_execute S (cost_act (Some ? l)) s1 s1'
     22      Srel … rel s1 s2
     23      ∃s2',s2'',s2'''.
     24       ∃t1: raw_trace S s2 s2'.
     25       as_execute … (cost_act (Some ? l)) s2' s2''
     26       ∃t3: raw_trace S s2'' s2'''.
     27        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    2728 ; 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
     29     ∀s1,s2,s1' : S.∀f,l.
     30      is_call_post_label … s1 →
     31      as_execute … (call_act f l) s1 s1'
     32      Srel … rel s1 s2
     33      ∃s2',s2'',s2'''.
     34       ∃t1: raw_trace S s2 s2'.
     35       as_execute … (call_act f l) s2' s2''
     36       ∃t3: raw_trace S s2'' s2'''.
     37        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    3738 ; 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
     39     ∀s1,s2,s1' : S.∀l.
     40      as_execute S (ret_act (Some ? l)) s1 s1'
     41      Srel  … rel s1 s2
     42      ∃s2',s2'',s2'''.
     43       ∃t1: raw_trace S s2 s2'.
     44       as_execute … (ret_act (Some ? l)) s2' s2''
     45       ∃t3: raw_trace S s2'' s2'''.
     46        Srel … rel s2 s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    4647 ; simulate_call_n:
    47      ∀s1,s2,l,s1'.
    48       as_execute s1 s2 (call_act l) →
    49       ¬ post_labelled … →
    50       Srel s1 s1' →
    51       ∃s2',s2'',s2'''.
    52        ∃t1: raw_trace s1' s2'.
    53        as_execute s2' s2'' (ret_act None) ∧
    54        ∃t3: raw_trace s2'' s2'''.
    55         Srel s2 s2''' ∧ silent t1 ∧ silent t3 (*???? BUG? ∧ Rrel s2 s2''*) ∧ Crel s1 s2'
     48     ∀s1,s2,s1' : S.∀f,l.
     49      as_execute … (call_act f l) s1 s1' →
     50      ¬ is_call_post_label … s1 →
     51      Srel … rel s1 s2 →
     52      ∃s2',s2'',s2'''.
     53       ∃t1: raw_trace S s2 s2'.
     54       as_execute … (call_act f l) s2' s2'' ∧
     55       ∃t3: raw_trace S s2'' s2'''.
     56        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     57        ∧ Crel … rel s1 s2'
    5658 ; simulate_ret_n:
    57      ∀s1,s2,l,s1'.
    58       as_execute s1 s2 (ret_act None) →
    59       Srel s1 s1' →
    60       ∃s2',s2'',s2'''.
    61        ∃t1: raw_trace s1' s2'.
    62        as_execute s2' s2'' (ret_act None) ∧
    63        ∃t3: raw_trace s2'' s2'''.
    64         Srel s2 s2''' ∧ silent t1 ∧ silent t3 ∧ Rrel s2 s2''
     59     ∀s1,s2,s1' : S.
     60      as_execute … (ret_act (None ?)) s1 s1' →
     61      Srel … rel s1 s2 →
     62      ∃s2',s2'',s2'''.
     63       ∃t1: raw_trace S s2 s2'.
     64       as_execute … (ret_act (None ?)) s2' s2''  ∧
     65       ∃t3: raw_trace S s2'' s2'''.
     66        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     67        ∧ Rrel … rel s2 s2''
    6568 }.
    6669
     70let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
     71(t : raw_trace S st1 st2) on t : list CostLabel ≝
     72match t with
     73[ t_base st ⇒ [ ]
     74| t_ind st1' st2' st3' l prf t' ⇒
     75    let tl ≝ get_costlabels_of_trace … t' in
     76    match l with
     77    [ call_act f c ⇒ c :: tl
     78    | ret_act x ⇒ match x with
     79                  [ Some c ⇒ ret_act_label_to_cost_label c :: tl
     80                  | None ⇒ tl
     81                  ]
     82    | cost_act x ⇒ match x with
     83                  [ Some c ⇒ a_non_functional_label c :: tl
     84                  | None ⇒ tl
     85                  ]
     86    | init_act ⇒ tl
     87    ]
     88].
     89
     90
    6791theorem simulates_pre_mesurable:
    68  ∀s1,s2. ∀τ1: raw_trace … s1 s2.
     92 ∀S : abstract_status.∀rel : relations S.
     93 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
    6994  pre_measurable_trace … t1 →
    70   well_formed_trace … t1 →
    71  ∀s1'.
    72    S s1 s1' →
    73    ∃s2'. ∃t2: raw_trace … s1' s2'.
    74     pre_mesurable_trace … t2 ∧
     95  well_formed_trace … t1 → ∀s2.Srel … rel s1 s2 →
     96  ∃s2'. ∃t2: raw_trace … s1' s2'.
     97    pre_measurable_trace … t2 ∧
    7598    well_formed_trace … t2 ∧
    76     |t1| = |t2| ∧
    77     S s2 s2'.
     99    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
     100    Srel … rel s2 s2'.
     101cases daemon (*TODO*)
     102qed.
    78103
    79104(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
     
    89114  as_execute … s2 so L'. *)
    90115
    91 (*CSC: definire usando un record?*)
    92 record L_raw_trace ≝
    93  { L_label: label
    94  ; L_s1: status
    95  ; L_s2: status
    96  ; L_t: raw_trace … s1 s2
    97  ; L_ok: ∃s0. as_execute … s0 L_s1 L_label.
    98  (* o, nel caso in cui s1 sia lo stato iniziale, non serve nessun s0
    99     e L e' la label init *)
     116record LR_raw_trace (S : abstract_status) : Type[0] ≝
     117 { L_label: ActionLabel
     118 ; R_label : ActionLabel
     119 ; LR_s1: S
     120 ; LR_s2: S
     121 ; LR_t : raw_trace S LR_s1 LR_s2
     122 ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act
     123 ; L_noinit_ok :
     124      bool_to_Prop (¬ as_initial … LR_s1) →
     125        ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label
     126        ∧ ¬ bool_to_Prop (is_act_io_entering S L_label)
     127 ; R_nonfin_ok :
     128    bool_to_Prop (¬ as_final … (LR_s2)) →
     129      ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label
     130          ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label)
    100131 }.
    101 
    102 definition measurable' ≝
    103  λt: L_raw_trace.
    104   ∃L',so.
    105    pre_measurable_trace … (L_t t) ∧
    106    well_formed_trace … (L_t t) ∧
    107    as_execute … (L_s2 t) so L'.
    108  (* o, nel caso in cui s2 sia uno stato finale, non serve nessun so e nessuna L' *)
     132 
     133definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S.
     134pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t).
     135
    109136
    110137(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
     
    113140
    114141definition unmovable_entry_label ≝
    115   call, return post-labelled, init, I/O-uscente.
     142λS : abstract_status.λl.
     143match l with
     144[ call_act _ _ ⇒ false
     145| ret_act _ ⇒ false
     146| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
     147                            | None ⇒ false
     148                            ]
     149| init_act ⇒ true
     150].
    116151 
    117 definition unmovable_exit_lable ≝
    118   I/O-entrante, stato finale (???).
     152definition unmovable_exit_label ≝
     153λS : abstract_status.λl.
     154match l with
     155[ call_act _ _ ⇒ false
     156| ret_act _ ⇒ false
     157| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
     158                            | None ⇒ false
     159                            ]
     160| init_act ⇒ false
     161].
     162
     163theorem simulates_LR_raw_trace :
     164∀S : abstract_status.
     165∀t : LR_raw_trace S.
     166∀rel : relations S.
     167measurable S t →
     168∀s1'.Srel … rel (LR_s1 … t) s1' →
     169∃ t' : LR_raw_trace S.
     170measurable S t' ∧
     171if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
     172   LR_s1 … t' = s1'
     173else
     174   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
     175∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
     176if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
     177   LR_s2 … t' = s1''
     178else
     179  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
     180
     181get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
     182cases daemon (*TODO*)
     183qed.
     184
     185xxxx
    119186
    120187theorem simulates_L_raw_trace:
Note: See TracChangeset for help on using the changeset viewer.