source: src/LTL/LTLToLIN.ma @ 753

Last change on this file since 753 was 753, checked in by mulligan, 10 years ago

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