Changeset 1380 for src/LTL/semantics.ma
- Timestamp:
- Oct 14, 2011, 10:25:03 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/semantics.ma
r1378 r1380 1 include " joint/SemanticUtils.ma".1 include "LIN/joint_LTL_LIN_semantics.ma". 2 2 include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *) 3 3 4 definition ltl_more_sem_params: more_sem_params ltl_params_ :=5 mk_more_sem_params ltl_params_6 unit hw_register_env graph_succ_p7 hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)8 (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)9 (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)10 (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)11 (λlocals,dest_src.12 match dest_src with13 [ from_acc reg ⇒14 do v ← hwreg_retrieve locals RegisterA ;15 hwreg_store reg v locals16 | to_acc reg ⇒17 do v ← hwreg_retrieve locals reg ;18 hwreg_store RegisterA v locals ])19 pointer_of_label.20 definition ltl_sem_params: sem_params ≝ mk_sem_params … ltl_more_sem_params.21 22 definition 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) × address) ≝24 fetch_ra ….25 definition ltl_save_frame:26 address → nat → unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝27 λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.28 29 definition ltl_more_sem_params1 : more_sem_params1 … ltl_lin_params1 ≝30 mk_more_sem_params1 ? ltl_lin_params1 ltl_more_sem_params31 ltl_init_locals ltl_pop_frame ltl_save_frame.32 33 (*CSC: XXXXX, for is_final only *)34 axiom ltl_fetch_result: state ltl_sem_params → res (list beval).35 36 (*CSC: XXXX, for external functions only*)37 axiom ltl_fetch_external_args: external_function → state ltl_sem_params → res (list val).38 axiom ltl_set_result: list val → state ltl_sem_params → res (state ltl_sem_params).39 40 definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → label → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))41 ≝ λglobals,ge,abs. ⊥.42 @abs qed.43 44 definition ltl_more_sem_params2: ∀globals. more_sem_params2 … (ltl_params globals) ≝45 λglobals.46 mk_more_sem_params2 … ltl_more_sem_params147 (graph_fetch_statement …) ltl_fetch_result ltl_fetch_external_args ltl_set_result48 (ltl_exec_extended …).49 50 4 definition ltl_fullexec ≝ 51 joint_fullexec … (λp. ltl_more_sem_params2 (prog_var_names … p)). 52 5 ltl_lin_fullexec … (graph_succ_p …) … (graph_fetch_statement … (ltl_lin_sem_params …)). 53 6 54 7 (*
Note: See TracChangeset
for help on using the changeset viewer.