Changeset 1312 for src/LTL


Ignore:
Timestamp:
Oct 6, 2011, 10:35:29 PM (8 years ago)
Author:
sacerdot
Message:

Type of frame operations (pop_frame/save_frame) generalized to take in account
the RTL semantics. LTL and LIN semantics fixed. Fixing of ERTL/RTL still to
be done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/semantics.ma

    r1303 r1312  
    22include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    5 definition ltl_pop_frame: unit → res unit ≝ λ_. OK … it.
    6 definition ltl_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it.
    7 
    84definition ltl_more_sem_params: more_sem_params ltl_params_ :=
    95 mk_more_sem_params ltl_params_
    10   unit hw_register_env graph_succ_p ltl_pop_frame ltl_save_frame
     6  unit hw_register_env graph_succ_p
    117   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    128    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
     
    2420definition ltl_sem_params: sem_params ≝ mk_sem_params … ltl_more_sem_params.
    2521
     22definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
     23definition ltl_pop_frame: state … ltl_sem_params → res (state … ltl_sem_params) ≝ λst. OK … st.
     24definition ltl_save_frame: state … ltl_sem_params → state … ltl_sem_params ≝ λst.st.
     25
     26definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
     27 mk_more_sem_params1 ? ltl_params1 ltl_more_sem_params
     28  ltl_init_locals ltl_pop_frame ltl_save_frame.
     29
    2630(*CSC: XXXXX, for is_final only *)
    2731axiom ltl_fetch_result: state ltl_sem_params → nat → res val.
     
    3741definition ltl_more_sem_params2: ∀globals. more_sem_params2 … (ltl_params globals) ≝
    3842 λglobals.
    39   mk_more_sem_params2 … ltl_more_sem_params ltl_init_locals
     43  mk_more_sem_params2 … ltl_more_sem_params1
    4044   (graph_fetch_statement …) ltl_fetch_result ltl_fetch_external_args ltl_set_result
    4145    (ltl_exec_extended …).
Note: See TracChangeset for help on using the changeset viewer.