source: src/LTL/LTL.ma @ 1233

Last change on this file since 1233 was 1233, checked in by sacerdot, 9 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: 471 bytes
Line 
1include "joint/Joint.ma".
2include "common/Graphs.ma".
3
4definition ltl_params: params ≝
5 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label.
6
7definition ltl_statement ≝ joint_statement ltl_params.
8
9(*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
10 λglobals.
11  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)
12
13definition ltl_program ≝ joint_program ltl_params.
Note: See TracBrowser for help on using the repository browser.