source: src/LTL/LTLToLIN.ma @ 716

Last change on this file since 716 was 716, checked in by mulligan, 10 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.