Commit graph

4833 commits

Author SHA1 Message Date
Alexandre GBAGUIDI AISSE
ebe3a15dcc remfin: add is_buchi_realizable() method
* NEWS: Update.
* spot/tl/hierarchy.cc: Replace rabin_to_buchi_maybe() with
is_buchi_realizable().
* spot/twaalgos/remfin.cc: Implement it.
* spot/twaalgos/remfin.hh: Declare it.
2018-01-19 02:09:28 +01:00
Alexandre GBAGUIDI AISSE
1b4002401a spot: small factorisations, improvements and typos
* spot/tl/hierarchy.cc: Factorisations, improvements.
* spot/twaalgos/totgba.cc:  Typos.
2018-01-19 02:07:00 +01:00
Alexandre GBAGUIDI AISSE
2c059a1099 sccinfo: Fix bug in states_on_acc_cycle_of_rec()
* spot/twaalgos/sccinfo.cc: Here.
2018-01-19 02:07:00 +01:00
Alexandre Duret-Lutz
1a0fa3b722 more doxygen
This introduce some section for acceptance transformation, and add
more comments in a few places.

* spot/taalgos/emptinessta.hh, spot/twa/twa.hh, spot/twa/twagraph.hh,
spot/twaalgos/bfssteps.hh, spot/twaalgos/cleanacc.hh,
spot/twaalgos/degen.hh, spot/twaalgos/dualize.hh,
spot/twaalgos/parity.hh, spot/twaalgos/rabin2parity.hh,
spot/twaalgos/remfin.hh, spot/twaalgos/sccinfo.hh,
spot/twaalgos/sepsets.hh, spot/twaalgos/split.hh,
spot/twaalgos/totgba.hh: More doxygen.
* spot/twa/twagraph.cc: Typos in comments.
2018-01-18 18:00:11 +01:00
Maximilien Colange
7e02aae366 Rabin to parity translation
* spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
  implement it
* spot/twaalgos/postproc.cc: use it
* spot/twaalgos/Makefile.am: build the new files
* NEWS: document the new function
* python/spot/impl.i: Python bindings for the new function
* tests/Makefile.am, tests/core/rabin2parity.test: test the new function
2018-01-16 16:23:10 +01:00
Maximilien Colange
7bf68b4c0e Typos and duplicates
* spot/twaalgos/degen.cc: typo in an error message
* NEWS: fix typos and remove duplicates
2018-01-16 09:43:35 +01:00
Alexandre Duret-Lutz
d94fb07168 twaalgos: more doxygen comments
* spot/twaalgos/product.hh, spot/twaalgos/remfin.hh,
spot/twaalgos/sum.hh, spot/twaalgos/totgba.hh: Improve documentation.
2018-01-16 08:12:28 +01:00
Alexandre Duret-Lutz
c920825fad work around issue #317
* spot/twaalgos/cobuchi.cc: Call sbacc() on transition-based input.
* tests/Makefile.am: Remove XFAIL_TESTS.
* NEWS: Adjust.
2018-01-14 22:18:55 +01:00
Alexandre Duret-Lutz
61b0a542f1 postproc: add support for co-Büchi output
* spot/twaalgos/cobuchi.cc, spot/twaalgos/cobuchi.hh (to_nca): New
function.
(weak_to_cobuchi): New internal function, used in to_nca and to_dca
when appropriate.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement
the CoBuchi option.
* python/spot/__init__.py: Support it in Python.
* bin/common_post.cc: Add support for --buchi.
* bin/autfilt.cc: Remove the --dca option.
* tests/core/dca.test, tests/python/automata.ipynb: Adjust and add
more tests.  In particular, add more complex persistence and
recurrence formulas to the list of dca.test.
* tests/python/dca.test: Adjust and rename to...
* tests/core/dca2.test: ... this.  Add more tests, to the point
that this is now failing, as described in issue #317.
* tests/python/dca.py: Remove.
* tests/Makefile.am: Adjust.
2018-01-14 22:16:40 +01:00
Alexandre Duret-Lutz
9464043d39 fix streett_to_generalized_buchi
Fixes #316.

* spot/twaalgos/totgba.cc: Fix confusing definition of scc_inf_wo_fin.
* tests/python/streett_totgba2.py: New test case.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
2018-01-14 16:08:40 +01:00
Alexandre Duret-Lutz
8a74ae6c9d misc: fix some down_cast issues
We had new failure on MinGW with GCC believing that some pointer
returned by down_cast could be NULL; and the down_cast function was in
the global namespace.

* spot/misc/casts.hh: Rewrite.
* NEWS: Mention the small issues.
* tests/core/ikwiad.cc, tests/core/ngraph.cc: Adjust to use
spot::down_cast instead of down_cast.
2018-01-10 21:35:46 +01:00
Alexandre Duret-Lutz
91fdc5ecb2 ltsmin: rework the dlsym interface to please GCC snapshot
* spot/ltsmin/ltsmin.cc: Avoid C-style function casts with
incompatible types.
2018-01-09 22:00:49 +01:00
Alexandre Duret-Lutz
31387e8f71 mark custom hash functions as noexcept
* spot/misc/bitvect.cc, spot/misc/bitvect.hh, spot/misc/hash.hh,
spot/twa/acc.hh, spot/twaalgos/cobuchi.cc, spot/twaalgos/degen.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/parity.cc,
spot/twaalgos/powerset.cc, spot/twaalgos/product.cc,
spot/twaalgos/stutter.cc, spot/twaalgos/totgba.cc,
spot/twaalgos/toweak.cc: Mark hash function as noexcept to please GCC
snapshot.
2018-01-09 21:23:11 +01:00
Alexandre Duret-Lutz
7f5c1d3707 * NEWS: Reorganize, in preparation for the 2.5 release. 2018-01-09 16:55:55 +01:00
Alexandre Duret-Lutz
57d5969079 fix some bibliographic references
* spot/twaalgos/cobuchi.hh, spot/twaalgos/totgba.hh: Here.
2018-01-09 16:46:44 +01:00
Alexandre Duret-Lutz
0b71df3fd3 genltl: add --gf-implies
* spot/gen/formulas.cc, spot/gen/formulas.hh: Implement
LTL_GF_IMPLIES.
* bin/genltl.cc: Add --gf-implies.
* NEWS: Mention it.
* tests/core/genltl.test: Use it.
2018-01-09 10:59:10 +01:00
Alexandre Duret-Lutz
f369db6cb1 python: add colored parity support to postproc and translate
* python/spot/impl.i: Bind is_colored().
* python/spot/__init__.py: Add Colored support to postproc.
* tests/python/parity.py: Add a test case.
2018-01-08 11:37:22 +01:00
Alexandre Duret-Lutz
abe4e12cc9 * spot/twaalgos/parity.hh: Fix typo in comment. 2018-01-08 11:35:59 +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
58e64e752c python: upgrade notebook format to v4
Fixes #311.

* tests/python/ipnbdoctest.py: Adjust to process the new format,
with a lot of inspiration from Vcsn's copy of this file.
* tests/python/_altscc.ipynb, tests/python/_aux.ipynb,
tests/python/acc_cond.ipynb, tests/python/accparse.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
tests/python/atva16-fig2b.ipynb, tests/python/automata-io.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/formulas.ipynb, tests/python/gen.ipynb,
tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb,
tests/python/ltsmin-pml.ipynb, tests/python/parity.ipynb,
tests/python/piperead.ipynb, tests/python/product.ipynb,
tests/python/randaut.ipynb, tests/python/randltl.ipynb,
tests/python/stutter-inv.ipynb, tests/python/testingaut.ipynb,
tests/python/word.ipynb: Upgrade to the new format.
* NEWS: Mention the change.
2018-01-07 12:59:59 +01:00
Alexandre Duret-Lutz
020c981188 ltlcross: detect remove_fin failures
Fixes #314, reported by František Blahoudek.

* bin/ltlcross.cc: Here.
* tests/core/ltlcross3.test: Add new test case.
* NEWS: Mention the bug.
2018-01-06 14:08:44 +01:00
Alexandre Duret-Lutz
a924bc561a remove_fin: use simplify_acceptance
* spot/twaalgos/remfin.cc: Simplify acceptance before trying the
different strategies.
* spot/twaalgos/cleanacc.cc: Skip simplify_complementary_marks_here()
on generalized Büchi.
* tests/core/remfin.test, tests/python/tra2tba.py: Adjust.
* spot/twaalgos/totgba.cc: Simplify the result of Streett->GBA.
* NEWS: Adjust.
2018-01-06 12:48:46 +01:00
Alexandre Duret-Lutz
2feba6ad5e simplify_acceptance: fix handling of first edge
Fixes #315.

* spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Do not
compare the first edge against previous_a.
* tests/core/accsimpl.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
2018-01-06 09:21:23 +01:00
Alexandre Duret-Lutz
17b295e10f python: SVG display of word as signals
Fixes #309.

* python/spot/__init__.py (twa_word.as_svg, twa_word.show): New
  methods.
* tests/python/word.ipynb: Use them.
* NEWS: Mention them.
2018-01-04 18:43:12 +01:00
Alexandre Duret-Lutz
678446f1d6 bump copyright year
* bin/common_setup.cc, debian/copyright: Here.
2018-01-02 20:34:38 +01:00
Alexandre Duret-Lutz
0aca26e3f9 parity: fix error handling
* spot/twaalgos/parity.cc: Do not throw a pointer to an exception,
throw the exception directly.  Factor all the throwing code in a
function.
* tests/python/parity.py: Add test case.
2018-01-02 17:45:33 +01:00
Alexandre Duret-Lutz
288ea95658 postproc: add Python bindings for Parity changes
* python/spot/__init__.py: Here.
* tests/python/parity.py: New file.
* tests/Makefile.am: Add it.
2018-01-02 17:45:33 +01:00
Alexandre Duret-Lutz
42ebf8b18c postproc: introduce --parity output
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add parity
  options.
* bin/common_post.cc: Add support for --parity.
* NEWS: Mention it.
* tests/core/parity2.test: New file.
* tests/Makefile.am: Add it.
2018-01-02 12:07:26 +01:00
Alexandre Duret-Lutz
412c2059bf man: obsolete paragraph in ltlcross doc
Reported by František Blahoudek.

* bin/man/ltlcross.x: Remove obsolete paragraph with reference to
columns in_states, in_edges, in_transitions, and in_acc that
were removed in 1.99.3.
2017-12-28 20:36:52 +01:00
Alexandre Duret-Lutz
0d963d5f7e Merge branch 'master' into next 2017-12-25 15:48:09 +01:00
Alexandre Duret-Lutz
9c77cb321e * NEWS, configure.ac: Bump version to 2.4.4.dev. 2017-12-25 15:46:44 +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
915d2f4659 sbacc: more fixes related to #312
The issue also exists with determinism.

* tests/core/sbacc.test: New test case.
* spot/twaalgos/sbacc.cc: Fix it.
* NEWS: Update.
2017-12-25 15:38:55 +01:00
Alexandre Duret-Lutz
18e65f3bc8 sbacc: fix sbacc producing complete automata marked as incomplete
Fixes #312, reported by František Blahoudek.

* spot/twaalgos/sbacc.cc: Detect the case were this can happen,
and fix it.
* tests/core/sbacc.test: New test case.
* NEWS: Mention the bug.
2017-12-25 15:38:47 +01:00
Alexandre Duret-Lutz
396024143c to_tgba: fix handling of CNF with multiple unit clauses
Fixes #313, reported by František Blahoudek.

* spot/twaalgos/totgba.cc (to_generalized_buchi): Fix it.
* tests/core/remfin.test: Test it.
* NEWS: Mention it.
2017-12-25 15:38:28 +01:00
Alexandre Duret-Lutz
ec393708bb sbacc: more fixes related to #312
The issue also exists with determinism.

* tests/core/sbacc.test: New test case.
* spot/twaalgos/sbacc.cc: Fix it.
* NEWS: Update.
2017-12-24 20:44:15 +01:00
Alexandre Duret-Lutz
5467fa1622 * spot/twaalgos/stutter.cc (highlight_vector): Replace existing colors. 2017-12-23 09:58:41 +01:00
Alexandre Duret-Lutz
8579bedfaf python: highlighting with vector of bools
* python/spot/__init__.py: Deal with vectors of bools.
* tests/python/highlighting.ipynb: Test this.
2017-12-23 09:58:41 +01:00
Alexandre Duret-Lutz
95fd75940a sbacc: fix sbacc producing complete automata marked as incomplete
Fixes #312, reported by František Blahoudek.

* spot/twaalgos/sbacc.cc: Detect the case were this can happen,
and fix it.
* tests/core/sbacc.test: New test case.
* NEWS: Mention the bug.
2017-12-22 18:27:07 +01:00
Alexandre Duret-Lutz
9ec7df670e to_tgba: fix handling of CNF with multiple unit clauses
Fixes #313, reported by František Blahoudek.

* spot/twaalgos/totgba.cc (to_generalized_buchi): Fix it.
* tests/core/remfin.test: Test it.
* NEWS: Mention it.
2017-12-22 17:53:30 +01:00
Alexandre Duret-Lutz
19348c8938 python: give access to the "product-states" property
* python/spot/impl.i (get_product_states, set_product_states): New.
* tests/python/product.ipynb: Use it.
* NEWS: Mention it.
2017-12-22 17:27:26 +01:00
Alexandre Duret-Lutz
904cfb27fa scc_info: detect incorrect initial state
* spot/twaalgos/sccinfo.cc: Here.
* tests/python/sccinfo.py: Test it.
2017-12-22 17:23:10 +01:00
Alexandre Duret-Lutz
31ccab026b python: allow spot.formula(spot.formula(...))
* python/spot/__init__.py: Recognize if the input is already a
formula.
* tests/python/formulas.ipynb: Test this.
2017-12-22 17:18:36 +01:00
Alexandre Duret-Lutz
3b4335d243 stutter: two new functions
* spot/twaalgos/stutter.hh, spot/twaalgos/stutter.cc: Introduce
is_stutter_invariant_forward_closed and
make_stutter_invariant_forward_closed_inplace.
* tests/python/stutter-inv.ipynb: Use them.
2017-12-19 21:03:35 +01:00
Alexandre Duret-Lutz
8d5f2ca917 * tests/python/ipnbdoctest.py: Work around different pandas versions. 2017-12-19 21:03:35 +01:00
Alexandre Duret-Lutz
7f97c90470 Merge branch 'master' into next 2017-12-19 10:40:50 +01:00
Alexandre Duret-Lutz
696d81f651 Bump version number
* configure.ac, NEWS: Update to 2.4.3.dev.
2017-12-19 10:40:07 +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
ac80b07d93 introduce check_determinism()
* spot/twaalgos/isdet.hh, spot/twaalgos/isdet.cc (check_determinism):
New function.
* NEWS: Mention it.
* tests/python/semidet.py: New file.
* tests/Makefile.am: Add it.
2017-12-18 15:57:17 +01:00