source: src/LTL/LTL.ma @ 1312

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

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

File size: 635 bytes
Line 
1include "joint/Joint.ma".
2
3definition ltl_params__: params__ ≝
4 (mk_params__ unit unit unit unit registers_move Register nat unit False).
5definition ltl_params_ : params_ ≝ graph_params_ ltl_params__.
6definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit.
7definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit.
8definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params1.
9
10definition ltl_statement ≝ joint_statement ltl_params_.
11
12definition ltl_program ≝ joint_program ltl_params.
13
14definition ltl_internal_function ≝
15 λglobals. joint_internal_function … (ltl_params globals).
Note: See TracBrowser for help on using the repository browser.