And also speedup implication checks for Boolean expressions.
* src/ltlvisit/simplify.cc: Improve implication-based rules
rules for multops by checking one operand against all the
other at once (instead of one by one). Do not break
Boolean expressions while performing implication checks.
* src/ltlvisit/simplify.hh: Typo.
* src/ltltest/reduccmp.test: More tests.
* src/ltlast/multop.cc, src/ltlast/multop.hh (multop::boolean_operands,
multop::boolean_count): New methods.
* src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh
(relabel): Take an optional relabeling_map as parameter.
(relabel_bse): New.
* src/ltltest/ltlrel.test, src/ltltest/ltlrel.cc: New files.
* src/ltltest/Makefile.am: Add them.
* src/bin/ltlfilt.cc: Add option --relabel-bool.
* src/ltltest/ltlfilt.test: Test it.
* NEWS: Mention it.
* doc/org/ltlfilt.org: Illustrate it.
* src/bin/common_output.cc: Add option --format and implement
it.
* src/bin/ltlfilt.cc, src/bin/randltl.cc: Document the
supported %-sequences.
* src/bin/genltl.cc: Document the %-sequences, and supply
the name of the pattern to output_formula().
* doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltlfilt.org,
NEWS: Document it.
* src/ltltest/latex.test: Use it.
* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case that is improved
by this.
* src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.test: Adjust.
* src/tgbaalgos/postproc.cc: Compute original_acc before calling
scc_filter(), and do not degeneralize the automaton before calling
tba_determinize() even when building a BA.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Greatly reduce
the number of clauses and variable by removing any path variable that
reference a reference transition that is not in a SCC.
* src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh
(to_latex_string): New function.
* src/bin/common_output.cc, src/bin/common_output.hh:
Add a --latex option.
* doc/tl/spotltl.sty: New file.
* doc/tl/Makefile.am: Distribute it.
* src/ltltest/latex.test: New test.
* src/ltltest/Makefile.am: Add it.
* NEWS: Mention it.
* src/misc/satsolver.cc, src/misc/satsolver.hh (satsolver_get_solution):
New function, that accepts a solution split on multiple 'v ' lines.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc (get_solution):
Remove, and adjust existing code to use satsolver_get_solution().
* src/tgbatest/readsat.cc, src/tgbatest/readsat.test: New files.
* src/tgbatest/Makefile.am: Add them.
* src/bin/man/spot-x.x: Mention the SAT competition rules for
the expected input/output format.
* src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh: Add
support for printing run-time.
* src/bin/ltl2tgba.cc, src/bin/dstar2tgba.cc: Compute
the run-time and show the option.
* NEWS: Mention it.
* src/tgbaalgos/isdet.cc: Simplify determinism check.
* src/tgbaalgos/isdet.hh, src/tgbaalgos/isdet.cc (is_complete): New
function.
* src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/bin/dstar2tgba.cc
src/bin/ltl2tgba.cc: Add escape sequence %p to the possible statistics
to show whether an automaton is complete.
* src/tgbatest/nondet.test: Add a couple more tests.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh:
Rename dba_sat_minimize to dtba_sat_minimize.
Make it possible to produce state-based automata, and do
not output useless clauses.
* src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh:
likewise, but also add the possibility to set the
target number of states, as in dtba_sat_minimize.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
Add new options for state-based computations and
setting acceptance and states number when using
dtgba_sat_minimize().
* src/tgbatest/ltl2tgba.cc: Adjust calls to
dtba_sat_minimize().
* src/tgbatest/satmin.test: Adjust calls.
* src/bin/ltlcross.cc: Complement deterministic automata,
and use them for additional intersection checks.
* NEWS, doc/org/ltlcross.org, src/bin/man/ltlcross.x: Document it.
This makes dstar2tgba able to produce a minimal WDBA when the input DRA
represent an obligation property.
* src/tgbaalgos/minimize.cc (minimize_obligation): When the
formula is not supplied but the input automaton is deterministic,
complement it to check the result of WDBA minimization.
* src/tgbatest/ltl2dstar.test, src/tgbatest/ltl2dstar2.test: Improve
tests.
Uses the value of the SPOT_SATSOLVER environment variable
to decide how to call the SAT solver.
* src/misc/satsolver.cc, src/misc/satsolver.hh: New files.
* src/misc/Makefile.am: Add them.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Use satsolver().
* src/tgbaalgos/postproc.cc: Use tba_determinize_check()
if option "tba-det" is set.
* src/tgbaalgos/postproc.hh (tba_determinize_): New attribute.
* src/tgbatest/det.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
