source: src/LTL/LTL.ma @ 1222

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

LTL fully ported to the joint syntax.

File size: 1.3 KB
Line 
1include "joint/Joint.ma".
2include "common/Graphs.ma".
3
4definition ltl_params: params ≝
5 mk_params
6   unit unit unit unit registers_move Register
7     unit unit unit unit.
8
9definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params 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(*
17 
18record ltl_internal_function (globals: list ident): Type[0] ≝
19{
20  ltl_if_luniverse: universe LabelTag;
21  ltl_if_runiverse: universe RegisterTag;
22  ltl_if_stacksize: nat;
23  ltl_if_graph: ltl_statement_graph globals;
24  ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
25  ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
26}.
27
28inductive ltl_function_definition (globals: list ident): Type[0] ≝
29  | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
30  | ltl_fu_external_function: external_function → ltl_function_definition globals.
31 
32record ltl_program (globals: list (ident × nat)): Type[0] ≝
33{
34  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
35  ltl_pr_main: option ident
36}.
37*)
Note: See TracBrowser for help on using the repository browser.