The gain is not very impressive. The runtime of the first example
in iface/dve2/README (also in dve2check.test) is 15% faster.
* src/tgba/tgbaproduct.hh (tgba_succ_iterator_product): Move ...
* src/tgba/tgbaproduct.cc (tgba_succ_iterator_product,
tgba_succ_iterator_product_common): ... in these two classes.
(tgba_succ_iterator_product_kripke): New class to speedup
successor computation on Kripke structures. We can assume that
all the transitions leaving the same state have the same label.
(tgba_product::tgba_product, tgba_product::succ_iter): Use
tgba_succ_iterator_product_kripke when appropriate.
(tgba_product_init::tgba_product_init): Adjust for the case
where tgba_product did reverse its operands.
* wrap/python/spot.i, wrap/python/buddy.i: Include <cstddef>
because Swig 2.0.2 uses ptrdiff_t and does not do the include
itself. In g++ most libstdc++ standard headers have been changed
to no longer include <cstddef> as an implementation detail, so
the difference shows.
* src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b"
to "a & b" if "a" is a pure eventual formula, remove the
constraint on "b".
* src/ltltest/reduccmp.test: Add two tests.
* 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.
Suggested by Yann Thierry-Mieg.
* iface/dve2/dve2.cc (convert_aps): Allow string on the right
of operators, and look them up.
* iface/dve2/dve2check.test: Test this syntax.
* iface/dve2/dve2.cc (compile_dve2): New function. Compile
the *.dve source if there is no newer *.dve2C already.
(load_dve2): Call compile_dve2 when given a *.dve file.
* iface/dve2/dve2.hh (load_dve2): Document it.
* src/ltlparse/ltlscan.ll: Do not recognize `.' as an AND. Allow
it in atomic propositions.
* src/evtgbaparse/evtgbascan.ll, src/tgbaparse/tgbascan.ll: Accept
`.' in identifiers.
* src/misc/bareword.cc (is_bareword): Accept `.' inside
barewords, so that there is no need to quote `X.Y'.
* src/ltltest/parse.test: Do not use `.' as and operator..
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.
* iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Retrieve
the name of all the state variables.
(dve2_kripke::format_state): Use them to format the name
of the state.
properties are still missing.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh: Add
classes for presenting the DiVinE2 model as a kripke object.
(load_dve2): Load the *.dve2C file using libltdl.
* iface/dve2/Makefile.am: Add a dve2check program.
* iface/dve2/dve2check.cc: New file. Currently it just
outputs the reachability graph using dotty.
Don't keep it under version control since it is installed by
autoreconf.
* configure.ac: Call LT_CONFIG_LTDL_DIR and LTDL_INIT.
* README: Mention ltdl/.
* Makefile.am: Recurse into ldtl.
* iface/dve2/Makefile.am: Link with it.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a new
assume_sba argument.
* src/tgbaalgos/dotty.cc (dotty_bfs): Take a new
mark_accepting_states arguments.
(dotty_bfs::process_state): Check if a state is accepting using
the state_is_accepting() method for tgba_sba_proxies, or by
looking at the first outgoing transition of the state. Pass
the result to the dectorator.
(dotty_reachable): Adjust function.
* src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc,
src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc
(state_decl): Add an "accepting" argument, and use it to
decorate accepting states with a double border.
* src/tgbatest/ltl2tgba.cc: Keep track of whether the output
is an SBA or not, so that we can tell it to dotty().
* wrap/python/ajax/spot.in: Likewise.
* wrap/python/cgi-bin/ltl2tgba.in: Likewise.
* src/tgba/tgbaexplicit.cc (tgba_explicit::compute_support_conditions):
Fix logic. This function has always been returning bddtrue instead
of the actual computed value...
* wrap/python/tests/run.in, iface/nips/nipstest/defs.in,
iface/gspn/defs.in: Do not disable VERBOSE when running from "make
check". Since we have started using parallel-check on 2009-08-31,
we should always send verbose output to the log.
* src/tgbatest/kv.test, iface/nips/nipstest/dotty.test: Don't rely
on the ${DOT-...} syntax, because DOT is always set and might be
set to the empty value.
access to that host.
* src/tgbatest/kv.test: Use ${DOT-true} instead of ${DOT-:}. I
don't know, the MacOS shell must be mixing the syntaxes for
${DOT:-} and ${DOT-:}.
* iface/nips/nipstest/dotty.test: Likewise
* src/tgbaalgos/sccfilter.cc (scc_filter): If the input automaton
is an instance of tgba_explicit_number, create a similar automaton
for output, instead of a tgba_explicit_string.
