source: src/LTL/LTL.ma @ 716

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

Finished translating LTL statements to LIN statements. Need to implement graph functions.

File size: 2.0 KB
Line 
1include "common/Graphs.ma".
2include "common/AST.ma".
3
4include "utilities/IdentifierTools.ma".
5
6include "ASM/I8051.ma".
7include "ASM/String.ma".
8
9inductive LTLStatement (globals: list Identifier): Type[0] ≝
10  | LTL_St_Skip: label → LTLStatement globals
11  | LTL_St_Comment: String → label → LTLStatement globals
12  | LTL_St_CostLabel: Identifier → label → LTLStatement globals
13  | LTL_St_Int: Register → Byte → label → LTLStatement globals
14  | LTL_St_Pop: label → LTLStatement globals
15  | LTL_St_Push: label → LTLStatement globals
16  | LTL_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → Identifier → label → LTLStatement globals
17  | LTL_St_FromAcc: Register → label → LTLStatement globals
18  | LTL_St_ToAcc: Register → label → LTLStatement globals
19  | LTL_St_OpAccs: OpAccs → label → LTLStatement globals
20  | LTL_St_Op1: Op1 → label → LTLStatement globals
21  | LTL_St_Op2: Op2 → Register → label → LTLStatement globals
22  | LTL_St_ClearCarry: label → LTLStatement globals
23  | LTL_St_Load: label → LTLStatement globals
24  | LTL_St_Store: label → LTLStatement globals
25  | LTL_St_CallId: Identifier → label → LTLStatement globals
26  | LTL_St_CondAcc: label → label → LTLStatement globals
27  | LTL_St_Return: LTLStatement globals.
28 
29definition LTLFunctionGraph ≝ λglobals. graph (LTLStatement globals).
30 
31record LTLInternalFunction (globals: list Identifier): Type[0] ≝
32{
33  LTL_IF_LUniverse: Universe;
34  LTL_IF_StackSize: nat;
35  LTL_IF_Graph: LTLFunctionGraph globals;
36  LTL_IF_Entry: label;
37  LTL_IF_Exit: label
38}.
39
40inductive LTLFunctionDefinition (globals: list Identifier): Type[0] ≝
41  | LTL_Fu_InternalFunction: LTLInternalFunction globals → LTLFunctionDefinition globals
42  | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
43 
44record LTLProgram (globals: list Identifier): Type[0] ≝
45{
46  LTL_Pr_Vars: list (Identifier × nat); (* 2nd component = size *)
47  LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition globals));
48  LTL_Pr_Main: option Identifier
49}.
Note: See TracBrowser for help on using the repository browser.