Changeset 2206 for src

Timestamp:

Jul 18, 2012, 12:27:02 PM (8 years ago)

Author:

campbell

Message:

Add note about cost maps to simulation definition.

File:

• src/common/Executions.ma (modified) (1 diff)

src/common/Executions.ma

@@ -82 +82 @@
 (* One execution is simulated by another, but possibly using a different number
    of steps.  Note that we have to allow for several steps at the end to make
-   the trace match up. *)
+   the trace match up.
+   
+   This assumes that the overall traces are exactly the same; this may not be
+   the case everywhere and we might have to add a cost label map.  (There is
+   a separate definition for the cost labelling stage, see
+   Clight/labelSpecification.ma.)
+ *)
 
 coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝