Changeset 3387


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

unified notation

Location:
LTS
Files:
2 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:

  • LTS/Traces.ma

    r3380 r3387  
    4545coercion ret_act_label_to_cost_label.
    4646
     47definition call_act_label_to_cost_label :
     48(CallCostLabel + NonFunctionalLabel) → CostLabel ≝
     49λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b].
     50
     51coercion call_act_label_to_cost_label.
     52
    4753inductive ActionLabel : Type[0] ≝
    4854 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
    4955 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
    50  | cost_act : list NonFunctionalLabel → ActionLabel.
     56 | cost_act : option NonFunctionalLabel → ActionLabel
     57 | init_act : ActionLabel.
    5158 
    5259definition is_cost_label : ActionLabel → Prop ≝
    … …  
    6471 ; as_classify : as_status → status_class
    6572 ; is_call_post_label : as_status → bool
     73 ; as_initial : as_status → bool
     74 ; as_final : as_status → bool
     75 ; is_io_entering : NonFunctionalLabel → bool
     76 ; is_io_exiting : NonFunctionalLabel → bool
    6677 }.
    6778 
     79definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
     80λS,l.match l with
     81[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ]
     82| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
     83                                                   | inr c' ⇒ is_io_entering S c']
     84                           | None ⇒ false
     85                           ]
     86| cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ]
     87| init_act ⇒ false
     88].
     89
     90definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝
     91λS,l.match l with
     92[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ]
     93| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
     94                                                   | inr c' ⇒ is_io_exiting S c']
     95                           | None ⇒ false
     96                           ]
     97| cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ]
     98| init_act ⇒ false
     99].
     100
     101
    68102inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
    69103  | t_base : ∀st : S.raw_trace S st st
    … …  
    81115λact.∃l.act = ret_act (Some ? l).
    82116
     117definition is_unlabelled_ret_act : ActionLabel → Prop ≝
     118λact.act = ret_act (None ?).
     119
    83120definition is_non_silent_cost_act : ActionLabel → Prop ≝
    84 λact. ∃hd,tl. act = cost_act (hd::tl).
     121λact. ∃l. act = cost_act (Some ? l).
     122
     123definition is_costlabelled_act : ActionLabel → Prop ≝
     124λact.match act with [ call_act _ _ ⇒ True
     125                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
     126                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
     127                    | init_act ⇒ False
     128                    ].
    85129
    86130inductive well_formed_trace (S : abstract_status) :
    … …  
    113157[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
    114158qed.
    115 (*
    116 inductive balanced_trace (S : abstract_status) :
     159
     160definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
     161raw_trace … st1 st3 → Prop≝
     162λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
     163
     164definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
     165raw_trace … st1 st3 → Prop≝
     166λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
     167
     168inductive silent_trace (S : abstract_status) :
    117169∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    118  | bal_empty : ∀ st : S.balanced_trace … (t_base S st)
    119  | bal_cons_cost : ∀st1,st2,st3 : S.∀l : ActionLabel.
    120                    ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    121                    balanced_trace … tl → is_cost_act l →
    122                    balanced_trace … (t_ind … prf … tl)
    123  | bal_cons_call : ∀s,st1,st2,st3,st4,f,l1,l2.
    124                    ∀prf1 : as_execute S (call_act f l1) s st1.
    125                    ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st3 st4.
    126                    ∀prf2 : as_execute S (ret_act l2) st2 st3.
    127                    (bool_to_Prop (is_call_post_label … s) → l2 ≠ None ?) →
    128                    as_syntactical_succ S s st3 →
    129                    balanced_trace … t1 → balanced_trace … t2 →
    130                    balanced_trace … (t_ind … prf1 … (t1 @ (t_ind … prf2 … t2))).
    131 *)
     170| silent_empty : ∀st : S.silent_trace … (t_base S st)
     171| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
     172                ∀tl : raw_trace S st2 st3. silent_trace … tl →
     173                silent_trace … (t_ind … prf … tl).
     174
    132175inductive pre_measurable_trace (S : abstract_status) :
    133176∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
    134  | pm_empty : ∀st : S. pre_measurable_trace … (t_base ? st)
     177 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
    135178 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
    136179                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    137                       is_cost_act l → pre_measurable_trace … tl →
     180                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
    138181                      pre_measurable_trace … (t_ind … prf … tl)
    139182 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
     183                      as_classify … st1 ≠ cl_io →
    140184                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    141185                      is_labelled_ret_act l → pre_measurable_trace … tl →
    … …  
    143187 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
    144188                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    145                       is_call_act l → is_call_post_label … st1 →
     189                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
    146190                      pre_measurable_trace … tl →
    147191                      pre_measurable_trace … (t_ind … prf … tl)
    … …  
    149193                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
    150194                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
    151                       is_call_act l1 → ¬ is_call_post_label … st1 →
     195                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
     196                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
    152197                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
    153198                      as_syntactical_succ S st1 st4 →
    154                       match l2 with
    155                       [ call_act _ _ ⇒ bool_to_Prop(is_call_post_label ? st3)
    156                       | ret_act _ ⇒ True
    157                       | cost_act x ⇒ match x with [ nil ⇒ False | _ ⇒ True ]
    158                       ]
    159                       → pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
    160 
    161 definition starts_with_label_trace : ∀S : abstract_status.∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    162 λS,st1,st2,t.match t with
    163 [ t_base st ⇒ False
    164 | t_ind st1 st2 st3 l _ _ ⇒ is_call_act l ∨ is_labelled_ret_act l ∨ is_non_silent_cost_act l
    165 ].
    166 
    167 inductive ends_with_label_trace (S : abstract_status) :
    168 ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    169 | call_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
    170                is_call_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
    171 | lab_ret_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
    172                is_labelled_ret_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
    173 | non_silent_cost_act_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
    174                is_non_silent_cost_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
    175 | cons : ∀st1,st2,st3 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
    176                ∀t : raw_trace S st2 st3. ends_with_label_trace … t →
    177                ends_with_label_trace … (t_ind … prf … t).
    178                      
    179 
    180  
    181 
    182 
    183 
     199                      is_unlabelled_ret_act l2 →
     200                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
Note: See TracChangeset for help on using the changeset viewer.