Commit graph

684 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
e7dc62e3c8 * NEWS: Add more news. 2014-08-19 14:57:35 +02:00
Alexandre Duret-Lutz
e5124faa13 man: more doc about TGBA and monitors
This was prompted by an exchange of emails with Caroline Lemieux.

* src/bin/man/ltl2tgba.x: Add notes and references.
* NEWS, THANKS: Update.
2014-08-19 14:52:51 +02:00
Alexandre Duret-Lutz
1eaaf8832a * NEWS: Mention recent removals. 2014-07-31 15:47:01 +02:00
Alexandre Duret-Lutz
6c76ba408e neverparse: Fix parsing of Modella's neverclaims.
Reported by František Blahoudek.

* src/neverparse/neverclaimparse.yy: Fix.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention the fix.
2014-05-29 15:48:31 +02:00
Alexandre Duret-Lutz
a4934c4f71 * NEWS: Mention recent fix. 2014-05-17 15:13:35 +02:00
Alexandre Duret-Lutz
53de8fc3a4 Merge branch 'master' into next
Conflicts:
	src/ltlvisit/simplify.cc
	src/tgbatest/Makefile.am
2014-05-15 14:30:49 +02:00
Alexandre Duret-Lutz
f431852af9 * NEWS, configure.ac: Bump version to 1.2.4a. 2014-05-15 12:13:29 +02:00
Alexandre Duret-Lutz
c11f15c76c Release Spot 1.2.4
* NEWS, configure.ac, doc/org/tools.org: Bump version.
2014-05-15 11:07:25 +02:00
Alexandre Duret-Lutz
d741d9266d simplify: remove an incorrect simplification rule
Fortunately was only enabled with the
ltl_simplifier_options::favor_event_univ option, which cannot yet be
turned on from the command-line tools.

* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/eventuniv.test: Adjust.
* NEWS: Mention the bug.
2014-05-13 17:31:51 +02:00
Alexandre Duret-Lutz
362862dace llt2tgba_fm: fix translation of ":" in some SERE
* src/tgbaalgos/ltl2tgba_fm.cc: Here.
* src/ltltest/reduccmp.test: Add a test case.
* NEWS: Mention it.
2014-05-13 17:09:11 +02:00
Alexandre Duret-Lutz
48471b5114 simplify: fix 3 incorrect simplification rules
* src/ltlvisit/simplify.cc: Remove two incorrect rules, and
partially disable another one.
* doc/tl/tl.tex: Reflect the change.
* src/ltltest/reduccmp.test: Likewise.
* src/ltltest/equals.cc: Add safety checks to catch such errors in the
future.
* NEWS: Mention the bug.
2014-05-13 16:59:51 +02:00
Alexandre Duret-Lutz
a5b6865c0b ltl2ta: fix a crash with --ta.
* src/taalgos/tgba2ta.cc: Do not assume the input is an sba.
* src/tgbatest/ltl2ta2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* NEWS: Mention the fix.
2014-04-07 18:21:10 +02:00
Alexandre Duret-Lutz
c4307e21ae * NEWS: Mention recent changes. 2014-04-07 18:21:10 +02:00
Alexandre Duret-Lutz
bd870f9ab8 tgba: remove the global_state and global_automaton argument of succ_iter
* iface/dve2/dve2.cc, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh,
src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbakvcomplement.hh, src/tgba/tgbamask.cc,
src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc:
Here.
* NEWS: Mention it.
2014-02-17 22:53:06 +01:00
Alexandre Duret-Lutz
0fba428cd9 tgba: remove the support_variable() method.
* src/kripke/fairkripke.cc, src/kripke/fairkripke.hh,
src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/tgba/taatgba.cc,
src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc:
Remove anything related to support_variables() and
compute_support_variables().
* NEWS: Mention it.
* src/tgbaalgos/powerset.cc: Adjust the computation of all possible
conditions.
2014-02-17 17:53:54 +01:00
Alexandre Duret-Lutz
358ea9ed87 * NEWS: Mention recent changes. 2014-02-14 14:21:44 +01:00
Alexandre Duret-Lutz
be43c1e957 * NEWS, configure.ac: Bump version to 1.2.3a. 2014-02-11 17:30:10 +01:00
Alexandre Duret-Lutz
2a7d5f5f7f Release Spot 1.2.3
* NEWS, configure.ac, doc/org/tools.org: Update version.
2014-02-11 17:20:58 +01:00
Alexandre Duret-Lutz
f567d88ff8 * NEWS: mention recent fixes. 2014-02-11 10:45:15 +01:00
Alexandre Duret-Lutz
eb778c569a sat: adjust SPOT_SATSOLVER default for glucose 3.0
* src/misc/satsolver.cc: Add the "-model" option.
* NEWS, doc/org/satmin.org, src/bin/man/spot-x.x: Mention it.
2014-02-08 21:34:35 +01:00
Alexandre Duret-Lutz
3c985a3235 sat: document the SPOT_SATLOG envvar
* doc/org/satmin.org, src/bin/man/spot-x.x: Document it.
* NEWS: Mention it.
2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
20824b96b9 timer: also consider the time spent in child processes
* src/misc/timer.hh: Fix.
* NEWS: Mention the bug.
2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
c2195600b8 Fix spurious failre with Pandas 0.13.
* src/tgbatest/ltlcross4.test: Work around Pandas 0.13.
* NEWS: Mention it.
2014-02-06 01:33:17 +01:00
Alexandre Duret-Lutz
38388748b0 * NEWS: Mention recent fixes. 2014-02-06 00:45:18 +01:00
Alexandre Duret-Lutz
494dbe2041 length: slight simplification
* src/ltlvisit/length.cc (length_boolone_visitor): Simplify.
* NEWS: Mention Alexandre's fix.
2014-02-03 09:49:30 +01:00
Alexandre Duret-Lutz
b6e5ce7e15 python: better support for Python 3
* wrap/python/spot.i (spot::ltl::parse_error_list,
spot::tgba_parse_error_list): Add a __bool__ method, that is used
instead of __nonzero__ in Python 3.
* wrap/python/tests/interdep.py, wrap/python/tests/parsetgba.py:
Force destruction order.
* NEWS: Update.
2014-02-02 15:45:19 +01:00
Alexandre Duret-Lutz
a6714119f9 * NEWS, configure.ac: Bump version to 1.2.2a. 2014-01-24 12:19:58 +01:00
Alexandre Duret-Lutz
35612f3626 Release Spot 1.2.2
* NEWS, configure.ac, doc/org/tools.org: Set version to 1.2.2.
2014-01-24 11:16:07 +01:00
Alexandre Duret-Lutz
ff816fbebb * NEWS: Update with recent fixes. 2014-01-15 16:42:53 +01:00
Alexandre Duret-Lutz
2febbd5929 * NEWS, configure.ac: Bump version to 1.2.1a 2013-12-11 11:38:27 +01:00
Alexandre Duret-Lutz
4d7638a269 Release Spot 1.2.1.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.1.
2013-12-11 10:40:33 +01:00
Alexandre Duret-Lutz
6c21089599 ltlcross: end CSV lines with \n, not \r\n
* src/bin/ltlcross.cc (print_stats_csv): Revert the recent
addition of \r, it is caussing too many issues.
* NEWS: Mention it.
2013-12-06 11:29:31 +01:00
Alexandre Duret-Lutz
846e33b9e5 ltl2tgba: Add a --csv-escape option and document CSV I/O.
* src/bin/common_output.cc, src/bin/common_output.hh:
(output_formula_checked, aut_stat_printer): New.
* src/bin/genltl.cc, src/bin/randltl.cc, src/bin/ltlfilt.cc: Call
output_formula_checked() instead of output_formula().
* src/bin/ltl2tgba.cc: Use aut_stat_printer and add option --csv-escape.
* doc/org/csv.org: New file to document CSV I/O.
* doc/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org, doc/org/ltl2tgba.org,
doc/org/tools.org: Link to csv.org
2013-12-06 11:09:36 +01:00
Alexandre Duret-Lutz
0faea814da bin: add support for reading formulas from CSV files.
* NEWS: Mention it.
* src/bin/common_finput.cc, src/bin/common_finput.hh: Implement it.
* src/bin/common_output.cc, src/bin/common_output.hh: Add the %< and
%> escapes.
* src/bin/ltlfilt.cc: Connect %< and %> to the
prefix andsuffix of the input, and document them.
* src/tgbatest/det.test, src/tgbatest/nondet.test: Simplify these
tests that read CSV files.
2013-12-06 11:09:36 +01:00
Alexandre Duret-Lutz
d719c706f4 ltlcross: report statistics about Rabin and Streett automata
* 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.
2013-11-22 08:59:13 +01:00
Alexandre Duret-Lutz
2b10745dfb ltlcross: support --products=+N
* src/bin/ltlcross.cc: Implement it.
* NEWS, doc/org/ltlcross.org: Document it.
* src/tgbatest/ltlcross3.test: Test it.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
f65c621a55 ltlcross: report exit_status and exit_code columns in CSV and JSON
* 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.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
686a45484d ltlcross: report missing input/output sequence
* src/bin/ltlcross.cc: Fix it.
* src/tgbatest/ltlcross3.test: New file.
* src/tgbatest/Makefile.am: Add it.
* NEWS: Mention it.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
7de25a32ef ltlcross: support short names
* 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.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
1c5536ea9c ltlcross: follow RFC 4180 for CSV output.
* 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.
2013-11-22 02:13:50 +01:00
Alexandre Duret-Lutz
65dc65b061 * NEWS, configure.ac: Bump version to 1.2a 2013-10-01 13:48:40 +02:00
Alexandre Duret-Lutz
c0a845b274 Release Spot 1.2.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.
2013-10-01 13:23:47 +02:00
Alexandre Duret-Lutz
87b65b9bce relabel: implement relabeling of Boolean subexpressions.
* 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.
2013-09-28 09:02:30 +02:00
Alexandre Duret-Lutz
536e45b342 Arrange multops so that Boolean arguments come first.
This helps recursive implication checks.  Also order
atomic propositions with strverscmp().

* src/ltlast/formula.hh (formula_ptr_less_than_multop,
is_literal, atomic_prop_cmp): New.
* src/ltlast/formula.cc (is_literal, atomic_prop_cmp): Implement them.
* src/ltlast/multop.cc: Use formula_ptr_less_than_multop.
* src/ltltest/isop.test, src/ltltest/ltlfilt.test,
src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/explicit.test, src/tgbatest/explpro2.test,
src/tgbatest/explpro3.test, src/tgbatest/explprod.test,
src/tgbatest/nondet.test, src/tgbatest/tripprod.test: Adjust tests.
* NEWS: Mention the new order.
2013-09-26 17:14:58 +02:00
Alexandre Duret-Lutz
ce5ea829bd tools: Add a --format option
* 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.
2013-09-22 23:56:56 +02:00
Alexandre Duret-Lutz
3076c3da4e org: document SAT-based minimization
* doc/org/satmin.org, doc/org/satmin.tex: New files.
* doc/Makefile.am: Add them.
* doc/org/tools.org: Point to satmin.org.
* NEWS: Mention satmin.html.
2013-09-16 08:39:06 +02:00
Alexandre Duret-Lutz
9cfe1a3496 tostring: add LaTeX output
* 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.
2013-09-08 20:43:53 +02:00
Alexandre Duret-Lutz
1ab46b0864 postproc: Add option to output Complete automata.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Tweak set_pref()
to also accept Any|Complete, Small|Complete, or Deterministic|Complete.
* src/bin/common_post.hh, src/bin/common_post.cc: Add option --complete
and set comp.
* src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Pass
comp to set_pref().
* src/tgbaalgos/complete.cc: Preserve state-based acceptance.
* src/tgbatest/dstar.test, src/tgbatest/ltlcross2.test,
src/tgbatest/nondet.test: Augment tests.
* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, NEWS: Document.
2013-09-08 20:43:52 +02:00
Alexandre Duret-Lutz
b31facffb1 * NEWS: Summarize recent changes 2013-09-08 20:43:52 +02:00
Alexandre Duret-Lutz
fdb157bf94 satmin: cleanup interfaces and minimization loops
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh:
(dtba_sat_minimize): Split into...
(dtba_sat_synthetize, dtba_sat_minimize): These.
(dtba_sat_minimize_dichotomy): New function.
* src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh
(dtgba_sat_minimize, dtgba_sat_synthetize): Likewise.
* src/tgbatest/ltl2tgba.cc: Adjust to new interface.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
Cleanup option processing for SAT options.
* src/tgbatest/satmin.test: Adjust.
* src/bin/spot-x.cc, src/bin/man/spot-x.x, NEWS: Document.
2013-09-08 20:43:17 +02:00