source: src/LTL/LTL.ma @ 753

Last change on this file since 753 was 753, checked in by mulligan, 9 years ago

Work from today.

File size: 877 bytes
Line 
1include "common/Graphs.ma".
2include "utilities/IdentifierTools.ma".
3
4include "LIN/LIN.ma".
5
6definition LTLStatement ≝ JointStatement Identifier.
7 
8definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).
9 
10record LTLInternalFunction (globals: list Identifier): Type[0] ≝
11{
12  LTL_IF_LUniverse: Universe;
13  LTL_IF_StackSize: nat;
14  LTL_IF_Graph: LTLStatementGraph globals;
15  LTL_IF_Entry: label;
16  LTL_IF_Exit: label
17}.
18
19inductive LTLFunctionDefinition (globals: list Identifier): Type[0] ≝
20  | LTL_Fu_InternalFunction: LTLInternalFunction globals → LTLFunctionDefinition globals
21  | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
22 
23record LTLProgram (globals: list (Identifier × nat)): Type[0] ≝
24{
25  LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));
26  LTL_Pr_Main: option Identifier
27}.
Note: See TracBrowser for help on using the repository browser.