Changeset 1246 for src/LTL/LTLToLIN.ma
 Timestamp:
 Sep 22, 2011, 2:50:44 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LTL/LTLToLIN.ma
r1236 r1246 2 2 include "LIN/LIN.ma". 3 3 include "utilities/BitVectorTrieSet.ma". 4 include "utilities/lists.ma".4 include alias "common/Graphs.ma". 5 5 6 definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝6 definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ 7 7 λglobals: list ident. 8 8 λs: ltl_statement globals. … … 11 11  joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it 12 12  joint_st_goto l ⇒ joint_st_goto … l 13  joint_st_extension ext ⇒ joint_st_extension lin_params … ext13  joint_st_extension ext ⇒ joint_st_extension lin_params_ … ext 14 14 ]. 15 15 … … 22 22 (globals: list ident) (g: label → option (ltl_statement globals)) 23 23 (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) 24 (generated: list ( (option label) × (lin_statement globals))) (l: label) (n: nat)25 on n: BitVectorTrieSet 16 × (list ( (option label) × (lin_statement globals))) ≝24 (generated: list (lin_statement globals)) (l: label) (n: nat) 25 on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝ 26 26 match n with 27 27 [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *) … … 61 61 definition translate_graph: 62 62 ∀globals. label → nat → 63 (label → option (ltl_statement globals)) → (label → option (lin_statement globals))63 (label → option (ltl_statement globals)) → codeT … (lin_params globals) 64 64 ≝ 65 65 λglobals,entry,labels_upper_bound,g. … … 77 77 〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?, 78 78 x〉]) 79 reversed in 80 λl. 81 find ?? (λs. let 〈l',x〉 ≝ s in 82 match l' with [ None ⇒ None …  Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) final. 79 reversed 80 in 81 dp … final ?. 82 (*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *) 83 cases daemon 84 qed. 83 85 84 86 definition translate_int_fun: 85 87 ∀globals. 86 joint_internal_function ltl_params globals→87 joint_internal_function lin_params globals88 joint_internal_function … (ltl_params globals) → 89 joint_internal_function … (lin_params globals) 88 90 ≝ 89 91 λglobals,f. 90 mk_joint_internal_function lin_params globals92 mk_joint_internal_function globals (lin_params globals) 91 93 (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f) 92 94 (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f))) 93 ( joint_if_lookup ?? f))95 (lookup ?? (joint_if_code … f))) 94 96 ??. 95 97 cases daemon (*CSC: XXXXXXXXX Dead code produced *)
Note: See TracChangeset
for help on using the changeset viewer.