source: src/LTL/LTLToLIN.ma @ 733

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

Fixed partial commit.

File size: 4.3 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
36definition foo ≝ λl2,visited,required,globals,generated,g,n.
37 λvisit:∀globals: list Identifier.∀g: LTLStatementGraph globals.∀required: BitVectorTrieSet 16.
38  ∀visited: BitVectorTrieSet 16.∀generated: list (PreLINStatement globals).∀l: Identifier.
39  ∀n: nat.BitVectorTrieSet 16 × (list (PreLINStatement globals)).
40  if marked l2 visited then
41    〈require lbl required, (Joint_St_Goto ? globals l2) :: generated〉
42  else
43   visit globals g required visited generated l2 n.
44
45let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
46              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
47              (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
48  match n with
49  [ O ⇒ 〈required, generated〉
50  | S n' ⇒
51    let visited' ≝ mark l visited in
52    match fetch globals l g with
53    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
54    | Some statement ⇒
55      let translated_statement ≝ translate_statement globals statement in
56      let generated'' ≝ translated_statement :: generated in
57      match statement with
58      [ Joint_St_Sequential instr l2 ⇒
59        match instr with
60        [ Joint_Instr_CondAcc l1 ⇒
61            let required' ≝
62              if marked l2 visited' then
63                require l2 required
64              else
65                required in
66            let 〈required', generated''〉 ≝
67             foo l2 visited' required' globals generated'' g n' visit (*
68              if marked l2 visited' then
69                〈required', (Joint_St_Goto ? globals l2) :: generated''〉
70              else
71                visit globals g required' visited' generated'' l2 n'*) in
72            let required'' ≝ require l1 required' in
73              if ¬(marked l1 visited') then
74                visit globals g required'' visited' generated'' l1 n'
75              else
76                〈required', generated''〉
77        | _ ⇒
78          let required' ≝
79            if marked l2 visited' then
80              require l2 required
81            else
82              required in
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'
87        ]
88      | Joint_St_Goto lbl ⇒
89        let required' ≝
90          if marked lbl visited' then
91            require lbl required
92          else
93            required in
94        if marked lbl visited' then
95          〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
96        else
97          visit globals g required' visited' generated'' lbl n'
98      | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
99      ]
100    ]
101  ].
102
103(*
104definition translate_graph ≝
105  λglobals: list Identifier.
106  λg: LTLStatementGraph globals.
107  λentry: Identifier.
108    let visited ≝ set_empty ? in
109    let required ≝ set_insert ? entry (set_empty ?) in
110    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
111    let reversed ≝ rev ? translated in
112      filter (λs: PreLINStatement globals. ?) reversed.
113*)
Note: See TracBrowser for help on using the repository browser.