source: src/ERTL/ERTLToLTLAxiom.ma @ 3195

Last change on this file since 3195 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 810 bytes
RevLine 
[3014]1include "ERTL/ERTLToLTL.ma".
2include "ERTL/ERTL_semantics.ma".
[2946]3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6include "common/AssocList.ma".
7
[3014]8axiom ERTLToLTL_ok :
[2946]9∀fix_comp : fixpoint_computer.
10∀colour : coloured_graph_computer.
[3014]11∀p_in : ertl_program.
12let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
[2946]13(* what should we do with n? *)
[3145]14let stacksizes ≝ stack_sizes m in
[3096]15∀init_in.make_initial_state
16  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
17∃init_out.
18  make_initial_state
19   (mk_prog_params LTL_semantics p_out stacksizes) =
20    OK ? init_out ∧
[2946]21∃[1] R.
[3096]22  status_simulation_with_init
[3014]23    (joint_status ERTL_semantics p_in stacksizes)
[2946]24    (joint_status LTL_semantics p_out stacksizes)
[3096]25    R init_in init_out.
Note: See TracBrowser for help on using the repository browser.