Changeset 1222 for src/LTL/LTL.ma

Timestamp:

Sep 16, 2011, 11:02:23 AM (9 years ago)

Author:

sacerdot

Message:

LTL fully ported to the joint syntax.

File:

• src/LTL/LTL.ma (modified) (3 diffs)

src/LTL/LTL.ma

@@ +1 @@
+include "joint/Joint.ma".
 include "common/Graphs.ma".
-include "utilities/IdentifierTools.ma".
-include "joint/Joint.ma".
 
 definition ltl_params: params ≝
@@ -9 +8 @@
 
 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
-  
-definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
+
+definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
+ λglobals.
+  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).
+
+definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals).
+(*
   
 record ltl_internal_function (globals: list ident): Type[0] ≝
@@ -31 +35 @@
   ltl_pr_main: option ident
 }.
+*)