- Timestamp:
- Apr 14, 2011, 5:54:37 PM (10 years ago)
- Location:
- src/ERTL
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTL.ma
r745 r753 58 58 ERTL_Pr_Main: option Identifier 59 59 }. 60 61 definition ERTL_Pr_Vars: ERTLProgram → list (Identifier × nat). 62 # E 63 cases E 64 # H1 # H2 # H3 65 @ H1 66 qed. -
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.