Changeset 1559 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Nov 24, 2011, 6:49:51 PM (8 years ago)
Author:
campbell
Message:

Add a notion of flat traces with evidence for RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1552 r1559  
    4242inversion H try #a try #b try #c try #d try #e try #f destruct
    4343qed.
     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
     51coinductive 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? *)
     57coinductive 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
     62let 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 ≝
     65let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
     66match 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
     130let 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 ≝
     134let ge ≝ make_global … p in
     135let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
     136match 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
Note: See TracChangeset for help on using the changeset viewer.