Changeset 2946 for src/LTL


Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

Location:
src/LTL
Files:
2 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r2286 r2946  
    2727
    2828definition ltl_program ≝ joint_program LTL.
     29unification hint 0 ≔ ⊢ ltl_program ≡ joint_program LTL.
    2930
    3031coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝
     
    3233coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝
    3334  hdw_argument_from_reg on _r : Register to snd_arg LTL.
     35
     36definition LTL_premain : ∀p : ltl_program.joint_closed_internal_function LTL (prog_var_names ?? p) ≝
     37λp.
     38let l1 : label ≝ an_identifier … one in
     39let l2 : label ≝ an_identifier … (p0 one) in
     40let l3 : label ≝ an_identifier … (p1 one) in
     41let res ≝
     42  mk_joint_internal_function LTL (prog_var_names … p)
     43  (mk_universe … (p0 (p0 one)))
     44  (mk_universe … one)
     45  it it 0 0 (empty_map …) l1 in
     46(* todo: args for main? *)
     47let res ≝ add_graph … l1
     48  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
     49  res in
     50let res ≝ add_graph … l2
     51  (sequential … (CALL LTL ? (inl … (prog_main … p)) 4 it) l3)
     52  res in
     53let res ≝ add_graph … l3
     54  (GOTO ? l3)
     55  res in
     56res.
     57%
     58[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
     59  %
     60  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     61  |2: %
     62  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
     63  ]
     64| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     65| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     66| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     67| %{l2} %{(init_cost_label … p)} %
     68]
     69qed.
  • src/LTL/LTLToLINAxiom.ma

    r2868 r2946  
    88axiom LTLToLIN_ok :
    99∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
    10 ∀p_in : LTL_program.
     10∀p_in : joint_program LTL.
    1111let p_out ≝ ltl_to_lin p_in in
    1212∃[1] R.
     
    1414    (joint_status LTL_semantics p_in stacksizes)
    1515    (joint_status LIN_semantics p_out stacksizes)
    16     R.
     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.
  • src/LTL/LTL_semantics.ma

    r2845 r2946  
    33
    44definition LTL_semantics ≝
    5   mk_sem_graph_params LTL LTL_LIN_semantics.
     5  mk_sem_graph_params LTL LTL_LIN_semantics LTL_premain.
Note: See TracChangeset for help on using the changeset viewer.