Commit graph

364 commits

Author SHA1 Message Date
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
Alexandre Duret-Lutz
1cce09bc80 Release Spot 2.0.2
* NEWS: Update.
* configure.ac, doc/org/setup.org: Bump version.
2016-06-17 16:33:30 +02:00
Alexandre Duret-Lutz
5f3cc52255 org: add a citing page
With a reference to the "to appear" ATVA'16 paper.

* doc/org/citing.org: New file.
* doc/Makefile.am: Add it.
* doc/org/index.org, doc/org/tools.org: Link to it.
2016-06-17 15:40:11 +02:00
Alexandre Duret-Lutz
b2a306c8d3 python: add the examples from the ATVA'16 paper
* tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb: New
files.
* tests/Makefile.am, doc/org/tut.org: Add them.
2016-06-17 15:40:08 +02:00
Alexandre Duret-Lutz
b439fc674b org: add a citing page
With a reference to the "to appear" ATVA'16 paper.

* doc/org/citing.org: New file.
* doc/Makefile.am: Add it.
* doc/org/index.org, doc/org/tools.org: Link to it.
2016-06-17 15:33:39 +02:00
Alexandre Duret-Lutz
a1260105a4 python: add the examples from the ATVA'16 paper
* tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb: New
files.
* tests/Makefile.am, doc/org/tut.org: Add them.
2016-06-17 14:18:48 +02:00
Alexandre Duret-Lutz
272daf62fc python: add a %%pml magic
Fixes #162.

* python/spot/ltsmin.i: Implement the magic.
* NEWS: Mention it.
* tests/python/ltsmin-pml.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* tests/python/ipnbdoctest.py: Adjust.
2016-06-12 12:53:55 +02:00
Alexandre Duret-Lutz
a7e4395f9d tests: rename ltsmin.ipynb
* tests/python/ltsmin.ipynb: Rename as ...
* tests/python/ltsmin-dve.ipynb: ... this.
* doc/org/tut.org, tests/Makefile.am: Adjust.
2016-06-12 12:28:15 +02:00
Alexandre Duret-Lutz
2cda41e244 * doc/org/tut04.org: Typos. 2016-05-30 16:27:04 +02:00
Alexandre Duret-Lutz
b408827110 add binding for language_containment_checker and document them
* spot/tl/contain.cc, spot/tl/contain.hh: Simplify the
use of language_containment_checker by adding default argument.
* python/spot/__init__.py, python/spot/impl.i: Bind it in Python.
* doc/org/tut04.org: New file to illustrate it.
* doc/org/tut.org, doc/Makefile.am: Add it.
* NEWS: Mention those changes.
2016-05-25 15:12:45 +02:00
Alexandre Duret-Lutz
1c8c86914f * doc/org/tut.org: Typo. 2016-05-25 11:06:19 +02:00
Alexandre Duret-Lutz
69cea65b35 * doc/org/tut.org: Typo. 2016-05-25 11:05:16 +02:00
Alexandre Duret-Lutz
1f9b18f54a org: fix sat-minimize example
Fixes #178.

* doc/org/satmin.org: Use a different example, where tba-det does not
work.  Also adjust the text to automatically adjust to the size of the
produced automata.
2016-05-17 22:18:44 +02:00
Alexandre Duret-Lutz
2d304f3dcf org: fix never claim example
* doc/org/concepts.org: Enlarge the width of the output of pr so that
the output is not truncated.  It add a missing closing brace.
2016-05-17 22:18:43 +02:00
Alexandre Duret-Lutz
d145e566dc org: fix sat-minimize example
Fixes #178.

* doc/org/satmin.org: Use a different example, where tba-det does not
work.  Also adjust the text to automatically adjust to the size of the
produced automata.
2016-05-17 22:01:50 +02:00
Alexandre Duret-Lutz
7c1a94721b org: fix never claim example
* doc/org/concepts.org: Enlarge the width of the output of pr so that
the output is not truncated.  It add a missing closing brace.
2016-05-17 20:57:14 +02:00
Alexandre Duret-Lutz
2bcaff138a * doc/org/ltlcross.org: Fix explanation. 2016-05-11 16:20:12 +02:00
Alexandre Duret-Lutz
c94787b7d9 * doc/org/ltlcross.org: Fix explanation. 2016-05-11 16:19:13 +02:00
Alexandre Duret-Lutz
86287be2ef org: disable postamble in html export
* doc/org/init.el.in, doc/org/.dir-locals.el.in: Here.
2016-05-10 10:48:33 +02:00
Alexandre Duret-Lutz
bb2c697072 org: add a description for each page
Part of #176.

* doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org,
doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genltl.org,
doc/org/hoa.org, doc/org/install.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org,
doc/org/satmin.org, doc/org/tools.org, doc/org/tut.org,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut30.org, doc/org/upgrade2.org: Here.
* doc/org/index.org: Also add keywords in case it is useful, and
use a more descripting title for search engines.
2016-05-10 10:48:33 +02:00
Alexandre Duret-Lutz
d0c5991768 org: disable postamble in html export
* doc/org/init.el.in, doc/org/.dir-locals.el.in: Here.
2016-05-10 10:39:24 +02:00
Alexandre Duret-Lutz
c035ea1822 org: add a description for each page
Part of #176.

* doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org,
doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genltl.org,
doc/org/hoa.org, doc/org/install.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org,
doc/org/satmin.org, doc/org/tools.org, doc/org/tut.org,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut30.org, doc/org/upgrade2.org: Here.
* doc/org/index.org: Also add keywords in case it is useful, and
use a more descripting title for search engines.
2016-05-10 10:23:01 +02:00
Alexandre Duret-Lutz
694e485ec2 Merge branch 'master' into next 2016-05-09 09:46:02 +02:00
Alexandre Duret-Lutz
cfd4a1b98d Release Spot 2.0.1
* NEWS, configure.ac, doc/org/setup.org: Update.
2016-05-09 09:33:24 +02:00
Alexandre Duret-Lutz
b708ab778f genltl: add formulas from three papers
Fixes #166.

* bin/genltl.cc: Add option --dac-patterns, --eh-patterns,
--sb-patterns.
* NEWS, bin/man/genltl.x, doc/org/genltl.org: Document them.
* bench/ltl2tgba/formulae.ltl: Delete.
* bench/ltl2tgba/known: Use genltl instead.
* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README: Update.
* tests/core/ltl2tgba2.test: New test case, using genltl.
* tests/Makefile.am: Add it.
2016-05-05 18:39:13 +02:00
Alexandre Duret-Lutz
9149724617 doc: add a spot(7) man page
Suggested by Akim Demaille.  Fixes #171.

* bin/man/spot.x, bin/spot.cc: New files.
* bin/man/Makefile.am, bin/Makefile.am: Add them.
* doc/org/tools.org, NEWS: Mention the new page.
2016-05-02 14:40:45 +02:00
Alexandre Duret-Lutz
d6e491a761 doc: fix css to not highlight table row in man pages
* doc/org/spot.css: Here.
2016-05-02 14:40:45 +02:00
Alexandre Duret-Lutz
5e6d096e0f * doc/org/tools.org: Minor tweaks. 2016-05-02 14:40:45 +02:00
Alexandre Duret-Lutz
d02ee34e10 doc: add a spot(7) man page
Suggested by Akim Demaille.  Fixes #171.

* bin/man/spot.x, bin/spot.cc: New files.
* bin/man/Makefile.am, bin/Makefile.am: Add them.
* doc/org/tools.org, NEWS: Mention the new page.
2016-05-02 10:41:41 +02:00
Alexandre Duret-Lutz
923f4b6277 doc: fix css to not highlight table row in man pages
* doc/org/spot.css: Here.
2016-05-02 10:12:32 +02:00
Alexandre Duret-Lutz
48e6ef7065 * doc/org/tools.org: Minor tweaks. 2016-05-02 10:06:29 +02:00
Alexandre Duret-Lutz
d9174593c8 common_trans: allow rewriting operators
Part of #168.

* spot/misc/formater.cc: Adjust to support bracketed options.
* bin/common_trans.hh, bin/common_trans.cc: Use that to
support rewriting operators.
* doc/org/ltlcross.org, tests/core/ltldo.test: Add some examples.
* NEWS: Mention it.
2016-05-01 21:05:49 +02:00