Changeset 753 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Apr 14, 2011, 5:54:37 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r752 r753 1 1 include "ERTL/ERTL.ma". 2 3 axiom translate_func: 2 include "LTL/LTL.ma". 3 4 axiom translate_ERTL_func: 4 5 ∀globals: list Identifier. 5 6 list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)). 6 7 7 definition translate: ERTLProgram → LTLProgram≝8 definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e) ≝ 8 9 λp. 9 let globals ≝ map ? ? \fst (ERTL_Pr_Vars e) in 10 let ltl_pr_var ≝ ERTL_Pr_Vars e in 11 let ltl_pr_funcs ≝ map ? ? (translate_func globals) (ERTL_Pr_Funcs e) in 10 let globals ≝ map ? ? \fst (ERTL_Pr_Vars p) in 11 let ltl_pr_funcs ≝ map ? ? ? (ERTL_Pr_Funcs p) in 12 mk_LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main p). 13 # H1 14 @ (translate_ERTL_func globals) in ⊢ (? × %) (* dpm here *)
Note: See TracChangeset
for help on using the changeset viewer.