Changeset 1222 for src/LTL/LTL.ma


Ignore:
Timestamp:
Sep 16, 2011, 11:02:23 AM (8 years ago)
Author:
sacerdot
Message:

LTL fully ported to the joint syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1183 r1222  
     1include "joint/Joint.ma".
    12include "common/Graphs.ma".
    2 include "utilities/IdentifierTools.ma".
    3 include "joint/Joint.ma".
    43
    54definition ltl_params: params ≝
     
    98
    109definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
    11  
    12 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
     10
     11definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
     12 λglobals.
     13  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).
     14
     15definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals).
     16(*
    1317 
    1418record ltl_internal_function (globals: list ident): Type[0] ≝
     
    3135  ltl_pr_main: option ident
    3236}.
     37*)
Note: See TracChangeset for help on using the changeset viewer.