Ignore:
Timestamp:
Mar 11, 2013, 12:18:05 PM (7 years ago)
Author:
campbell
Message:

Basic structure of RTLabs measurable to structured traces results.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_traces.ma

    r2760 r2839  
     1
     2(* This file shows that structured traces can be generated for entire executions
     3   of RTLabs programs (given no failure or I/O).  It stands alone; the file
     4   RTLabs/RTLabs_partial_traces.ma contains a finite variant that is used for
     5   the compiler proofs. *)
    16
    27include "RTLabs/RTLabs_abstract.ma".
Note: See TracChangeset for help on using the changeset viewer.