Changeset 1880 for src/common


Ignore:
Timestamp:
Apr 6, 2012, 4:57:22 PM (8 years ago)
Author:
campbell
Message:

Show that RTLabs flat traces are determined by their starting state, and
that structured traces can be flattened, so must describe the same
execution as a flat trace from the same starting point.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1812 r1880  
    167167            trace_label_diverges_exists S status_initial.
    168168
    169 
    170 inductive trace_whole_program (S:abstract_status) : S → Type[0] ≝
     169record final_abstract_status : Type[1] ≝ {
     170  as_as :> abstract_status;
     171  as_final:as_status as_as → Prop
     172}.
     173
     174
     175inductive trace_whole_program (S:final_abstract_status) : S → Type[0] ≝
    171176  | twp_terminating:
    172177      ∀status_initial: S.
     
    176181        as_execute S status_initial status_start_fun →
    177182        trace_label_return S status_start_fun status_final →
     183        as_final S status_final →
    178184        trace_whole_program S status_initial
    179185  | twp_diverges:
     
    186192
    187193(* Again, an identical version in Prop for existence proofs. *)
    188 inductive trace_whole_program_exists (S:abstract_status) : S → Prop ≝
     194inductive trace_whole_program_exists (S:final_abstract_status) : S → Prop ≝
    189195  | twp_terminating:
    190196      ∀status_initial: S.
     
    194200        as_execute S status_initial status_start_fun →
    195201        trace_label_return S status_start_fun status_final →
     202        as_final S status_final →
    196203        trace_whole_program_exists S status_initial
    197204  | twp_diverges:
Note: See TracChangeset for help on using the changeset viewer.