source: src/ERTL/ERTLToLTLAxiom.ma @ 3096

Last change on this file since 3096 was 3096, checked in by tranquil, 7 years ago

preliminary work on closing correctness.ma

File size: 965 bytes
Line 
1include "ERTL/ERTLToLTL.ma".
2include "ERTL/ERTL_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6include "common/AssocList.ma".
7
8(* Inefficient, replace with Trie lookup *)
9definition lookup_stack_cost ≝
10 λp.λid : ident.
11  assoc_list_lookup ? ℕ id (eq_identifier …) p.
12
13axiom ERTLToLTL_ok :
14∀fix_comp : fixpoint_computer.
15∀colour : coloured_graph_computer.
16∀p_in : ertl_program.
17let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
18(* what should we do with n? *)
19let stacksizes ≝ lookup_stack_cost m in
20∀init_in.make_initial_state
21  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
22∃init_out.
23  make_initial_state
24   (mk_prog_params LTL_semantics p_out stacksizes) =
25    OK ? init_out ∧
26∃[1] R.
27  status_simulation_with_init
28    (joint_status ERTL_semantics p_in stacksizes)
29    (joint_status LTL_semantics p_out stacksizes)
30    R init_in init_out.
Note: See TracBrowser for help on using the repository browser.