Spot 0.7.1 used to need 190 acceptance conditions to translate the
188 literature formulae. With this patch we are down to 185.
That's not an impressive, but there are only ~20 formulae that
require more than 1 acceptance conditions; hence little room for
improvement.
* src/misc/bddlt.hh (bdd_hash): New function.
* src/misc/accconv.hh, src/misc/accconv.cc: New files.
* src/misc/Makefile.am: Add them.
* src/tgbaalgos/scc.cc (scc_map::build_map): Adjust
to record all combination of acceptance conditions occurring in a SCC.
* src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description.
* src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance
conditions that are always implied by another acceptance
conditions. Previously, we only removed acceptance conditions
that where always present in accepting SCCs.
* src/tgbatest/sccsimpl.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
states).
* src/tgbaalgos/tgbatba.cc: When degeneralizing to SBA, remove the
acceptance conditions that are common to all outgoing transitions
of this state. This helps to make the degeneralization
idempotent.
* src/tgbatest/degenid.test: New test case.
* src/tgbatest/Makefile.am: Add it.
after the simulation-reduction.
Report from Tomáš Babiak <xbabiak@fi.muni.cz>.
* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take
a tgba as input.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call
state_is_accepting() only if this tgba turns out to be
a tgba_sba_proxy. Otherwise check the acceptance of one
outgoing transition as we do in dotty_bfs since 2011-03-05.
* src/tgbatest/ltl2tgba.cc: Do not redegeneralize before
calling never_claim_reachable() if we know the automaton is
degeneralized already.
* src/tgbatest/ltl2tgba.test: Add a test case.
Reported by Tomáš Babiak <xbabiak@fi.muni.cz>.
* src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used
to record outgoing transitions by an Sgi::hash_map, and keep the
order of these transitions in a separate list.
* src/tgbatest/degendet.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
* THANKS: Add Tomáš and convert to utf8.
generate these formulae with "genltl".
* src/tgbatest/ltlcounter/: Remove this directory.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltlcounter.test, bench/ltlcounter/run: Use genltl
to generate the formulae.
* bench/ltlcounter/README: Do not mention src/tgbatest/ltlcounter/
anymore.
* src/misc/intvcomp.cc (stream_compression_base::run): Limit
repeatitions to 40, not 42.
(stream_decompression_base::refill): Refill the end of the stream
with 0.
(stream_decompression_base::look_n_bits): Add assertion.
* src/tgbatest/intvcomp.cc: Add a new test case.
* src/misc/intvcomp.cc, src/misc/intvcomp.cc: Add interfaces to
compress vector<int> to vector<unsigned>.
* src/tgbatest/intvcomp.cc: Test them.
* src/sanity/style.test: Refine check to avoid a spurious report.
* iface/dve2/dve2.cc: Adjust to use the new mspool allocator,
and get rid of the std::vector used to store compressed states.
* src/misc/intvcomp.hh: Add an "int* -> int*" interface
in addition to the "int* -> vector<unsigned>*" interface.
* src/tgbatest/intvcomp.cc: Test the two interfaces.
* iface/dve2/dve2.cc (dve2_compressed_state): New class.
(callback_context): Deal with general state*s, not dve2_state*s.
(transition_callback_compress): New function.
(dve2_kripke): Take a compress option.
(get_init_state, compute_state_condition, succ_iter,
format_state, state_condition): Handle compressed states.
(get_vars, compute_state_condition_aux): New helper methods.
* iface/dve2/dve2.hh (load_dve2): Add a compress option.
* iface/dve2/dve2check.cc: Add a -z option.
* iface/dve2/finite.test, iface/dve2/dve2check.test: Add more
tests.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Merge
state_explicit and tgba_explicit::state. In the past,
state_explicit was a small object encapsulating a pointer to the
persistent tgba_explicit::state; and we used to clone() and
destroy() a lot of state_explicit instance. Now state_explicit is
persistent, and clone() and destroy() have no effects.
* src/tgba/tgbareduce.cc: Adjust, since this inherits from
tgbaexplicit and uses the internals of state_explicit.
* src/tgbatest/reductgba.cc: Fix deletion order for automata.
* src/tgba/tgba.hh (last_support_conditions_input_,
last_support_variables_input_): Make these protected, so
they can be zeroed by tgba_explicit.
* 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/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/stats.hh (tgba_sub_statistics): New class.
(sub_stats_reachable): New function.
* src/tgbaalgos/stats.cc (sub_stats_bfs): New class.
(tgba_sub_statistics::dump, sub_stats_reachable): New function.
* src/tgbatest/ltl2tgba.cc (-kt): New option.
* src/tgbatest/ltl2tgba.test: Use -kt.
So far all neverclaims encountered would use (!(x)), but the
files from the Büchi store do not.
* src/neverparse/neverclaimscan.ll: Accept ! in front of guard,
so that we can read Promela files from Goal's Büchi store.
* src/tgbatest/neverclaimread.test: Test it.
* src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding
incorrect monitor if the input tgba is not deterministic.
* src/tgbatest/ltl2tgba.test: Add test case.
implement is_safety_mwdba().
Note: I swapped the name of safety and guarantee when I
implemented is_safety_automaton() on 2010-03-20. Fortunately,
is_safety_automaton() was only used where is_guarantee_automaton()
would have been correct.
* src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ...
(is_guarantee_automaton): ... this.
(is_safety_mwdba): New function.
* src/tgbaalgos/safety.hh: Adjust and add documentation.
* src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead
of is_safety_automaton().
* src/tgbatests/safety.test: Rename as ...
* src/tgbatests/obligation.test: ... this, and augment the
test.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc (-O): Display whether a formula
represent a safety, guarantee, or obligation property.
* NEWS: Adjust.
translation contain useless SCCs that where not ignored for
minimization.
* src/tgbaalgos/minimize.cc (minimize_wdba): Strip useless
SCCs before minimization.
* src/tgbatest/ltl2tgba.test: Add a check.
understood by Spot.
* src/neverparse/neverclaimparse.yy: Support "if :: false fi;"
instructions. Spin sometimes output these on dead states.
Also rewrite the "transitions" rule as a left recursion.
* src/tgbatest/neverclaimread.test: Adjust output because
of the right->left recursion change, and add two more formula
to submit to Spin to test its output.
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
(minimize): Split into ...
(minimize_wdba, minimize_monitor): ... these two functions.
* src/tgbatest/ltl2tgba.cc (main): Adjust the call to
minimize_monitor.
* wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to
minimize_monitor and minimize_obligation.
* wrap/python/spot.i: Declare minimize_monitor, minimize_wdba,
minimize_obligations.
* src/tgba/tgbaexplicit.hh (tgba_explicit_string)
(tgba_explicit_formula, tgba_explicit_number): Add fake
declarations so that SWIG can see they inherits from tgba.
correct from ltl2tgba to the library.
* src/tgbaalgos/minimize.hh,
src/tgbaalgos/minimize.cc (minimize_obligation): New function.
* src/tgbatests/ltl2tgba.cc (main): Fix constness of automata,
and call minimize_obligation() for -R3b.
* src/tgbatest/wdba.test: Speed up execution by running only a
couple of formula with valgrind. Half of those with`-l -R3b' and
the other half with `-f -R3'.
* src/tgbatest/ltl2tgba.cc (-M): New option for building
deterministic monitors.
* src/tgbaalgos/minimize.cc (minimize): Take a monitor
argument and adjust the code.
* src/tgbaalgos/minimize.hh (minimize): Document it.
* src/tgbaalgos/minimize.cc (init_sets, minimize): Fix memory
leaks and a usage of the wrong automaton.
* src/tgbatest/wdba.test: Try using -Rm with -R3 or -R3b, and with
valgrind. This caught all the bugs fixed above.
* src/tgbaalgos/minimize.cc (minimize): Don't add acceptance
conditions if the final set is empty.
* src/tgbaalgos/powerset.cc (tgba_powerset): Add the initial state
to acc_list if it is accepting. Also do not compute an SCC build
map if we don't have to build acc_list.
* src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when
it is correct. Either we can quickly determine that a formula or
its negation is a safety formula, or we can slowly check the
equivalence of the WDBA-minimized automaton and the original
automaton.
* src/tgbatest/wdba.test: New test.
* src/tgbatest/safety.test: Adjust comment.
* src/tgbatest/spotlbtt.test: Use -Rm.
* src/tgbatest/Makefile.am (TESTS): Add wdba.test.
* src/tgbatest/ltl2tgba.cc (main): Delete the minimized automaton.
* src/tgbaalgos/minimize.cc (minimize): Remove the call to
unregister_variable() at the end. It was both
wrong (unregistering only the first variable) and useless ("delete
del_a" will unregister all these variables). Use a map and a set
to keep track of free BDD variable and reuse them, otherwise the
algorithm would sometimes use more variables than allocated.
* src/tgbatest/minimize.cc: New file. Minimize an automaton
from a LTL formula and compare the size of the initial automaton
to the size of the minimized automaton.
With this change the output of
ltl2tgba -f -x -k -DS "GF(p_1) & ... & GF(p_n)
uses less than (n+1)^2 transitions when it used
exactly (n+1)*(2^n) transitions before.
* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Merge
transitions going to the same states if they are both accepting or
if neither are.
(state_ptr_bool_t, state_ptr_bool_less_than): Helper type to
store a transition in tgba_tba_proxy_succ_iterator.
* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh
(tgba_tba_proxy::transition_annotation): Remove. We cannot
implement this method if transitions are merged.
SCC information).
* src/tgbatest/ltl2tgba.cc (syntax, main): Add a -ks option.
* src/tgbatest/ltl2tgba.test, bench/ltlclasses/run,
bench/ltlcounter/run: Use -ks instead of -k to speed things up.
* src/tgbatest/ltl2tgba.cc (main): Either replay the accepting
run or print it, but do not do both.
* src/tgbatest/emptchk.test: Adjust. I.e. use -C instead of -CR
when we expect the run to be displayed.
* src/tgbatest/randtgba.cc (main): Remove the set but unused opt_A
variable (the upcoming GCC 4.6 would warn about it) and set opt_ec
to 1 if -A is used without -e.
