Skip to content
  • Alexandre Duret-Lutz's avatar
    Teach the DVE2 interface about atomic propositions such as "a <= · 8136bd41
    Alexandre Duret-Lutz authored
    10" or "b != 3".  This only work for integer variables presently.
    
    * iface/dve2/dve2.hh (load_dve2): Take an atomic_prop_set
    argument to indicate the AP to observe.
    * iface/dve2/dve2.cc (convert_aps): New function.  Parse the
    atomic propositions in format them in a prop_set structure that
    will allow fast generation of the state condition.
    (load_dve2): Call convert_aps, and pass the resulting prop_set
    structure to the kripke object.
    (dve2_kripke::dve2_kripke): Store the prop_set structure.
    (dve2_kripke::~dve2_kripke): Release the prop_set, and unregister
    the bdd_variable associated to it.
    (compute_state_condition): New method that uses the prop_set.
    (succ_iter, state_condition): Call compute_state_condition().
    * iface/dve2/dve2check.cc: Adjust the call to load_dve2 to
    pass it atomic propositions read from the command line.
    8136bd41
To find the state of this project's repository at the time of any of these versions, check out the tags.