Changeset 2206


Ignore:
Timestamp:
Jul 18, 2012, 12:27:02 PM (5 years ago)
Author:
campbell
Message:

Add note about cost maps to simulation definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Executions.ma

    r2203 r2206  
    8282(* One execution is simulated by another, but possibly using a different number
    8383   of steps.  Note that we have to allow for several steps at the end to make
    84    the trace match up. *)
     84   the trace match up.
     85   
     86   This assumes that the overall traces are exactly the same; this may not be
     87   the case everywhere and we might have to add a cost label map.  (There is
     88   a separate definition for the cost labelling stage, see
     89   Clight/labelSpecification.ma.)
     90 *)
    8591
    8692coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.