source: src/LTL/LTLToLIN.ma @ 728

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

Changes from last two days.

File size: 3.7 KB
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3include "utilities/BitVectorTrieSet.ma".
4include "common/Graphs.ma".
5
6definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
7  λglobals: list Identifier.
8  λs: LTLStatement globals.
9    match s with
10    [ Joint_St_Return ⇒ Joint_St_Return ? globals
11    | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it
12    | Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl
13    ].
14   
15definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
16  λl: Identifier.
17  λg: BitVectorTrieSet 16.
18    set_insert ? l g.
19   
20definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
21  λl: Identifier.
22  λg: BitVectorTrieSet 16.
23    set_insert ? l g.
24   
25definition marked: Identifier → BitVectorTrieSet 16 → bool ≝
26  λl: Identifier.
27  λg: BitVectorTrieSet 16.
28    set_member ? l g.   
29   
30definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝
31  λglobals: list Identifier.
32  λl: Identifier.
33  λg: LTLStatementGraph globals.
34    graph_lookup ? g l.
35
36let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
37              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
38              (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
39  match n with
40  [ O ⇒ 〈required, generated〉
41  | S n' ⇒
42    let visited' ≝ mark l visited in
43    match fetch globals l g with
44    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
45    | Some statement ⇒
46      let translated_statement ≝ translate_statement globals statement in
47      let generated'' ≝ translated_statement :: generated in
48      match statement with
49      [ Joint_St_Sequential instr l2 ⇒
50        match instr with
51        [ Joint_Instr_CondAcc l1 ⇒
52            let required' ≝
53              if marked l2 visited' then
54                require l2 required
55              else
56                required in
57            let 〈required', generated''〉 ≝
58              if marked l2 visited' then
59                〈required', (Joint_St_Goto ? globals l2) :: generated''〉
60              else
61                visit globals g required' visited' generated'' l2 n' in
62            let required'' ≝ require l1 required' in
63              if ¬(marked l1 visited') then
64                visit globals g required'' visited' generated'' l1 n'
65              else
66                〈required', generated''〉
67        | _ ⇒
68          let required' ≝
69            if marked l2 visited' then
70              require l2 required
71            else
72              required in
73          if marked l2 visited' then
74            〈required', Joint_St_Goto ? globals l2 :: generated''〉
75          else
76            visit globals g required' visited' generated'' l2 n'
77        ]
78      | Joint_St_Goto lbl ⇒
79        let required' ≝
80          if marked lbl visited' then
81            require lbl required
82          else
83            required in
84        if marked lbl visited' then
85          〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
86        else
87          visit globals g required' visited' generated'' lbl n'
88      | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
89      ]
90    ]
91  ].
92
93(*
94definition translate_graph ≝
95  λglobals: list Identifier.
96  λg: LTLStatementGraph globals.
97  λentry: Identifier.
98    let visited ≝ set_empty ? in
99    let required ≝ set_insert ? entry (set_empty ?) in
100    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
101    let reversed ≝ rev ? translated in
102      filter (λs: PreLINStatement globals. ?) reversed.
103*)
Note: See TracBrowser for help on using the repository browser.