* src/tgba/sba.hh: New file, extrated from...
* src/tgba/tgbaexplicit.hh: ... here. Also rename
sba_explicit::is_accepting as sba_explicit::state_is_accepting for
consistency with tgba_sba_proxy.
* src/tgbatest/explicit2.cc: Adjust to the renaming.
* src/tgba/Makefile.am: Add sba.hh.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: Factor most of
the code in an explicit_graph<State, Type> that inherits from type.
The tgba_explicit type<State> now inherits from
explicit_graph<State,tgba>.
* src/ltlvisit/contain.cc, src/neverparse/neverclaimparse.yy
src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, src/tgbaalgos/cutscc.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/minimize.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/sccfilter.cc, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/explicit.cc,
src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc:
Replace tgba_explicit* by the actual type used.
* src/tgbatest/explicit2.cc: New file.
* src/tgbatest/Makefile.am: Add it.
* src/misc/intvcmp2.cc (stream_compression_base::run): Fix a case
where the "id" of the compression to use would be miscalculated,
causing wrong values to be encoded.
* src/tgbatest/intvcmp2.cc: Add this particular test case.
* src/tgbaalgos/minimize.cc (minimize_wdba): Fix the Löding
algorithm to use colors. The previous implementation was an
incorrect approximation.
* src/tgbatest/wdba2.test: New file showing two equivalent
formulas that were minimized in automata with different sizes.
* src/tgbatest/Makefile.am: Add it.
There is no point in degeneralizing an automaton if it can be WDBA
minimized. Doing so will only augment the number of states and
slow down the powerset construction used by the WDBA minimization.
* src/tgbatest/babiak.test: New file. It includes 5 formulae
which Tomáš Babiak reported Spot 0.7.1 would take over one hour to
translate if degeneralization and WDBA minimization were both
requested.
* src/tgbatest/Makefile.am (TESTS): Add it.
* src/tgbatest/ltl2tgba.cc: Do WDBA minimization before
degeneralization. The above formulae are now all translated in a
few seconds.
Especially with should write !(p0) and not !p0, because p0 is
usually #define'd by the user and he may have forgotten to quote
the value of the macro. This issue was discovered by Kristin
Yvonne Rozier and diagnosed by Gerard Holzmann.
* src/tgbaalgos/neverclaim.cc (process_link): Call
to_spin_string(..., true) to fully parentheses the string.
* src/tgbatest/neverclaimread.test: Add a test.
* src/neverparse/neverclaimscan.ll: Make the space between `!' and
`(' optional. This fixes the patch from 2011-02-07 that made this
space mandatory...
* src/tgbatest/neverclaimread.test: Augment test case.
* src/tgba/tgbasafracomplement.cc
(tgba_safra_complement::tgba_safra_complement)
(tgba_safra_complement::succ_iter): Correct the declaration and
use of multiple acceptance conditions.
(state_complement::to_string): Output the L set, not U. The previous
code caused different states to share the same names, causing issues
with the text-based output (state with identical names get merged).
* src/tgba/tgbasafracomplement.hh
(tgba_safra_complement::acceptance_cond_vec_): Adjust type to
store BDDs.
* src/tgbatest/complementation.cc: Implement a new "-b" option
to output automata in Spot's syntax.
* src/tgbatest/complementation.test: Add a test-case supplied
by Martin Dieguez Lodeiro.
* THANKS: Add Martin.
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.
