Changeset 1246 for src/LTL


Ignore:
Timestamp:
Sep 22, 2011, 2:50:44 AM (8 years ago)
Author:
sacerdot
Message:

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

Location:
src/LTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1233 r1246  
    11include "joint/Joint.ma".
    2 include "common/Graphs.ma".
     2include alias "common/Graphs.ma".
    33
    4 definition ltl_params: params
    5  mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label.
     4definition ltl_params_: params_
     5 mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) label.
    66
    7 definition ltl_statement ≝ joint_statement ltl_params.
     7definition ltl_statement ≝ joint_statement ltl_params_.
    88
    9 (*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
    10  λglobals.
    11   mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)
     9definition ltl_params: ∀globals. params globals ≝
     10 λglobals. mk_params globals ltl_params_ (graph (ltl_statement globals)) (lookup …).
    1211
    1312definition ltl_program ≝ joint_program ltl_params.
  • src/LTL/LTLToLIN.ma

    r1236 r1246  
    22include "LIN/LIN.ma".
    33include "utilities/BitVectorTrieSet.ma".
    4 include "utilities/lists.ma".
     4include alias "common/Graphs.ma".
    55
    6 definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
     6definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
    77  λglobals: list ident.
    88  λs: ltl_statement globals.
     
    1111  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
    1212  | joint_st_goto l ⇒ joint_st_goto … l
    13   | joint_st_extension ext ⇒ joint_st_extension lin_params … ext
     13  | joint_st_extension ext ⇒ joint_st_extension lin_params_ … ext
    1414  ].
    1515
     
    2222  (globals: list ident) (g: label → option (ltl_statement globals))
    2323  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    24   (generated: list ((option label) × (lin_statement globals))) (l: label) (n: nat)
    25     on n: BitVectorTrieSet 16 × (list ((option label) × (lin_statement globals))) ≝
     24  (generated: list (lin_statement globals)) (l: label) (n: nat)
     25    on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
    2626  match n with
    2727  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
     
    6161definition translate_graph:
    6262 ∀globals. label → nat →
    63   (label → option (ltl_statement globals)) → (label → option (lin_statement globals))
     63  (label → option (ltl_statement globals)) → codeT … (lin_params globals)
    6464
    6565 λglobals,entry,labels_upper_bound,g.
     
    7777          〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
    7878           x〉])
    79     reversed in
    80   λl.
    81    find ?? (λs. let 〈l',x〉 ≝ s in
    82     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) final.
     79    reversed
     80  in
     81   dp … final ?.
     82(*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *)
     83cases daemon
     84qed.
    8385
    8486definition translate_int_fun:
    8587 ∀globals.
    86   joint_internal_function ltl_params globals
    87    joint_internal_function lin_params globals
     88  joint_internal_function … (ltl_params globals)
     89   joint_internal_function … (lin_params globals)
    8890
    8991 λglobals,f.
    90   mk_joint_internal_function lin_params globals
     92  mk_joint_internal_function globals (lin_params globals)
    9193   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
    9294    (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f)))
    93      (joint_if_lookup ?? f))
     95     (lookup ?? (joint_if_code … f)))
    9496    ??.
    9597cases daemon (*CSC: XXXXXXXXX Dead code produced *)
Note: See TracChangeset for help on using the changeset viewer.