source: src/LTL/LTL.ma @ 1280

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

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

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