 Timestamp:
 Jul 4, 2013, 5:59:22 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3382 r3383 1 1 include "Common.ma". 2 2 3 replace_last x 4 epsilon ⇒ epsilon, Some x 5  hd::[ 3 record relations: Type[0] ≝ 4 { Srel: status → status → Prop 5 ; Crel: status → status → Prop 6 }. 7 8 definition Rrel ≝ λs,s'. 9 ∀s1,s1'. succ s1 s → Crel s1 s1' → succ s1' s'. 10 11 record 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 66 theorem 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 80 replace_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'' 6 87 7 88 theorem simulates: … … 12 93 ∀s1'. 13 94 S s1 s1' → 95 ∃dead_labels. 14 96 ∃s2'. ∃t2: raw_trace … s1' s2'. 15 97 pre_mesurable_trace … t2 ∧ … … 22 104  Some l2' ⇒ t1 = l2'::t2 ] 23 105  Some l1' ⇒ 24 let 〈t1',x〉 ≝ replace_last l1' t1 in25 match x with26 [ None⇒27 match l2 with28 [ None ⇒ t1' = t229  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.