Changeset 1379 for src/LTL


Ignore:
Timestamp:
Oct 14, 2011, 7:44:46 PM (8 years ago)
Author:
sacerdot
Message:

Invariant on LIN code removed. In Paris it was decided that a simpler invariant
(to be added later) holds: every function in graph format starts with a
label that is equal to the name of the funciton.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r1282 r1379  
    6666  let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
    6767  let reversed ≝ rev ? translated in
    68   let final ≝
    6968   map ??
    7069    (λs. let 〈l,x〉 ≝ s in
     
    7473          〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
    7574           x〉])
    76     reversed
    77   in
    78    dp … final ?.
    79 (*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *)
    80 cases daemon
    81 qed.
     75    reversed.
    8276
    8377definition translate_int_fun:
Note: See TracChangeset for help on using the changeset viewer.