Commit graph

627 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
f3a0ede9f3 Release Spot 2.5
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2018-01-20 15:09:00 +01:00
Florian Perlié-Long
206b1ee287 * doc/tl/tl.tex: Typos 2018-01-19 08:17:44 +01:00
Alexandre Duret-Lutz
bd6dc7a806 postproc: add support for colored-parity
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Add support
for a colored option.
* bin/common_post.cc, bin/common_post.hh bin/autfilt.cc,
bin/ltl2tgba.cc, bin/dstar2tgba.cc: Add support for --colored-parity.
* bin/ltldo.cc: Adjust as well for consistency, even if --parity and
--colored-parity is not used here.
* tests/core/parity2.test: Add tests.
* doc/org/autfilt.org, doc/org/ltl2tgba.org: Add examples.
* NEWS: Mention --colored-parity.
2018-01-08 11:35:49 +01:00
Alexandre Duret-Lutz
6bad8aebdd python: remove error recovery checks from the public notebooks
* tests/python/_autparserr.ipynb: New files, containing error
checking code from automata-io.ipynb and piperead.ipynb.
* tests/python/automata-io.ipynb: Remove error checks, and pipe
examples from piperead.ipynb.
* tests/python/piperead.ipynb: Delete.
* tests/python/word.ipynb: Move error checking code...
* tests/python/_word.ipynb: ... in this new file.
* doc/org/tut.org, tests/Makefile.am: Adjust.
2018-01-07 16:22:46 +01:00
Alexandre Duret-Lutz
0d963d5f7e Merge branch 'master' into next 2017-12-25 15:48:09 +01:00
Alexandre Duret-Lutz
2f5fb47c7f Release Spot 2.4.4
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2017-12-25 15:42:03 +01:00
Alexandre Duret-Lutz
7f97c90470 Merge branch 'master' into next 2017-12-19 10:40:50 +01:00
Alexandre Duret-Lutz
325d3f921f Release Spot 2.4.3
* NEWS, configure.ac, doc/org/setup.org: Update.
2017-12-19 10:13:07 +01:00
Alexandre Duret-Lutz
7500962c3d org: fix URL to last successful build
* doc/org/install.org: Here.
2017-12-14 09:55:38 +01:00
Alexandre Duret-Lutz
49b76bcf66 doxygen doc: minor improvements
* doc/footer.html: Make the footer XML compatible.
* doc/mainpage.dox: Fix references to modules.
* spot/tl/formula.hh: Introduce a hierarchy module.
* spot/tl/hierarchy.hh: Use it.
2017-12-08 22:07:11 +01:00
Alexandre Duret-Lutz
f56e1e8a6c org: fix URL to last successful build
* doc/org/install.org: Here.
2017-11-28 18:22:32 +01:00
Alexandre Duret-Lutz
7b2517a518 formula: accept additional arguments for map and traverse
Fixes #306.

* spot/tl/formula.hh, python/spot/__init__.py: Implement this
in C++ and Python.
* doc/org/tut03.org: Document (and indirectly test) it.
* NEWS: Mention it.
2017-11-23 23:04:15 +01:00
Alexandre Duret-Lutz
7dd791fe59 * doc/Makefile.am (DISTCLEANFILES): Avoid multiple definitions. 2017-11-23 23:03:09 +01:00
Maximilien Colange
1da0afbafe Improve ltlsynt interface
To ease debugging and testing, ltlsynt can output the synthesized
strategy as an automaton, not just an aiger circuit.
Also, its exit code has been changed to something meaningful.

* bin/ltlsynt.cc: Various improvements: options, exit code, code style
* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc,
  spot/twaalgos/Makefile.am: Move the aiger printer to separate files
* tests/core/ltlsynt.test: Clean up and update test file
* tests/Makefile.am: Add the test file to the test suite
* NEWS: document the new aiger printer
* doc/org/concepts.org: document the named property "synthesis-outputs",
  used by print_aiger
2017-11-23 14:46:50 +01:00
Alexandre Duret-Lutz
5504e2255a do not run optipng anymore
* doc/Makefile.am (dist-hook): Remove.
* HACKING: Adjust.
2017-11-23 13:40:05 +01:00
Alexandre Duret-Lutz
246b5d8fed doc: implement --enable-doxygen and do not distribute the doc
Fixes #299.

* configure.ac, doc/Makefile.am: Adjust.
* NEWS, HACKING, README: Document the change.
* doc/dot.in: Delete, not used anymore.
* doc/Doxyfile.in: Adjust to not look for dot.
* debian/rules: Use --enable-doxygen.
2017-11-22 16:06:04 +01:00
Alexandre Duret-Lutz
61602a3bba org: convert all images to svg
Suggested in #299.

* doc/org/autfilt.org, doc/org/concepts.org, doc/org/dstar2tgba.org,
doc/org/genaut.org, doc/org/hierarchy.org, doc/org/hoa.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org,
doc/org/tut11.org, doc/org/tut23.org, doc/org/tut24.org,
doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org,
doc/org/tut51.org: Adjust all dot outputs to produce svg.
* doc/org/arch.tex, doc/org/hierarchy.tex, doc/org/satmin.tex: Adjust
to produce a pdf with 12pt text.
* doc/Makefile.am: Adjust the generation of arch.svg, hierarchy.svg,
and satmin.svg: From above.
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Adjust dot arguments
to produce svg with 12pt text (the default was 14pt).
* doc/org/spot.css: Use Lato as the main font for consistency with
automata.
* HACKING: pdf2svg is now required to build the doc.
2017-11-22 12:03:53 +01:00
Alexandre Duret-Lutz
454cc73670 doc: use SVG in the doxygen manual
Suggested in #299.

* doc/Doxyfile.in: Here.
2017-11-22 12:03:52 +01:00
Alexandre Duret-Lutz
b20687630b org: ltl3hoa -> ltl3tela
Fixes #296.

* doc/org/ltlcross.org: Here.
2017-11-07 17:15:13 +01:00
Alexandre Duret-Lutz
010b418583 Merge branch 'master' into next 2017-11-07 07:48:53 +01:00
Alexandre Duret-Lutz
ed5463cf6f Release Spot 2.4.2
* NEWS, configure.ac, doc/org/setup.org: Update.
2017-11-07 07:44:27 +01:00
Alexandre Duret-Lutz
75a1d6ac61 bin: add %g options to print acceptance name
Fixes #289.

* spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
bin/common_aoutput.cc, bin/common_aoutput.hh: plug %g and %G into
acc_cond::name() when arguments are given as %[arg]g.  or %[arg]G.
* tests/core/acc2.test: Add test case.
* doc/org/randaut.org, NEWS: Document it.
2017-11-04 07:43:41 +01:00
Alexandre Duret-Lutz
6459877a1a overhaul the stutter-invariance checks
* spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Cleanup and
document the api.
* spot/twa/twa.hh, doc/mainpage.dox: Add a stutter-invariant section.
* tests/python/stutter-inv-states.ipynb: Rename as ...
* tests/python/stutter-inv.ipynb: ... this, and add more comments.
* tests/Makefile.am, doc/org/tut.org: Adjust renaming.
* bench/stutter/stutter_invariance_randomgraph.cc,
bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/Makefile.am: Make it compile again.
* bin/autfilt.cc: Call inplace variants.
* NEWS: Mention the overhaul.
2017-11-01 10:35:11 +01:00
Alexandre Duret-Lutz
7510743b47 org: update for gpg-signed Debian repository
* doc/org/install.org: Mention the GPG key.
2017-10-23 17:59:57 +02:00
Alexandre Duret-Lutz
2222661f98 org: update for gpg-signed Debian repository
* doc/org/install.org: Mention the GPG key.
2017-10-23 17:58:32 +02:00
Alexandre Duret-Lutz
d597c58106 org: improve wording
* doc/org/tut04.org: This tests equivalence, not equality.
2017-10-19 18:45:55 +02:00
Alexandre Duret-Lutz
bdfa2b3983 org: improve wording
* doc/org/tut04.org: This tests equivalence, not equality.
2017-10-19 18:44:37 +02:00
Alexandre Duret-Lutz
1a0dcf4f69 document the recent changes to implication rules
* doc/tl/tl.tex: This adds the rules implemented in 0a2bca137
for #293.
2017-10-18 14:53:29 +02:00
Alexandre Duret-Lutz
427c696954 org: fix the example for ltlcross --verbose
* doc/org/ltlcross.org: Use SPOT_HOA_TOLERANT=1 to work around a bug
in ltl3ba -H1.
2017-10-18 14:52:30 +02:00
Alexandre Duret-Lutz
308415f88a document the recent changes to implication rules
* doc/tl/tl.tex: This adds the rules implemented in 0a2bca137
for #293.
2017-10-17 17:58:59 +02:00
Alexandre Duret-Lutz
fcccd5f425 ltlcross: add support for --reference translators
Suggested by Tobias Meggendorfer.  Fixes #295.

* bin/ltlcross.cc, bin/common_trans.hh, bin/common_trans.cc: Implement
this --reference option.
* NEWS, doc/org/ltlcross.org: Document it.
* tests/core/ltlcross3.test: Test it.
2017-10-15 19:35:28 +02:00
Alexandre Duret-Lutz
77c0e76258 org: fix the example for ltlcross --verbose
* doc/org/ltlcross.org: Use SPOT_HOA_TOLERANT=1 to work around a bug
in ltl3ba -H1.
2017-10-15 18:48:00 +02:00
Alexandre Duret-Lutz
183ec1fb4e ltlcross, autcross, ltldo: support --fail-on-timeout
Suggested by Tobias Meggendorfer.  Fixes #294.

* bin/autcross.cc, bin/ltlcross.cc, bin/ltldo.cc: Add the option.
* tests/core/autcross3.test, tests/core/ltlcross3.test,
tests/core/ltldo.test: Test it.
* tests/Makefile.am: Add autcross3.test.
* NEWS, doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
Mention the option.
* THANKS: Add Tobias.
2017-10-15 12:22:15 +02:00
Alexandre Duret-Lutz
9b18729721 stutter: detect stutter-invariance at the state level
* spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Implement
stutter-invariance detection at the state level.
* python/spot/impl.i: Instantiate std::vector<bool>
* tests/python/stutter-inv-states.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
2017-10-11 15:01:29 +02:00
Alexandre Duret-Lutz
584430803d Merge branch 'master' into next 2017-10-05 16:00:07 +02:00
Alexandre Duret-Lutz
5c22db3c73 Release Spot 2.4.1
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2017-10-05 15:52:57 +02:00
Alexandre Duret-Lutz
d2c4e596d1 org: fix the dot2tex example
* doc/org/oaut.org: Fix the call to convert.
2017-10-05 15:52:57 +02:00
Florian Perlié-Long
89c312cb57 * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos 2017-10-03 16:48:00 +02:00
Florian Perlié-Long
0f023bd0fe * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos 2017-10-03 15:54:48 +02:00
Thibaud Michaud
d6ae7af5f5 ltlsynt: translate winning strategy to AIGER
* bin/ltlsynt.cc: Here.
* doc/org/ltlsynt.org: Document it.
* tests/core/ltlsynt.test: Test it.
2017-09-25 12:23:47 +02:00
Thibaud Michaud
f414e9f5f2 parity game: add Zielonka's recursive algorithm
* spot/misc/game.cc, spot/misc/game.hh: Implement it.
* bin/ltlsynt.cc: Use it.
* doc/org/ltlsynt.org: Document it.
2017-09-25 12:23:47 +02:00
Thibaud Michaud
0821c97eb8 add ltlsynt executable
For now, ltlsynt only handles LTL realizability. It uses a reduction to
parity game followed by Calude et al.'s reduction from parity game to
reachability game.

* bin/ltlsynt.cc, bin/Makefile.am, bin/man/ltlsynt.x,
bin/man/Makefile.am, bin/.gitignore: New binary.
* doc/org/arch.tex, doc/Makefile.am, doc/org/tools.org,
doc/org/ltlsynt.org: Document it.
* spot/misc/game.cc, spot/misc/game.hh, spot/misc/Makefile.am: Parity
game wrapper for parity automata + reachability game interface from
Calude et al.'s paper.
2017-09-25 12:23:47 +02:00
Laurent XU
27982fb80f parity: add spot::change_parity()
This function changes the parity acceptance of an automaton.

* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
* python/spot/impl.i: Add spot/twaalgos/parity.hh
* spot/twaalgos/Makefile.am: Add spot/twaalgos/parity.{cc,hh}
* tests/core/parity.cc, tests/core/parity.test: Add
spot::change_parity() tests
* tests/python/parity.ipynb: Add documentation about
spot::change_parity()
* tests/Makefile.am: Add tests/core/parity.{cc,hh} and
tests/python/parity.ipynb
* doc/org/tut.org: Add the html page of tests/python/parity.ipynb
2017-09-25 12:10:14 +02:00
Alexandre Duret-Lutz
1941bac22c org: improve dot2tex conversion to png
* doc/org/oaut.org: Here.
2017-09-06 11:18:34 +02:00
Alexandre Duret-Lutz
80621557b2 Release Spot 2.4
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2017-09-05 21:08:48 +02:00
Alexandre Duret-Lutz
bc626788af dot: make 'x' compatible with 'b'/'r'/'R'
* spot/twaalgos/dot.cc: Implement.
* doc/org/oaut.org: Illustrate.
* tests/core/dot2tex.test: Add some limited tests.
2017-09-05 07:45:11 +02:00
Alexandre Duret-Lutz
290d7b56fb * doc/org/oaut.org: Missing word. 2017-09-04 19:57:40 +02:00
Alexandre Duret-Lutz
f726152ebd org: fix one example
* doc/org/genaut.org: Output the result for the last example.
2017-09-04 17:23:07 +02:00
Alexandre Duret-Lutz
e7df182a30 gen: rename KS_COBUCHI to KS_NCA for consistency
* spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Rename
the enum, function, and command-line option.
* tests/core/genaut.test, tests/python/gen.ipynb, tests/python/gen.py:
Adjust test cases.
* doc/org/genaut.org: Adjust doc.
2017-09-03 15:47:27 +02:00
Alexandre Duret-Lutz
e8527d5ae9 Improve simplification of expr[*0..1]
Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
2017-09-02 16:35:18 +02:00