Changeset 3374


Ignore:
Timestamp:
Jul 1, 2013, 5:08:00 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3372 r3374  
    1616include "basics/types.ma".
    1717include "basics/deqsets.ma".
     18include "../src/ASM/Util.ma".
    1819
    1920inductive FunctionName : Type[0] ≝
     
    4950 | cost_act : NonFunctionalLabel → ActionLabel
    5051 | tau_act : ActionLabel.
     52 
     53definition is_cost_label : ActionLabel → Prop ≝
     54λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
    5155
    5256record program_counter_type : Type[1] ≝
     
    6367 }.
    6468 
    65 inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
    66   | t_base : ∀st : S.raw_trace S st st
    67   | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
    68              as_execute S l st1 st2 → raw_trace S st2 st3 → raw_trace S st1 st3.
     69inductive raw_trace (S : abstract_status) : option(ActionLabel) → S → S → Type[0] ≝
     70  | t_base : ∀st : S.raw_trace S (None ?) st st
     71  | t_ind : ∀st1,st2,st3 : S.∀m.∀l : ActionLabel.
     72             as_execute S l st1 st2 → raw_trace S m st2 st3 →
     73             raw_trace S (Some ? l) st1 st3.
     74             
     75inductive well_formed_trace (S : abstract_status) :
     76   ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
     77  | t_empty : ∀st: S.well_formed_trace … (t_base S st)
     78  | t_cons_uncosted :  ∀st1,st2 : .
     79 
    6980
    7081
Note: See TracChangeset for help on using the changeset viewer.