Changeset 3156 for src/correctness.ma


Ignore:
Timestamp:
Apr 17, 2013, 3:24:22 PM (7 years ago)
Author:
campbell
Message:

Rebuild prefix traces in back-end's preferred form.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r3145 r3156  
    2323  let ctrace ≝ costlabels_of_observables itrace in
    2424  Σ_{l ∈ ctrace}(costmap l).
     25
     26definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝
     27λC,p,m.
     28  let g ≝ make_global … (pcs_exec … C) p in
     29  let C' ≝ pcs_to_cs C g in
     30  ! s0 ← make_initial_state … p;
     31  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
     32  return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉.
    2533
    2634definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝
     
    8593
    8694(* atm they are all axioms *)
    87 include "RTLabs/RTLabsExecToTrace.ma".
    8895include "RTLabs/RTLabsToRTLAxiom.ma".
    8996include "RTL/RTL_separate_to_overflow.ma".
     
    166173#ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
    167174#OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
    168 #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
     175#ra_s0 * #ra_s1 * #ra_s2 * #fn * #ra_init * #ra_ft * * #ra_ft_fn #ra_ft_obs * #ra_tlr * * #ra_unrepeating #ra_max #ra_obs'
    169176>OBS -ra_meas
    170 cases (produce_rtlabs_flat_trace … ra_exec_prefix)
    171 #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
    172177%{prefix} %{subtrace} %{fn} %[%]
    173 %{ra_init_ok ra_max}
    174 %{ra_unrepeating EQ_ra_pref_obs ra_obs'}
    175 (* fn is the current function ... *) cases daemon
     178%{ra_init ra_max}
     179%{ra_unrepeating ra_ft_obs ra_ft_fn ra_obs'}
    176180qed.
    177181
Note: See TracChangeset for help on using the changeset viewer.