source: src/LIN/LIN.ma @ 1517

Last change on this file since 1517 was 1379, checked in by sacerdot, 10 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
RevLine 
[1378]1include "LIN/joint_LTL_LIN.ma".
[1246]2include "utilities/lists.ma".
[491]3
[1378]4definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.
[1168]5
[1246]6definition pre_lin_statement ≝ joint_statement lin_params_.
[1379]7definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals).
[1168]8
[1246]9definition lin_params: ∀globals. params globals ≝
[1224]10 λglobals.
[1379]11  mk_params globals unit ltl_lin_params1 (list (lin_statement globals))
12   (λcode. λl.
[1246]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).
[1224]15
[1264]16definition lin_function ≝ λglobals. joint_function … (lin_params globals).
[1379]17definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.