source: src/LTL/LTL.ma @ 1326

Last change on this file since 1326 was 1281, checked in by sacerdot, 10 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.