Skip to content
  • Alexandre Duret-Lutz's avatar
    Add support for finite behaviors in the DVE interface. · cb83e855
    Alexandre Duret-Lutz authored
    * iface/dve2/dve2.hh (load_dve2): Take a "dead" argument.
    * iface/dve2/dve2.cc (callback_context): Add a destructor
    to simplify...
    (dve2_succ_iterator::~dve2_succ_iterator) ... this one.
    (convert_aps): Skip the dead proposition.
    (dve2_kripke::dve2_kripke): Take a dead argument, and
    setup alive_prop and dead_prop.
    (compute_state_condition, get_succ): Use a cache for the
    conditions and successor of the last state, to share
    some work between these two function.  Add loops on dead
    states.
    (load_dve2): Pass dead to dve2_kripke and convert_aps.
    * iface/dve2/dve2check.cc: Add a -dDEAD option.
    * iface/dve2/finite.test, iface/dve2/finite.dve: New file.
    * iface/dve2/Makefile.am: Declare them.
    cb83e855