Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTLAxiom.ma

    r3096 r3145  
    2020include "RTLabs/MeasurableToStructured.ma". (* for make_ext_initial_state *)
    2121
    22 definition RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop ≝
    23 λstack_sizes,p.
    24 All …
    25   (λi_f.let 〈i, f〉 ≝ i_f in
    26     match f with
    27     [ External _ ⇒ True
    28     | Internal def ⇒
    29       ∃sz.stack_sizes i = Some ? sz ∧ f_stacksize … def ≤ sz
    30     ]) (prog_funct … p).
     22definition RTLabsToRTLstacksizes_ok : RTLabs_program → stack_cost_model → Prop ≝
     23λp.stack_cost_model_le (rtlabs_stack_cost p).
    3124
    3225axiom RTLabsToRTL_ok :
    33 ∀stacksizes : ident → option ℕ.
     26∀stack_model : stack_cost_model.
    3427∀cost.
    3528∀p_in : RTLabs_program.
    36 RTLabsToRTLstacksizes_ok stacksizes p_in
     29RTLabsToRTLstacksizes_ok p_in stack_model
    3730let p_out ≝ rtlabs_to_rtl cost p_in in
     31let stacksizes ≝ stack_sizes stack_model in
    3832∀init_in.make_ext_initial_state p_in = OK … init_in →
    3933∃init_out : state_pc RTL_semantics_separate.
Note: See TracChangeset for help on using the changeset viewer.