Reported by František Blahoudek.
* spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in
a non-deterministic automaton.
* tests/core/det.test: Add test case.
* NEWS: Mention the issue.
Reported by František Blahoudek.
* spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the bug.
* spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
that depend on the error. Based on a report from Shengping Shaw.
* THANKS: Add reporter.
* tests/core/ltlcross5.test: New file.
* tests/Makefile.am: Add it.
This fixes a complementation bug reported by Juraj Major and Tereza
Šťastná.
* spot/twaalgos/remfin.cc (is_scc_tba_type): Fix the condition for
handling Fin-alone pairs.
* tests/core/complement.test: Add Juraj & Tereza's test case.
* NEWS: Mention it.
* spot/twa/acc.hh (acc_cond::mark_t): Diagnose mark_t with set numbers
that are too larges.
* tests/python/except.py: Adjust.
* tests/core/acc.cc: Remove most of asserts, as those can be disabled,
and adjust expected exception.
* spot/twaalgos/aiger.cc: Simplify some bit operatitions. Force the
ordering of operations in aig_and, that was causing a test case to
fail on ARM, and greatly simplify the code and data structures used in
remove_unused().
* tests/core/ltlsynt.test: Adjust expected output.
Suggested by Victor Khomenko.
* bin/ltl2tgba.cc, bin/ltldo.cc: Implement it.
* doc/org/hierarchy.org: Use it.
* tests/core/ltldo2.test: Test it.
* bin/common_output.cc: Typo.
* NEWS: Mention the new option.
This was prompted by reports by Andrew Wells and Yong Li.
* NEWS, doc/tl/tl.tex: Document the changes.
* THANKS: Add Andrew.
* bin/ltlfilt.cc: Match --ltl before --from-ltlf if needed.
* spot/parsetl/parsedecl.hh, spot/parsetl/parsetl.yy,
spot/parsetl/scantl.ll: Parse X[!].
* spot/tl/formula.cc, spot/tl/formula.hh: Declare the new operator.
* spot/tl/ltlf.cc: Adjust to handle op::X and op::strong_X correctly.
* spot/tl/dot.cc, spot/tl/mark.cc, spot/tl/mutation.cc,
spot/tl/print.cc, spot/tl/simplify.cc, spot/tl/snf.cc,
spot/tl/unabbrev.cc, spot/twa/formula2bdd.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
tests/core/ltlgrind.test, tests/core/rand.test,
tests/core/sugar.test, tests/python/randltl.ipynb: Adjust.
* tests/core/ltlfilt.test, tests/core/sugar.test,
tests/core/utf8.test: More tests.
std::cerr will flush after each operator<< by default, so it's simpler
to use \n instead of std::endl, especially if we can merge \n into the
previous string. Ideally we should prefer \n for std::cout as well,
but there are reasonable cases where we want to call std::endl there,
so it's hard to enforce.
* tests/sanity/style.test: Diagnose occurrences of cerr.*<<.*endl.
* bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc, bin/ltlsynt.cc,
spot/tl/formula.cc, spot/twa/bdddict.cc, tests/core/checkpsl.cc,
tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
tests/core/length.cc, tests/core/ltlrel.cc, tests/core/parity.cc,
tests/core/randtgba.cc, tests/core/reduc.cc, tests/core/syntimpl.cc,
tests/ltsmin/modelcheck.cc: Fix them.
Reported by Salomon Sickert.
* spot/twaalgos/complement.cc: Make sure the output of postproc
is deterministic.
* tests/core/ltlcross.test: Add test case.
* NEWS: Mention the bug.
These rules come from Delag's paper, and help some cases
in issue #385.
* spot/tl/simplify.cc: Implement the simplification.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/385.test: New file.
* tests/Makefile.am: Add it.
* tests/core/reduccmp.test: More tests.
* tests/core/ltl2tgba2.test: Adjust one improved case.
* tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
Adjust expected output, as the cnf/dnf reorder some subformulas.
* bin/autcross.cc: Let complement() decide how to complement automata.
Do not apply remove_fin(), because we have a generic emptiness check
now. Use intersecting_word() instead of product()+accepting_word() so
that the former can maybe be optimized in the future.
* tests/core/autcross2.test: Adjust test case to use TGBA instead
of monitors, as calling complement() had a side-effect of setting
the "weak" property on the input.
* spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
output_aborter argument to abort if the output is too large.
* bin/ltlcross.cc: Use complement() with an output_aborter
so that ltlcross will not attempt to build complement larger
than 500 states or 5000 edges. Add --determinize-max-states
and --determinize-max-edges options.
* tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/stutter-inv.ipynb: Adjust test cases.
* NEWS: Document this.
* bin/spot-x.cc: Add documentation for postprocessor's
det-max-states and det-max-edges arguments.
* doc/org/ltlcross.org: Update description.
The first issue was reported by Victor Khomenko.
* spot/tl/formula.cc: Introduce a single-argument
version of sugar_delay().
* spot/parsetl/parsetl.yy: Use it.
* doc/tl/tl.tex, spot/tl/formula.hh: Adjust doc.
* tests/core/ltlfilt.test, tests/core/sugar.test: More tests.
Following a discussion with Victor Khomenko.
* doc/tl/tl.tex: Document those rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* spot/tl/formula.cc, spot/tl/formula.hh (formula::sugar_delay): New
function to implement this operator as syntactic sugar.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* doc/tl/tl.tex: Document the syntactic sugar rules and precedence.
* tests/core/sugar.test: Add tests.
* NEWS: Mention this new feature.
Since b[+] and [*0] are siSERE, b* is siSERE as well.
Suggested by Victor Khomenko.
* spot/tl/formula.cc: Implement that for Star and also
in the concatenation rule.
* tests/core/kind.test, tests/core/ltlfilt.test: Adjust.
Reported by Victor Khomenko.
* spot/tl/formula.cc: Rewrite the siPSL detection for ";".
* tests/core/ltlfilt.test: Add more tests.
* tests/core/kind.test: Adjust.
* NEWS: Mention the bug.
Report from David Müller.
* spot/twaalgos/simulation.cc: Add wrapper to deal with automata
sharing Fin/Inf sets.
* tests/core/ltl2tgba2.test: New test cases.
* NEWS: Mention the change.
* configure.ac: Test for <spawn.h>.
* bin/common_trans.cc: Use posix_spawn when available.
* NEWS: Mention the change.
* tests/core/ltldo.test: Adjust expected error message.
* spot/twaalgos/simulation.cc: Restrict common_in marks to current SCC
when pushing them, otherwise weak automata might become inherently
weak.
* tests/core/sim3.test: Add test case.
* spot/twaalgos/dot.cc: Implement support for hidding labels.
* tests/core/readsave.test: Test it.
* bin/common_aoutput.cc: Add --help text.
* NEWS: Mention it.
