Changeset 2511 for src/common


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2502 r2511  
    7373}.
    7474
     75(* FIXME: this definition is unreasonable because it presumes we can easily
     76   identify the change in stack usage from return states, but that information
     77   is rather implicit (we only really record the function called in the
     78   extended RTLabs states when building the structured traces). *)
     79
    7580definition measurable : ∀C:preclassified_system.
    7681  ∀p:program ?? C. nat → nat →
Note: See TracChangeset for help on using the changeset viewer.