Changeset 3465 for LTS/Vm.ma


Ignore:
Timestamp:
Feb 21, 2014, 8:49:01 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3464 r3465  
    902902qed.
    903903
    904 
    905 
    906 
     904(*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
     905theorem static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
     906∀abs_t : abstract_transition_sys (m … p').∀instr_m.
     907∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
     908∀EQmap : static_analisys p ? instr_m mT prog = return map1.
     909∀t : measurable_trace (asm_operational_semantics p p' prog).
     910∀a1.rel_galois … good st1 (L_s1 … t) →
     911let stop_state ≝ match R_post_state … t with [None ⇒ R_s2 … t | Some x ⇒ x ] in
     912∀costs.
     913costs = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
     914rel_galois … good stop_state (act_abs … abs_t (big_op … costs) a1).
     915
     916
     917
Note: See TracChangeset for help on using the changeset viewer.