Ignore:
Timestamp:
Nov 30, 2012, 6:31:29 PM (8 years ago)
Author:
campbell
Message:

Conjecture main Cminor/RTLabs simulation results.
Add a few notes about measurable traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableTraces.ma

    r2502 r2511  
    1313(* The start and end states are existentially quantified because the states
    1414   need to be extended with the shadow stack of functions.  (I'm not sure that
    15    was such a great idea now...) *)
     15   was such a great idea now...)  In principle the quantified away part of the
     16   stack would be important for stack-space correctness, except that the
     17   structured trace will never touch it, only the suffix of the trace will.
     18   We could extract the true value from the execution of the prefix anyway. *)
    1619
    1720(* XXX: split of observables seem arbitrary *)
Note: See TracChangeset for help on using the changeset viewer.