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/LTL/LTLToLINAxiom.ma

    r2946 r3096  
    1010∀p_in : joint_program LTL.
    1111let p_out ≝ ltl_to_lin p_in in
     12∀init_in.make_initial_state
     13  (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in →
     14∃init_out.
     15  make_initial_state
     16   (mk_prog_params LIN_semantics p_out stacksizes) =
     17    OK ? init_out ∧
    1218∃[1] R.
    13   status_simulation
     19  status_simulation_with_init
    1420    (joint_status LTL_semantics p_in stacksizes)
    1521    (joint_status LIN_semantics p_out stacksizes)
    16     R ∧
    17   ∀init_in.make_initial_state
    18     (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in →
    19   ∃init_out.
    20     make_initial_state
    21      (mk_prog_params LIN_semantics p_out stacksizes) =
    22       OK ? init_out ∧
    23    R init_in init_out.
     22    R init_in init_out.
Note: See TracChangeset for help on using the changeset viewer.