Changeset 3465 for LTS

Timestamp:

Feb 21, 2014, 8:49:01 PM (7 years ago)

Author:

piccolo

Message:

 

File:

• LTS/Vm.ma (modified) (1 diff)

LTS/Vm.ma

@@ -902 +902 @@
 qed.
 
-
-
-
+(*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
+theorem static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
+∀abs_t : abstract_transition_sys (m … p').∀instr_m.
+∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
+∀EQmap : static_analisys p ? instr_m mT prog = return map1.
+∀t : measurable_trace (asm_operational_semantics p p' prog).
+∀a1.rel_galois … good st1 (L_s1 … t) → 
+let stop_state ≝ match R_post_state … t with [None ⇒ R_s2 … t | Some x ⇒ x ] in
+∀costs.
+costs = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
+rel_galois … good stop_state (act_abs … abs_t (big_op … costs) a1).
+
+
+