 Timestamp:
 Mar 31, 2011, 5:53:16 PM (9 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/LTL/LTLToLIN.ma
r723 r728 1 1 include "LTL/LTL.ma". 2 2 include "LIN/LIN.ma". 3 include "utilities/BitVectorTrieSet.ma". 4 include "common/Graphs.ma". 3 5 4 6 definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝ … … 8 10 [ Joint_St_Return ⇒ Joint_St_Return ? globals 9 11  Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it 12  Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl 10 13 ]. 14 15 definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ 16 λl: Identifier. 17 λg: BitVectorTrieSet 16. 18 set_insert ? l g. 19 20 definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ 21 λl: Identifier. 22 λg: BitVectorTrieSet 16. 23 set_insert ? l g. 24 25 definition marked: Identifier → BitVectorTrieSet 16 → bool ≝ 26 λl: Identifier. 27 λg: BitVectorTrieSet 16. 28 set_member ? l g. 29 30 definition 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 36 let 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 (* 94 definition 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 *) 
src/LTL/LTLToLINI.ma
r722 r728 1 include "common/Graphs.ma".2 include "LTL/LTL.ma".3 4 definition fetch: ∀globals. LTLStatementGraph globals → label → option (LTLStatement globals) ≝5 λglobals: list Identifier.6 λgraph: LTLStatementGraph globals.7 λl: label.8 graph_lookup ? graph l.9 10 definition generate: ∀globals. LTLStatement globals → list (LTLStatement globals) → list (LTLStatement globals) ≝11 λglobals.12 λstatement.13 λstatements.14 statement :: statements. 
src/common/Graphs.ma
r726 r728 25 25 definition graph_add : ∀T. graph T → label → T → graph T ≝ 26 26 λT,g,l,v. insert T 16 l v g. 27 28
Note: See TracChangeset
for help on using the changeset viewer.