source: src/common/Executions.ma @ 2202

Last change on this file since 2202 was 2202, checked in by campbell, 8 years ago

Start defining equivalent executions.

File size: 1.5 KB
RevLine 
[2202]1include "common/SmallstepExec.ma".
2include "common/IO.ma".
3
4(* Equivalences of execution traces. *)
5
6(* A finite trace is produced by some prefix of an execution. *)
7
8inductive steps (state:Type[0]) : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
9| steps_stop : ∀tr,s,r. steps state tr (e_stop … tr s r) (e_stop … tr s r)
10| steps_step : ∀tr,s,e. steps state tr (e_step … tr s e) e
11| steps_steps : ∀tr,s,e,tr',e'. steps state tr e e' → steps state (tr'⧺tr) (e_step … tr' s e) e'.
12
13(* In some places we do not consider wrong executions. *)
14
15coinductive not_wrong (state:Type[0]) : execution state io_out io_in → Prop ≝
16| nw_stop : ∀tr,i,s. not_wrong state (e_stop … tr i s)
17| nw_step : ∀tr,s,e. not_wrong state e → not_wrong state (e_step … tr s e)
18| nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k).
19
20(* One execution is simulated by another, but possibly using a different number
21   of steps. *)
22
23coinductive simulates (state:Type[0]) : execution state io_out io_in → execution state io_out io_in → Prop ≝
24| sim_stop : ∀tr,tr',r,s1,s2,e1,e2.
25    steps state tr e1 (e_stop … tr' r s1) →
26    steps state tr e2 (e_stop … tr' r s2) →
27    simulates state e1 e2
28| sim_steps : ∀tr,e1,e1',e2,e2'.
29    steps state tr e1 e1' →
30    steps state tr e2 e2' →
31    simulates state e1' e2' →
32    simulates state e1 e2
33| sim_interact : ∀o,k1,k2.
34    (∀i. simulates state (k1 i) (k2 i)) →
35    simulates state (e_interact … o k1) (e_interact … o k2).
36
Note: See TracBrowser for help on using the repository browser.