source: src/LTL/LTLToLIN.ma @ 714

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

Work on translation from LTL to LIN.

File size: 730 bytes
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    | _ ⇒ ?
21    ].
Note: See TracBrowser for help on using the repository browser.