Changeset 1382 for src/LIN


Ignore:
Timestamp:
Oct 14, 2011, 10:50:56 PM (8 years ago)
Author:
sacerdot
Message:
  • succ_pc generalized to return a res (necessary for LIN semantics)
  • succ_pc implemented for LIN
Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1380 r1382  
    33
    44(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
    5 definition ltl_lin_more_sem_params: ∀succT:Type[0].∀succ:succT → address → address. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
     5definition ltl_lin_more_sem_params: ∀succT:Type[0].∀succ:succT → address → res address. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    66 λsuccT,succ.
    77 mk_more_sem_params ?
     
    2222
    2323definition ltl_lin_sem_params:
    24  ∀succT:Type[0].∀succ:succT → address → address. sem_params ≝
     24 ∀succT:Type[0].∀succ:succT → address → res address. sem_params ≝
    2525 λsuccT,succ.mk_sem_params … (ltl_lin_more_sem_params … succ).
    2626
    2727definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2828definition ltl_lin_pop_frame:
    29  ∀succT:Type[0].∀succ:succT → address → address. state … (ltl_lin_sem_params … succ) → res ((state … (ltl_lin_sem_params … succ)) × address) ≝
     29 ∀succT:Type[0].∀succ:succT → address → res address. state … (ltl_lin_sem_params … succ) → res ((state … (ltl_lin_sem_params … succ)) × address) ≝
    3030 λ_.λ_.fetch_ra ….
    3131definition ltl_lin_save_frame:
    32  ∀succT:Type[0].∀succ:succT → address → address. address → nat → unit → nat → unit → state … (ltl_lin_sem_params … succ) → res (state … (ltl_lin_sem_params … succ)) ≝
     32 ∀succT:Type[0].∀succ:succT → address → res address. address → nat → unit → nat → unit → state … (ltl_lin_sem_params … succ) → res (state … (ltl_lin_sem_params … succ)) ≝
    3333 λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3434
    35 definition ltl_lin_more_sem_params1 : ∀succT:Type[0].∀succ:succT → address → address.more_sem_params1 … ltl_lin_params1 ≝
     35definition ltl_lin_more_sem_params1 : ∀succT:Type[0].∀succ:succT → address → res address.more_sem_params1 … ltl_lin_params1 ≝
    3636 λsuccT,succ.
    3737 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params ? succ)
     
    3939
    4040(*CSC: XXXXX, for is_final only *)
    41 axiom ltl_lin_fetch_result: ∀succT:Type[0].∀succ:succT → address → address.state (ltl_lin_sem_params … succ) → res (list beval).
     41axiom ltl_lin_fetch_result: ∀succT:Type[0].∀succ:succT → address → res address.state (ltl_lin_sem_params … succ) → res (list beval).
    4242
    4343(*CSC: XXXX, for external functions only*)
    44 axiom ltl_lin_fetch_external_args: ∀succT:Type[0].∀succ:succT → address → address.external_function → state (ltl_lin_sem_params … succ) → res (list val).
    45 axiom ltl_lin_set_result: ∀succT:Type[0].∀succ:succT → address → address.list val → state (ltl_lin_sem_params … succ) → res (state (ltl_lin_sem_params … succ)).
     44axiom ltl_lin_fetch_external_args: ∀succT:Type[0].∀succ:succT → address → res address.external_function → state (ltl_lin_sem_params … succ) → res (list val).
     45axiom ltl_lin_set_result: ∀succT:Type[0].∀succ:succT → address → res address.list val → state (ltl_lin_sem_params … succ) → res (state (ltl_lin_sem_params … succ)).
    4646
    47 definition ltl_lin_exec_extended: ∀succT:Type[0].∀succ:succT → address → address.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params … succ) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ)))
     47definition ltl_lin_exec_extended: ∀succT:Type[0].∀succ:succT → address → res address.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params … succ) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ)))
    4848 ≝ λsuccT,succ,p,globals,ge,abs. ⊥.
    4949@abs qed.
  • src/LIN/semantics.ma

    r1380 r1382  
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 (*CSC: XXXX*)
    5 axiom lin_succ_pc: unit → address → address.
     4definition lin_succ_pc: unit → address → res address :=
     5 λ_.λaddr. addr_add addr 1.
    66
    77(*CSC: XXXXXXXXXX *)
Note: See TracChangeset for help on using the changeset viewer.