source: src/LTL/LTL.ma @ 723

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

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

File size: 921 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): Type[0] ≝
24{
25  LTL_Pr_Vars: list (Identifier × nat); (* 2nd component = size *)
26  LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition globals));
27  LTL_Pr_Main: option Identifier
28}.
Note: See TracBrowser for help on using the repository browser.