source: src/LTL/LTL.ma @ 1246

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

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

File size: 451 bytes
Line 
1include "joint/Joint.ma".
2include alias "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
9definition ltl_params: ∀globals. params globals ≝
10 λglobals. mk_params globals ltl_params_ (graph (ltl_statement globals)) (lookup …).
11
12definition ltl_program ≝ joint_program ltl_params.
Note: See TracBrowser for help on using the repository browser.