source: src/LTL/LTLToLIN.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: 1.4 KB
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3
4definition label_to_Identifier ≝
5  λl: label.
6  let n ≝ nat_of_pos l in
7    bitvector_of_nat 8 n.
8
9definition translate_statement ≝
10  λglobals: list Identifier.
11  λs: LTLStatement globals.
12    match s with
13    [ LTL_St_Skip lbl ⇒ LIN_St_Goto globals (label_to_Identifier lbl)
14    | LTL_St_Comment comment lbl ⇒ LIN_St_Comment globals comment
15    | LTL_St_CostLabel cost lbl ⇒ LIN_St_CostLabel globals cost
16    | LTL_St_Int register val lbl ⇒ LIN_St_Int globals register val
17    | LTL_St_Pop lbl ⇒ LIN_St_Pop globals
18    | LTL_St_Push lbl ⇒ LIN_St_Push globals
19    | LTL_St_Address ident proof address lbl ⇒ LIN_St_Address globals ident proof
20    | LTL_St_FromAcc register lbl ⇒ LIN_St_FromAcc globals register
21    | LTL_St_ToAcc register lbl ⇒ LIN_St_ToAcc globals register
22    | LTL_St_OpAccs opaccs lbl ⇒ LIN_St_OpAccs globals opaccs
23    | LTL_St_Op1 op1 lbl ⇒ LIN_St_Op1 globals op1
24    | LTL_St_Op2 op2 register lbl ⇒ LIN_St_Op2 globals op2 register
25    | LTL_St_ClearCarry lbl ⇒ LIN_St_ClearCarry globals
26    | LTL_St_Load lbl ⇒ LIN_St_Load globals
27    | LTL_St_Store lbl ⇒ LIN_St_Store globals
28    | LTL_St_CallId identifier lbl ⇒ LIN_St_CallId globals identifier
29    | LTL_St_CondAcc tgt lbl ⇒ LIN_St_CondAcc globals (label_to_Identifier tgt)
30    | LTL_St_Return ⇒ LIN_St_Return globals
31    ].
Note: See TracBrowser for help on using the repository browser.