Ignore:
Timestamp:
Apr 5, 2013, 6:04:14 PM (7 years ago)
Author:
tranquil
Message:

preliminary work on closing correctness.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLAxiom.ma

    r3014 r3096  
    1818(* what should we do with n? *)
    1919let 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 ∧
    2026∃[1] R.
    21   status_simulation
     27  status_simulation_with_init
    2228    (joint_status ERTL_semantics p_in stacksizes)
    2329    (joint_status LTL_semantics p_out stacksizes)
    24     R ∧
    25   ∀init_in.make_initial_state
    26     (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
    27   ∃init_out.
    28     make_initial_state
    29      (mk_prog_params LTL_semantics p_out stacksizes) =
    30       OK ? init_out ∧
    31    R init_in init_out.
     30    R init_in init_out.
Note: See TracChangeset for help on using the changeset viewer.