Changeset 2511 for src/RTLabs


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

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

Location:
src/RTLabs
Files:
2 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 *)
  • src/RTLabs/abstract.ma

    r2499 r2511  
    44
    55definition RTLabs_state ≝ state.
    6 
     6definition RTLabs_genv ≝ genv.
    77
    88(* Build a full abstract status record that can be used with structured traces. *)
Note: See TracChangeset for help on using the changeset viewer.