Ignore:
Timestamp:
Jul 2, 2012, 4:12:12 PM (8 years ago)
Author:
campbell
Message:

Cost labelling doesn't affect interaction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSpecification.ma

    r2134 r2145  
    2828    trace_with_extra_labels tr1 tr2 →
    2929    sim_with_labels e1 e2' →
    30     sim_with_labels (e_step … tr1 s1 e1) e2.
     30    sim_with_labels (e_step … tr1 s1 e1) e2
     31| swl_interact : ∀o,k1,k2.
     32    (∀i. sim_with_labels (k1 i) (k2 i)) →
     33    sim_with_labels (e_interact … o k1) (e_interact … o k2).
    3134
    3235(* We do not consider wrong executions or I/O. *)
    3336
    34 coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝
    35 | nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s)
    36 | nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e).
     37coinductive not_wrong : execution state io_out io_in → Prop ≝
     38| nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)
     39| nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)
     40| nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).
    3741
    3842(* Desired result *)
     
    4246  let e1 ≝ exec_inf … clight_fullexec p in
    4347  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
    44   not_wrong_no_io e1 →
     48  not_wrong e1 →
    4549  sim_with_labels e1 e2.
Note: See TracChangeset for help on using the changeset viewer.