Changeset 1359 for src/LTL


Ignore:
Timestamp:
Oct 11, 2011, 6:00:03 PM (8 years ago)
Author:
sacerdot
Message:
  1. more work on the RTL semantics
  2. changes to joint/semantics to accomodate the RTL one
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/semantics.ma

    r1324 r1359  
    2121
    2222definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    23 definition ltl_pop_frame: state … ltl_sem_params → res (state … ltl_sem_params) ≝ λst. OK … st.
    24 definition ltl_save_frame: state … ltl_sem_params → state … ltl_sem_params ≝ λst.st.
     23definition ltl_pop_frame: list beval → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λst. OK … st.
     24definition ltl_save_frame: unit → state … ltl_sem_params → state … ltl_sem_params ≝ λ_.λst.st.
    2525
    2626definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
     
    2929
    3030(*CSC: XXXXX, for is_final only *)
    31 axiom ltl_fetch_result: state ltl_sem_params → nat → res val.
     31axiom ltl_fetch_result: state ltl_sem_params → res (list beval).
    3232
    3333(*CSC: XXXX, for external functions only*)
Note: See TracChangeset for help on using the changeset viewer.