Changeset 1559
 Timestamp:
 Nov 24, 2011, 6:49:51 PM (9 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1552 r1559 42 42 inversion H try #a try #b try #c try #d try #e try #f destruct 43 43 qed. 44 45 (* Before attempting to construct a structured trace, let's show that we can 46 form flat traces with evidence that they were constructed from an execution. 47 48 For now we don't consider I/O. *) 49 50 51 coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ 52  noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) 53  noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) 54  noio_wrong : ∀m. exec_no_io o i (e_wrong … m). 55 56 (* add I/O? *) 57 coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ 58  ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s 59  ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s 60  ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. 61 62 let corec make_flat_trace ge s 63 (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : 64 flat_trace io_out io_in ge s ≝ 65 let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in 66 match e return λx. e = x → ? with 67 [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) 68  e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?) 69  e_wrong m ⇒ λE. ft_wrong … s m ? 70  e_interact o f ⇒ λE. ⊥ 71 ] (refl ? e). 72 [ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E; 73 cases (eval_statement ge s) 74 [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct 75  2,5: * #tr #s1 whd in ⊢ (??%? → ?); 76 >(?:is_final ????? = RTLabs_is_final s1) // 77 lapply (refl ? (RTLabs_is_final s1)) 78 cases (RTLabs_is_final s1) in ⊢ (???% → %); 79 [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct 80  #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl 81  #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct 82 ] 83  *: #m whd in ⊢ (??%? → ?); #E destruct 84 ] 85  whd in E:(??%?); >exec_inf_aux_unfold in E; 86 cases (eval_statement ge s) 87 [ #O #K whd in ⊢ (??%? → ?); #E destruct 88  * #tr #s1 whd in ⊢ (??%? → ?); 89 cases (is_final ?????) 90 [ whd in ⊢ (??%? → ?); #E destruct @refl 91  #i whd in ⊢ (??%? → ?); #E destruct 92 ] 93  #m whd in ⊢ (??%? → ?); #E destruct 94 ] 95  whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; 96 cases (eval_statement ge s) 97 [ #O #K whd in ⊢ (??%? → ?); #E destruct 98  * #tr #s1 whd in ⊢ (??%? → ?); 99 cases (is_final ?????) 100 [ whd in ⊢ (??%? → ?); #E 101 change with (eval_statement ge s1) in E:(??(??????(?????%))?); 102 destruct 103 inversion H 104 [ #a #b #c #E1 destruct 105  #trx #sx #ex #H1 #E2 #E3 destruct @H1 106  #m #E1 destruct 107 ] 108  #i whd in ⊢ (??%? → ?); #E destruct 109 ] 110  #m whd in ⊢ (??%? → ?); #E destruct 111 ] 112  whd in E:(??%?); >exec_inf_aux_unfold in E; 113 cases (eval_statement ge s) 114 [ #O #K whd in ⊢ (??%? → ?); #E destruct 115  * #tr1 #s1 whd in ⊢ (??%? → ?); 116 cases (is_final ?????) 117 [ whd in ⊢ (??%? → ?); #E destruct 118  #i whd in ⊢ (??%? → ?); #E destruct 119 ] 120  #m whd in ⊢ (??%? → ?); #E destruct @refl 121 ] 122  whd in E:(??%?); >E in H; #H 123 inversion H 124 [ #a #b #c #E destruct 125  #a #b #c #d #E1 destruct 126  #m #E1 destruct 127 ] 128 ] qed. 129 130 let corec make_whole_flat_trace p s 131 (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) 132 (I:make_initial_state ??? p = OK ? s) : 133 flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ 134 let ge ≝ make_global … p in 135 let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in 136 match e return λx. e = x → ? with 137 [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? 138  e_step _ _ e' ⇒ λE. make_flat_trace ge s ? 139  e_wrong m ⇒ λE. ⊥ 140  e_interact o f ⇒ λE. ⊥ 141 ] (refl ? e). 142 [ whd in E:(??%?); >exec_inf_aux_unfold in E; 143 whd in ⊢ (??%? → ?); 144 >(?:is_final ????? = RTLabs_is_final s) // 145 lapply (refl ? (RTLabs_is_final s)) 146 cases (RTLabs_is_final s) in ⊢ (???% → %); 147 [ #_ whd in ⊢ (??%? → ?); #E destruct 148  #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct 149 ] 150  whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); 151 >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) 152 [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H 153 [ #a #b #c #E1 destruct 154  #tr1 #s1 #e1 #H1 #E1 #E2 E2 I destruct (E1) 155 @H1 156  #m #E1 destruct 157 ] 158  #i whd in ⊢ (??%? → ???% → ?); #E destruct 159 ] 160  whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); 161 cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct 162  whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); 163 cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct 164 ] qed. 165 
src/RTLabs/semantics.ma
r1535 r1559 197 197 ] qed. 198 198 199 definition is_final : state → option int ≝199 definition RTLabs_is_final : state → option int ≝ 200 200 λs. match s with 201 201 [ State _ _ _ ⇒ None ? … … 212 212 213 213 definition RTLabs_exec : trans_system io_out io_in ≝ 214 mk_trans_system … ? (λ_. is_final) eval_statement.214 mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement. 215 215 216 216 definition make_global : RTLabs_program → genv ≝
Note: See TracChangeset
for help on using the changeset viewer.