source: src/LIN/semantics.ma @ 1382

Last change on this file since 1382 was 1382, checked in by sacerdot, 8 years ago
  • succ_pc generalized to return a res (necessary for LIN semantics)
  • succ_pc implemented for LIN
File size: 448 bytes
Line 
1include "LIN/joint_LTL_LIN_semantics.ma".
2include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
3
4definition lin_succ_pc: unit → address → res address :=
5 λ_.λaddr. addr_add addr 1.
6
7(*CSC: XXXXXXXXXX *)
8axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc) → res (pre_lin_statement globals).
9
10definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement.
Note: See TracBrowser for help on using the repository browser.