Reported by Juraj Major.
* spot/twa/twa.hh: check num_sets() in prop_state_acc() so we do not
have to set it in set_acceptance(), causing trouble if set_acceptance()
is called multiple times.
* tests/python/setacc.py: New test case.
* tests/Makefile.am: Add it.
* THANKS: Add Juraj.
* NEWS: Mention the bug.
* spot/twaalgos/remfin.cc: Do not add a sink states to deterministic
weak automata, and actually apply the "weak" Fin-removal to any weak
automaton.
* tests/core/explprod.test: Add a test case for the previous patch,
but that used to fail because of this bug.
* NEWS: Mention the bug.
Jupyter 4.2 just landed in Debian unstable, so we have a few failures
because of all the renamings.
* tests/python/ipnbdoctest.py: Adjust imports for Jupyter 4.2.
This fixes the incorrect output of tgba_determinize() reported yesterday
by Reuben Rowe.
* spot/twaalgos/simulation.cc: Do not purge unreachable states when
recording implications.
* tests/python/bugdet.py: New test case.
* tests/Makefile.am: Add it.
* THANKS: Add Reuben.
* NEWS: Mention the bug.
Related to #188. This is a third fix that independently
makes `'utfilt --is-unambiguous -q smaller.hoa' instantaneous.
* spot/twaalgos/remfin.cc: Clean the received automaton if
necessary.
* bin/autfilt.cc: No need to call cleanup_acceptance_here() before
remove_fin() anymore.
* tests/core/remfin.test: Add an additional test.
* NEWS: Mention the change.
Avoid calling scc_info::determine_unknown_acceptance on the product, as
suggested in #188.
* spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite.
* tests/core/unambig.test: Add the automaton from #188.
* NEWS: Mention the improved function.
* spot/twaalgos/mask.cc,
spot/twaalgos/mask.hh (mask_keep_accessible_states): New function.
Suggested by František Blahoudek.
* bin/ltlcross.cc: Implement the two options.
* doc/org/ltlcross.org, NEWS: Document them.
* tests/core/complementation.test: Adjust test case.
* tests/core/ltlcross3.test, tests/core/unambig.test: More tests.
Report from František Blahoudek.
* bin/ltlcross.cc: Do not display stats for automata
that do not exist.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the fix.
This now holds the scc_info while processing the %c sequence, so that
using options we will soon be able to specify which SCC to count.
* spot/twaalgos/stats.hh, spot/twaalgos/stats.cc (printable_scc_info):
New class.
(state_printer): Use it for %c.
* spot/misc/formater.hh: Add move assignment.
* bin/common_aoutput.hh, bin/common_aoutput.cc: Use printable_scc_info
for %C.
* tests/core/format.test: Add a quick test case to make sure nothing
changed.
Fixes#91.
* bin/autfilt.cc, bin/dstar2tgba.cc: Implement reading CSV files.
* bin/common_finput.cc: Fix comments.
* bin/common_aoutput.cc: Show %<, %> in help text.
* NEWS, doc/org/csv.org: Document it.
* tests/core/readsave.test: Add a short test case.
Reported by Laurent Xu.
* python/spot/impl.i: Fix the iterator to return pointers instead of
references. Because references are ultimately copied.
* tests/python/automata.ipynb: Add test cases.
* NEWS: Mention it.
Part of #38.
* bin/ltlcross.cc: Implement it.
* NEWS: Mention it.
* doc/org/ltlcross.org: Adjust example.
* tests/core/ltlcrossce2.test: New test case.
For #184.
* spot/graph/graph.hh, spot/kripke/kripkegraph.hh,
spot/misc/bitvect.hh, spot/misc/common.hh, spot/misc/fixpool.hh,
spot/misc/mspool.hh, spot/misc/timer.hh, spot/tl/formula.hh,
spot/twa/acc.hh, spot/twa/taatgba.hh, spot/twa/twa.hh,
spot/twa/twagraph.hh, spot/twaalgos/emptiness_stats.hh,
spot/twaalgos/mask.hh, spot/twaalgos/ndfs_result.hxx,
spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.hh: Replace
assert() by SPOT_ASSERT(), or an exception, or nothing, depending
on the case.
* tests/sanity/style.test: Flag all asserts in headers.
* HACKING: Discuss assertions.
If no input have been specified, and the standard input is not a tty all
tools now default to reading it. If standard input is a tty, all tools
display an error message. Additionally, - is now a shorthand for -F- in
all tools.
* NEWS: Summarize this.
* bin/common_finput.cc, bin/common_finput.hh (check_no_formulas,
check_no_automaton): New functions that implement the above istty()
logic.
* bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc,
bin/ltlcross.cc, bin/ltldo.cc, bin/ltlgrind.cc: Use these function,
and recognize '-' if it was not the case.
* tests/core/acc_word.test, tests/core/ltldo.test,
tests/core/minusx.test, tests/core/readsave.test,
tests/core/unambig.test: Adjust some tests to exercise this.
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/ltl2tgba.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
doc/org/oaut.org: Adjust the documentation and simplify some
examples.
{e[*0..j]}<>->f = {e[*1..j]}<>->f
{e[*0..j]}[]->f = {e[*1..j]}[]->f
Fixes#81.
This required a small change to the bounded-star-normal-form to prevent
infinite recursion.
* spot/tl/simplify.cc: Implement these rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test: Add tests, and adjust others.
* tests/core/unambig.test: Replace formula that used to generated an
ambiguous automaton, but now generates a deterministic one.
if e is pure eventuality and g => e, then e U g = Fg
if u is purely universal and u => g, then u R g = Gg
Fixes#93.
* doc/tl/tl.tex, NEWS: Document the rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* tests/core/det.test: Adjust.
The streett_to_generalized_buchi() function was not tested unless
ltl2dstar is installed.
* tests/core/streett.test: New file.
* tests/Makefile.am: Add it.
Fixes#164.
* spot/twaalgos/stutter.hh, spot/twaalgos/stutter.cc: Implement
the determinization, while keeping it optional.
* NEWS: Mention the change.
* tests/core/ltl2dstar.test, tests/core/stutter-tgba.test: Add
test cases.
* tests/core/readsave.test: Adjust.
* spot/twa/twagraph.hh (twa_graph::edge_number): New method.
* spot/twaalgos/copy.cc: Copy the highlights if requested.
* tests/python/highlighting.ipynb: More tests.
Fixes#153.
* spot/twa/twa.cc, spot/twa/twa.hh: Add the methods.
* bin/autfilt.cc, bin/common_aoutput.hh, bin/ltlcross.cc,
tests/python/highlighting.ipynb, tests/python/word.ipynb: Use
them to simplify the code.
* NEWS: Mention them.
* bin/autfilt.cc: Add the option.
* NEWS: Mention it.
* tests/core/acc_word.test: Test it.
* spot/twaalgos/emptiness.cc,
spot/twaalgos/emptiness.hh (twa_run::project): New method.
* spot/twa/twa.hh (twa::get_or_set_named_prop): New method.
* spot/twaalgos/emptiness.cc, spot/twaalgos/isdet.cc: Use it to not
overwrite existing highlights.
* tests/core/det.test: Add test case.
* spot/twa/twa.cc, spot/twa/twa.hh: Add a way to
remove named properties.
* spot/twa/twagraph.cc: Clear highlight-edges on operations
that reorder the edge vector.
* spot/twaalgos/randomize.cc, spot/twaalgos/randomize.hh:
Preserve highlighted state, but not highlighted edges.
* spot/twaalgos/hoa.cc: Adjust output of highlight-edge
when the edges are not stored in order.
* tests/core/readsave.test, tests/core/tgbagraph.test,
tests/core/twagraph.cc: More test cases.
Reported by Ayrat Khalimov against the trans.html page when using
ltl3ba.
* spot/twaalgos/relabel.cc: Here.
* tests/core/ltl3dra.test: Test it.
* NEWS: Mention it.
* THANKS: Add Ayrat.
