- Timestamp:
- Jul 18, 2012, 12:27:02 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Executions.ma
r2203 r2206 82 82 (* One execution is simulated by another, but possibly using a different number 83 83 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 *) 85 91 86 92 coinductive 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.