* src/bin/ltlcross.cc: Implement it.
* src/bin/man/ltlcross.x, doc/org/ltlcross.org, NEWS: Document it.
* src/tgbatest/ltl2dstar.test, src/tgbatest/ltlcross3.test: Test it.
* src/bin/ltlcross.cc: Report exit_status and exit_code columns in CSV
and JSON files. Also output lines for failed translations, and add
a --omit-missing option to disable that. Move the time column right
after exit_status and exit_code.
* src/bin/man/ltlcross.x: Document each column of the output.
* bench/ltl2tgba/tools: Use the "{name}cmd" notation.
* bench/ltl2tgba/sum.py: Adjust to the new columns.
* bench/ltl2tgba/README: Update to point to the man page for a
description of the columns.
* bench/ltl2tgba/Makefile.am: Build results.pdf as said announced in
README.
* bench/spin13/html.bottom: Update code to ignore these two new
columns and lines with null values.
* src/tgbatest/ltlcross3.test: Add tests.
* doc/org/ltlcross.org: Adjust examples.
* NEWS: Mention this.
* NEWS: Mention it.
* doc/org/ltlcross.org: Document it.
* src/bin/ltlcross.cc: Implement it.
* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
src/tgbatest/ltlcross4.test: Test it.
* src/misc/escape.cc, src/misc/escape.hh (escape_rfc4180): New
function.
* src/bin/ltlcross.cc: Do not output space after ',', use
"\r\n" for end of line, and use escape_rfc4180().
* NEWS: Mention it.
* 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/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/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/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.
Extended former conversion from DRA->DBA to handle
the case where some SCC is not DBA-realizable.
* src/dstarparse/dra2dba.cc: Rename as...
* src/dstarparse/dra2ba.cc: ... this.
(dra_to_dba, dra_to_dba_worker): Rename as...
(dra_to_ba, dra_to_ba_worker): ... these and extend.
* src/dstarparse/Makefile.am, src/dstarparse/public.hh,
src/dstarparse/dstar2tgba.cc, src/dstarparse/nra2nba.cc: Adjust.
* NEWS: Update the description of dstar2tgba accordingly.
* src/bin/dstar2tgba.cc, src/bin/man/dstar2tgba.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
* NEWS: Mention it.
* src/bin/ltl2tgba.cc, src/tgbaalgos/stats.cc, doc/org/ltl2tgba.org:
Rename the %S sequence as %c, for consistency with dstar2tgba.
* src/tgbatest/ltl2dstar.test: Add more tests.
* src/tgbatest/ltl2dstar2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* src/bin/ltlcross.cc: Add support for %D.
* src/bin/man/ltlcross.x: Add example.
* NEWS: Mention it.
* src/tgbatest/ltl2dstar.test: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbaalgos/degen.cc: Choose the initial level according
to acceptance condition common to all outgoing transitions.
* src/tgbatest/degenid.test: Add test case.
* NEWS: Mention it.
* src/tgbaalgos/word.cc, src/tgbaalgos/word.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltlcrossce.test: New file.
* src/tgbatest/Makefile.am: Add it.
* src/bin/ltlcross.cc: Compute and display an accepted word
for nonempty cross-products.
* NEWS, doc/org/ltlcross.org: Document it.
This follows from a discussion with Ernesto Posse.
The semantics for the {...} operator we use in Spot comes from the
cl(...) operator defined by Dax et al. (ATVA'09). This is slightly
different from the the way the PSL spec interprets a SERE used in the
context of a temporal formula (appendix B.3.1.1.2, item 7).
cl({a;b}[*]) would match any infinite word that starts with a;b, while
in PSL {a;b}[*] would match any infinite word that alternates a and b.
Spot documents that {SERE} in a temporal formula is interpreted like
cl(SERE) however it failed to ignore the empty prefix of SERE. So
{{a;b}[*]} would match anything, because the empty word is a prefix of
any word, and is also accepted by {a;b}[*]. Some trivial identities
and basic rewritings were also wrongly considering these empty
prefixes as well.
This patch therefore fixes the translation and syntactic
simplification rules, to really ignore these empty prefixes.
In some future version it should probably be wise to rename this {...}
operator as cl(...), and use {...} for the semantics given in appendix
B.3.1.1.2 (item 7) of the PSL specs.
* src/ltlast/unop.cc: Fix trivial identities. We have
{[*0]} = 0 and !{[*0]} = 1.
* src/ltlvisit/simplify.cc: Fix basic rewriting rules.
{e[*]} = {e} and !{e[*]} = !{e}.
* doc/tl/tl.tex: Adjust documentation.
* doc/tl/tl.bib (dax.09.atva): New entry.
* src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
infinite word for {e[*]} just because the empty
prefix is matched by e[*].
* src/tgbatest/ltl2tgba.test: Add a test case.
* NEWS: Mention it.
* THANKS: Add Ernesto.
These translator may output guards such as (a) || (b), but with the
changes in Spot 1.1.3 it would only work with ((a) || (b)).
Furthermore when ltlcross would fail to parse a neverclaim containing
such a guard, it would fail to parse all later neverclaims, because
the lexer was not properly reset.
* src/neverparse/neverclaimscan.ll: Scan (a) || (b) as a single
token.
(neverclaimyyopen): Reset the lexer.
* src/tgbatest/neverclaimread.test: Add a test for (a) || (b).
* NEWS: Update.
* src/bin/ltlcross.cc: Implement the new option. Average the product
statistics on all products.
* src/tgbatest/basimul.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlcross2.test, bench/ltl2tgba/tools: Use the new option.
* NEWS: Mention it.
* src/tgba/bdddict.cc, src/tgba/bdddict.hh
(unregister_all_typed_variables): New method.
* src/tgbaalgos/degen.cc (degeneralize): Use it.
* NEWS: Mention it.
* src/tgbaalgos/simulation.hh, src/tgbaalgos/simulation.cc
(simulation_sba, cosimulation_sba, iterated_simulations_sba): New
function. Also speedup the existing functions by avoiding
add_acceptince_conditions() and add_conditions(). Finally, use
scc_filter_states() when dealing with degeneralized automata.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh (do_ba_simul):
New method. Use it after degeneralization.
* src/tgba/tgbaexplicit.hh (get_transition, get_state): New methods.
* src/tgbatest/basimul.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
* NEWS: Introduce the new function and summarize the bug.
The main motivation is the upcoming patch that introduces
simulation_sba() and requires this function.
* src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: Implement it.
* src/tgbaalgos/postproc.cc: Use it for monitors, because we do not
care about acceptance conditions.
* NEWS: Mention it.
* src/bin/ltlfilt.cc: Handle --universal and --eventual. Match
only LTL formulas with --stutter-invariant.
* src/ltltest/ltlfilt.test: New file.
* src/ltltest/Makefile.am (TESTS): Add it.
* NEWS: Mention these bug fixes.
