source: src/LIN/LIN.ma @ 1451

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

Invariant on LIN code removed. In Paris it was decided that a simpler invariant
(to be added later) holds: every function in graph format starts with a
label that is equal to the name of the funciton.

File size: 732 bytes
Line 
1include "LIN/joint_LTL_LIN.ma".
2include "utilities/lists.ma".
3
4definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.
5
6definition pre_lin_statement ≝ joint_statement lin_params_.
7definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals).
8
9definition lin_params: ∀globals. params globals ≝
10 λglobals.
11  mk_params globals unit ltl_lin_params1 (list (lin_statement globals))
12   (λcode. λl.
13    find ?? (λs. let 〈l',x〉 ≝ s in
14     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
15
16definition lin_function ≝ λglobals. joint_function … (lin_params globals).
17definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.