source: src/LIN/semantics.ma @ 1380

Last change on this file since 1380 was 1380, checked in by sacerdot, 8 years ago

LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma.
Very cool.

File size: 420 bytes
Line 
1include "LIN/joint_LTL_LIN_semantics.ma".
2include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
3
4(*CSC: XXXX*)
5axiom lin_succ_pc: unit → address → address.
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.