source: src/LIN/LIN.ma @ 1233

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

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File size: 744 bytes
Line 
1include "joint/Joint.ma".
2
3definition lin_params: params ≝
4 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit.
5
6definition lin_statement ≝ joint_statement lin_params.
7
8definition well_formed_P ≝
9  λA, B: Type[0].
10  λcode: list (option A × B).
11    match code with
12    [ nil ⇒ False
13    | cons hd tl ⇒
14      match \fst hd with
15      [ Some lbl ⇒ False
16      | None ⇒ True]].
17
18(*
19definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
20 λglobals.
21  mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
22(*CSC: lookup function to be implemented *)
23cases daemon
24qed.
25*)
26
27definition ltl_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.