Commit graph

345 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
cf9ad8ebd1 org: minor tweaks
* doc/org/ltlfilt.org: Update example.
* doc/org/ioltl.org: Explain %s briefly.
2017-01-12 21:04:38 +01:00
Alexandre GBAGUIDI AISSE
823dc56e6b Update NEWS and documentations
* NEWS: Update.
* doc/org/satmin.org: Update satmin page.
* bin/man/spot-x.x: Document SPOT_XCNF and edit SPOT_SATSOLVER.
* bin/spot-x.cc: Update satmin options.
* bin/autfilt.cc: Update satmin related documentations.
* bin/man/autfilt.x: Update autfilt options.
2017-01-06 19:53:21 +01:00
Alexandre Duret-Lutz
4b01387817 support for semi-deterministic property
* spot/twa/twa.hh (prop_semi_deterministic): New methods.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the
semi-deterministic property.
* doc/org/concepts.org, doc/org/hoa.org: Document it.
* spot/twaalgos/isdet.cc,
spot/twaalgos/isdet.hh (is_semi_deterministic): New function.
* bin/autfilt.cc: Add --is-semi-deterministic.
* bin/common_aoutput.cc: Add --check=semi-deterministic.
* tests/core/semidet.test: New file.
* tests/Makefile.am: Add it.
* tests/core/parseaut.test, tests/core/readsave.test: Adjust.
2016-12-29 16:37:43 +01:00
Alexandre Duret-Lutz
12f6c8cf10 twa_graph: add a merge_univ_dests() method
and call it after parsing

* spot/twa/twagraph.cc, spot/twa/twagraph.hh
(twa_graph::merge_univ_dests): New method.
* spot/parseaut/parseaut.yy: Call it.
* spot/twaalgos/dot.cc: Improve output, now that
several edges can use the same universal destination.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/parseaut.test, tests/python/_altscc.ipynb,
tests/python/alternating.py, tests/python/alternation.ipynb: Adjust
test case.
* doc/org/tut24.org: Adjust example.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
3d0a971aa8 org: examples with alternating automata
* doc/org/tut23.org, doc/org/tut24.org, doc/org/tut31.org: New files.
* doc/Makefile.am, doc/org/tut.org: Add them.
* doc/org/hoa.org, doc/org/concepts.org: Adjust for alternation support.
* NEWS: Add links.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
87c9d6f039 ltlcross: add support for alternating automata
* bin/ltlcross.cc: Add an alternation-removal pass, and
adjust CSV output.
* doc/org/ltlcross.org: Update.
* tests/core/ltl3dra.test, tests/core/ltl3ba.test: Add more tests.
* tests/Makefile.am: Add tests/core/ltl3ba.test.
* NEWS: Mention it.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
fa06cfa303 alternation: implement remove_alternation() for weak alt automata
This mixes the subset construction (for 1-state rejecting SCCs) and
the breakpoint construction (for larger rejecting SCCs).  The
algorithm should probably be rewritten in a cleaner and more efficient
way, but that should do for a first version.  It should be easy to
extend it to support Büchi acceptance (since the breakpoint
construction works for this) when we need it.

* spot/twaalgos/alternation.hh,
spot/twaalgos/alternation.cc (remove_alternation): New function.
* tests/python/alternation.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
2016-12-29 12:57:16 +01:00
Alexandre Duret-Lutz
582d455c23 twa: add support for very-weak property
* spot/twa/twa.hh: Implement the property.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input
and output for it.
* spot/twaalgos/strength.cc,
spot/twaalgos/strength.hh (is_very_weak_automaton): New function.
* tests/core/alternating.test: Add a test for --check=strength
on an alternating automaton.
* tests/core/strength.test, tests/core/parseaut.test: Adjust expected
output.
* NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it.
2016-12-27 12:36:38 +01:00
Alexandre Duret-Lutz
dcd21aaabf org: call set_init_state() in tut22
* doc/org/tut22.org: Here.
2016-12-25 12:27:17 +01:00
Alexandre Duret-Lutz
34ac6f08cc org: ltlcross supports any acceptance condition
* doc/org/ltlcross.org: Also fix the documentation of terminal and
weak SCCs.
2016-12-24 21:08:01 +01:00
Alexandre Duret-Lutz
8e8c6a8cea org: support org >= 8.3
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Load "shell" instead
of "sh" for recent org-mode version.
2016-12-24 21:08:01 +01:00
Alexandre Duret-Lutz
574f47c366 Release Spot 2.2.2
* NEWS, configure.ac, doc/org/setup.org: Update version.
2016-12-16 06:50:59 +01:00
Alexandre Duret-Lutz
341eeb2ba1 strength: fix is_terminal()
Fix #198.  Reported by Maximilien Colange.

* spot/twaalgos/strength.cc (is_terminal): Test that no accepting
transition lead to a rejecting SCC.
* tests/core/strength.test: Add test case.
* spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org:
Adjust documentation.
* NEWS: Mention the fix.
2016-11-28 18:03:30 +01:00
Alexandre Duret-Lutz
9cf8535578 Release Spot 2.2.1
* NEWS, configure.ac, doc/org/setup.org: Update.
2016-11-21 09:00:51 +01:00
Alexandre Duret-Lutz
dd960dc71c Release Spot 2.2
* configure.ac, doc/org/setup.org, NEWS: Set version number.
2016-11-14 06:02:13 +01:00
Alexandre Duret-Lutz
4bd04fc65c * doc/org/oaut.org: Shorten a long line. 2016-11-13 21:58:37 +01:00
Alexandre Duret-Lutz
e91073a9f1 org: document %r and %R
* doc/org/oaut.org (Timing): New section.
* NEWS: Link to it.
2016-11-13 14:30:12 +01:00
Alexandre Duret-Lutz
c225747749 twa: introduce intersects() and friends
* spot/twa/twa.hh, spot/twa/twa.cc (intersects, intersecting_run,
intersecting_word): New functions.
* NEWS: Mention them.
* doc/org/tut51.org, tests/python/bugdet.py: Use them.
2016-11-13 11:23:12 +01:00
Alexandre Duret-Lutz
b0c60e799a Release Spot 2.1.2
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2016-10-14 17:18:23 +02:00
Alexandre Duret-Lutz
3b5fa22a3b ltlcross: add option --strength and --ambiguous
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.
2016-10-13 15:41:49 +02:00
Alexandre Duret-Lutz
ad502eb324 * doc/org/citing.org: Update references. 2016-10-13 12:04:54 +02:00
Alexandre Duret-Lutz
062643cc88 * doc/org/tut51.org: Typos. 2016-10-12 10:53:03 +02:00
Alexandre Duret-Lutz
a2575e0d3e org: really hide the plantuml logo
Fix a5d6aa2.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Use
-Djava.awt.headless=true, not -Djava.awt.headless.
2016-10-10 15:40:19 +02:00
Alexandre Duret-Lutz
fa80571d44 org: avoid displaying the plantuml log during builds
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Make sure plantuml is
started via "java -Djava.awt.headless".
2016-10-07 15:29:41 +02:00
Alexandre Duret-Lutz
e2b4d38ade more file to ignore
* bin/.gitignore, doc/org/.gitignore: Here.
2016-10-03 16:15:35 +02:00
Alexandre Duret-Lutz
959e757a22 org: cleanup some temporary
* doc/org/concepts.org: Here.
2016-10-03 15:27:09 +02:00
Alexandre Duret-Lutz
fd6614181b Release Spot 2.1.1
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
2016-09-20 08:54:56 +02:00
Alexandre Duret-Lutz
d618495440 * doc/org/citing.org: Add LNCS number. 2016-09-19 21:50:13 +02:00
Alexandre Duret-Lutz
2dfe429447 org: fix an example input
* doc/org/autfilt.org: Remove incorrect acc-name.
2016-08-19 14:30:05 +02:00
Alexandre Duret-Lutz
926ffbf965 bin: %a,%b,%s format specs for LTL output
* NEWS: Mention those.
* bin/common_output.cc, bin/common_output.hh: Implement them.
* bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Update
--help.
* tests/core/format.test: New file.
* tests/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org: Update documentation.
2016-08-15 16:09:53 +02:00
Alexandre Duret-Lutz
78232df3bf Release Spot 2.1
* configure.ac, NEWS, doc/org/setup.org: Update version.
2016-08-08 13:23:18 +02:00
Alexandre Duret-Lutz
ca0d81b5d7 autfilt, dstar2tgba: add CSV input
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.
2016-08-08 13:18:50 +02:00
Alexandre Duret-Lutz
0d753048ce formater: add support for double-quoted fields
Part of #91.

* spot/misc/formater.cc, spot/misc/formater.hh: Here.
* bin/common_output.cc: Adjust automatic output format.
* doc/org/csv.org: Adjust.
* tests/core/lbt.test, tests/core/ltlfilt.test: More tests.
* NEWS: Mention the changes.
2016-08-08 10:53:33 +02:00
Alexandre Duret-Lutz
2b4cf8e7cb org: more typos and small fixups
* doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org,
doc/org/csv.org, doc/org/ltl2tgba.org, doc/org/oaut.org: Here.
* tools/help2man: Adjust regex for optional arguments.
2016-08-06 11:49:53 +02:00
Alexandre Duret-Lutz
ce7b9c5161 org: fix some automata rendering
The new ob-dot.el installed by 15ea2e66e8
makes all the sed escaping useless (and actually harmful).

* doc/org/ltl2tgta.org, doc/org/oaut.org: Fix those.
2016-08-05 20:47:33 +02:00
Alexandre Duret-Lutz
06d5aa5ea2 org: several typos
* doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut04.org, doc/org/tut10.org, doc/org/tut20.org,
doc/org/tut21.org, doc/org/tut50.org: Fix some typos and reword some
sentences.
2016-08-05 11:13:15 +02:00
Alexandre Duret-Lutz
59efe470ca ltlcross: show cross-comparison checks counterexamples
Part of #38.

* bin/ltlcross.cc: Implement it.
* NEWS: Mention it.
* doc/org/ltlcross.org: Adjust example.
* tests/core/ltlcrossce2.test: New test case.
2016-07-29 11:58:12 +02:00
Alexandre Duret-Lutz
fcd6783157 * doc/org/tut50.org: Simplify UML diagrams. 2016-07-27 16:21:37 +02:00
Alexandre Duret-Lutz
15ea2e66e8 org: show how to implement Kripke structures
* doc/org/tut51.org: New file.
* doc/org/tut.org, doc/Makefile.am, NEWS: Add it.
* elisp/ob-dot.el: New file, to work around old org-mode versions.
* elisp/README, elisp/Makefile.am: Add it.
2016-07-27 16:21:03 +02:00
Alexandre Duret-Lutz
da464d8199 org: document explicit vs. on-the-fly
* doc/org/tut50.org: New file.
* doc/org/tut.org: Add it.
* NEWS: Mention it.
* doc/Makefile.am: Add tut50.org, and download plantuml.jar when needed.
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Activate plantum.
* HACKING: Mention the Java dependency.
2016-07-26 11:26:16 +02:00
Alexandre Duret-Lutz
7534f62dba org: add autfilt decoration examples
* doc/org/autfilt.org: Here.
* doc/org/hoa.org: Add a link to it.
* bin/autfilt.cc: Typo.
2016-07-20 11:22:20 +02:00
Alexandre Duret-Lutz
dd6875d5fe bin: overhaul default input selection
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.
2016-07-19 21:55:12 +02:00
Alexandre Duret-Lutz
d1aca565b5 remove the incorrect project_twa_run()
It was bogus, and is better replaced by twa_run::project().

* NEWS, doc/org/upgrade2.org: Mention the removal.
* spot/twaalgos/projrun.cc, spot/twaalgos/projrun.hh: Remove the files.
* spot/twaalgos/Makefile.am: Adjust.
2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
e17a617bc2 hoa: output highlighted states and edges in v1.1
* spot/twaalgos/hoa.cc: Here.
* doc/org/hoa.org, NEWS: Document that.
* tests/core/readsave.test: Test it.
2016-07-18 14:19:08 +02:00
Alexandre Duret-Lutz
bbc3afe1cf org: document named properties
* doc/org/concepts.org: Add a new section.
* doc/org/hoa.org, spot/twa/twa.hh: Link to it.
* NEWS: Mention it.
2016-07-15 18:52:06 +02:00
Alexandre Duret-Lutz
556db2a203 Merge branch 'master' into next 2016-07-11 11:06:05 +02:00
Alexandre Duret-Lutz
2abfd73a30 Release Spot 2.0.3
* NEWS, configure.ac, doc/org/setup.org: Update.
2016-07-11 10:59:23 +02:00
Alexandre Duret-Lutz
ebd4c2dc7a * doc/org/citing.org: Typo. 2016-07-11 10:51:59 +02:00
Alexandre Duret-Lutz
9080a9227f * doc/org/citing.org: Typo. 2016-06-20 13:31:33 +02:00
Alexandre Duret-Lutz
31627eac0b Merge branch 'master' into next 2016-06-17 16:41:48 +02:00