Changeset 1559 for src/RTLabs

Timestamp:

Nov 24, 2011, 6:49:51 PM (9 years ago)

Author:

campbell

Message:

Add a notion of flat traces with evidence for RTLabs.

Location:

src/RTLabs

Files:

• Traces.ma (modified) (1 diff)
• semantics.ma (modified) (2 diffs)

src/RTLabs/Traces.ma

@@ -42 +42 @@
 inversion H try #a try #b try #c try #d try #e try #f destruct
 qed.
+
+(* Before attempting to construct a structured trace, let's show that we can
+   form flat traces with evidence that they were constructed from an execution.
+   
+   For now we don't consider I/O. *)
+
+
+coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
+| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
+| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
+| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
+
+(* add I/O? *)
+coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
+| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
+| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
+| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
+
+let corec make_flat_trace ge s
+  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
+  flat_trace io_out io_in ge s ≝
+let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
+match e return λx. e = x → ? with
+[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
+| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
+| e_wrong m ⇒ λE. ft_wrong … s m ?
+| e_interact o f ⇒ λE. ⊥
+] (refl ? e).
+[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
+  cases (eval_statement ge s)
+  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
+  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
+    >(?:is_final ????? = RTLabs_is_final s1) //
+    lapply (refl ? (RTLabs_is_final s1))
+    cases (RTLabs_is_final s1) in ⊢ (???% → %);
+    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
+    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
+    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
+    ]
+  | *: #m whd in ⊢ (??%? → ?); #E destruct
+  ]
+| whd in E:(??%?); >exec_inf_aux_unfold in E;
+  cases (eval_statement ge s)
+  [ #O #K whd in ⊢ (??%? → ?); #E destruct
+  | * #tr #s1 whd in ⊢ (??%? → ?);
+    cases (is_final ?????)
+    [ whd in ⊢ (??%? → ?); #E destruct @refl
+    | #i whd in ⊢ (??%? → ?); #E destruct
+    ]
+  | #m whd in ⊢ (??%? → ?); #E destruct
+  ]
+| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
+  cases (eval_statement ge s)
+  [ #O #K whd in ⊢ (??%? → ?); #E destruct
+  | * #tr #s1 whd in ⊢ (??%? → ?);
+    cases (is_final ?????)
+    [ whd in ⊢ (??%? → ?); #E
+      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
+      destruct
+      inversion H
+      [ #a #b #c #E1 destruct
+      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
+      | #m #E1 destruct
+      ]
+    | #i whd in ⊢ (??%? → ?); #E destruct
+    ]
+  | #m whd in ⊢ (??%? → ?); #E destruct
+  ]
+| whd in E:(??%?); >exec_inf_aux_unfold in E;
+  cases (eval_statement ge s)
+  [ #O #K whd in ⊢ (??%? → ?); #E destruct
+  | * #tr1 #s1 whd in ⊢ (??%? → ?);
+    cases (is_final ?????)
+    [ whd in ⊢ (??%? → ?); #E destruct
+    | #i whd in ⊢ (??%? → ?); #E destruct
+    ]
+  | #m whd in ⊢ (??%? → ?); #E destruct @refl
+  ]
+| whd in E:(??%?); >E in H; #H
+  inversion H
+  [ #a #b #c #E destruct
+  | #a #b #c #d #E1 destruct
+  | #m #E1 destruct
+  ]
+] qed.
+
+let corec make_whole_flat_trace p s
+  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
+  (I:make_initial_state ??? p = OK ? s) :
+  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
+let ge ≝ make_global … p in
+let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
+match e return λx. e = x → ? with
+[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
+| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
+| e_wrong m ⇒ λE. ⊥
+| e_interact o f ⇒ λE. ⊥
+] (refl ? e).
+[ whd in E:(??%?); >exec_inf_aux_unfold in E; 
+  whd in ⊢ (??%? → ?);
+  >(?:is_final ????? = RTLabs_is_final s) //
+  lapply (refl ? (RTLabs_is_final s))
+  cases (RTLabs_is_final s) in ⊢ (???% → %);
+  [ #_ whd in ⊢ (??%? → ?); #E destruct
+  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
+  ]
+| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
+  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
+  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
+    [ #a #b #c #E1 destruct
+    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
+      @H1
+    | #m #E1 destruct
+    ]
+  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
+  ]
+| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
+  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
+| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
+  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
+] qed.
+

src/RTLabs/semantics.ma

@@ -197 +197 @@
 ] qed.
 
-definition is_final : state → option int ≝
+definition RTLabs_is_final : state → option int ≝
 λs. match s with
 [ State _ _ _ ⇒ None ?
@@ -212 +212 @@
 
 definition RTLabs_exec : trans_system io_out io_in ≝
-  mk_trans_system … ? (λ_.is_final) eval_statement.
+  mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement.
 
 definition make_global : RTLabs_program → genv ≝