Commit graph

5111 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
188d210521 python: suggest installing GraphViz when dot is not found
This fixes an issue mentioned in #375.

* python/spot/aux.py (str_to_svg): Catch a missing 'dot' and instruct
the user to install GraphViz.
* THANKS: Add reporter.
2019-01-25 23:16:46 +01:00
Alexandre Duret-Lutz
573c593fa2 powerset: some clean up
* spot/twaalgos/powerset.cc: Remove some unnecessary code, as spotted
by Fanda.  Also fix some comments.
2019-01-23 11:32:00 +01:00
Alexandre Duret-Lutz
ff960ee313 * THANKS: Add the reporter of #372. 2019-01-23 11:05:36 +01:00
Alexandre Duret-Lutz
476a874c71 org: work around issue with Org 9.2
See the following email
http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html

* doc/org/tut24.org, doc/org/tut51.org: Export the output of
noweb-based block without ':export results' or ':export both'.
* doc/org/spot.css: Add style for src-text.
2019-01-16 18:06:04 +01:00
Alexandre Duret-Lutz
3908cc1bca python: improve bdd_dict bindings
Fixes #372.

* python/spot/impl.i: Refactor the handling of exceptions using a
Lippincott function.  Map out_of_range to IndexError.  Add
PyObject* version for bdd_dict's register and unregister functions
so we can use Python objects as well.
* tests/python/bdddict.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the changes.
2019-01-14 16:42:30 +01:00
Alexandre Duret-Lutz
bd0f959418 Bump copyright year
* bin/common_setup.cc, debian/copyright: Here.
2019-01-07 11:30:18 +01:00
Alexandre Duret-Lutz
365fde8364 org: typo
* doc/org/concepts.org: Typo reported by Paul Guénézan.
* THANKS: Add him.
2019-01-07 11:26:45 +01:00
Alexandre Duret-Lutz
98c8725d0c print_dot_psl: fix numbering of commutative operands
* spot/tl/dot.cc: Here.
* tests/python/formulas.ipynb: Add test case.
* NEWS: Mention the bug.
2018-12-17 17:09:56 +01:00
Alexandre Duret-Lutz
dc1f713391 * tests/python/stutter-inv.ipynb: Add link to on-line translator. 2018-12-13 11:22:35 +01:00
Alexandre Duret-Lutz
d67053a2da * NEWS: Typo. 2018-12-13 11:17:04 +01:00
Alexandre Duret-Lutz
db02a0b270 * NEWS, configure.ac: Bump version number. 2018-12-11 09:07:11 +01:00
Alexandre Duret-Lutz
68da48484b Release Spot 2.7
* configure.ac, NEWS, doc/org/setup.org: Bump version.
2018-12-11 09:00:52 +01:00
Alexandre Duret-Lutz
77f3ba9478 translate: fix stutter-invariant flag on leading Xs
Issue discovered by Mikuláš Klokočka and reported by František
Blahoudek.

* spot/twaalgos/translate.cc: Reset the stutter-invariant flag
when adding extra transitions for leading Xs.
* tests/core/stutter-tgba.test: New test case.
* NEWS: Mention the bug.
2018-12-07 15:53:54 +01:00
Alexandre Duret-Lutz
560c6f2d48 * spot/twa/acc.hh: More documentation. 2018-12-07 11:29:33 +01:00
Alexandre Duret-Lutz
c20f49aeac * NEWS: Add a missing entry. 2018-12-05 10:05:58 +01:00
Etienne Renault
dba2305367 gitlab-ci: force distcheck to use included GNU ltdl
* .gitlab-ci.yml: Here.
2018-12-04 14:42:02 +00:00
Etienne Renault
9038e48ea4 gitlab-ci: use the included GNU ltdl sources
* .gitlab-ci.yml: Here.
2018-12-03 14:52:13 +00:00
Etienne Renault
c2c8d21538 noexcept: please gcc snapshot
* bin/common_finput.hh,
bin/common_trans.cc,
bin/common_trans.hh,
spot/misc/minato.hh,
spot/ta/ta.cc,
spot/ta/ta.hh,
spot/twa/acc.hh,
spot/twaalgos/cycles.hh,
spot/twaalgos/emptiness.hh,
spot/twaalgos/gtec/gtec.hh,
spot/twaalgos/ndfs_result.hxx,
spot/twaalgos/sccinfo.hh,
spot/twaalgos/word.cc,
spot/twaalgos/word.hh: Here.
2018-11-29 10:16:01 +00:00
Alexandre Duret-Lutz
b8164ef979 add an Alpine Linux build
* .gitlab-ci.yml (alpine-gcc): Here.
2018-11-10 22:15:59 +01:00
Alexandre Duret-Lutz
3b830ec0aa fix rpm builds
* spot.spec.in: Do not hardcode the Python version.
2018-11-10 22:11:51 +01:00
Alexandre Duret-Lutz
6cfdf02c5a Fix Alpine Linux builds
Reported by Maxime Bouton.

* spot/misc/tmpfile.cc: Include stdlib.h, not cstdlib, so
that our replacement secure_getenv() is found.
* THANKS: Add Maxime.
2018-11-10 12:48:11 +01:00
Alexandre Duret-Lutz
fd32ab5dd7 fix is_generalized_rabin and is_generalized_streett
* spot/twa/acc.cc: Recoginize the single-pair case.
* python/spot/impl.i: Return the vector instead of taking it
by reference.
* tests/python/setacc.py: Add test cases.
* NEWS: Mention those changes.
2018-11-08 11:35:15 +01:00
Alexandre Duret-Lutz
29e08a1afb introduce count_univbranch_states() and count_univbranch_edges()
Fixes #368, suggested by František Blahoudek.

* spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh
(count_univbranch_states(), count_univbranch_edges()): New functions.
* bin/common_aoutput.cc, bin/common_aoutput.hh: Add %u and variants.
* NEWS: Mention these.
* tests/core/alternating.test: Test them.
2018-11-08 10:33:49 +01:00
Alexandre Duret-Lutz
60296317c7 python: more conventional __repr__ for several types
* NEWS: Mention the change.
* python/spot/__init__.py: Add _repr_latex_ for twa_word, and
remove __repr__ and __str__ for atomic_prop_set.
* python/spot/impl.i: Implement __repr__ and __str__ for
atomic_prop_set.  Fix __repr__ for trival, acc_code, acc_cond,
mark_t.  Remove __repr__ for twa_run and twa_word.
* tests/python/acc_cond.ipynb, tests/python/accparse.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/bdditer.py, tests/python/contains.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltlsimple.py, tests/python/ltsmin-dve.ipynb,
tests/python/product.ipynb, tests/python/relabel.py,
tests/python/satmin.ipynb tests/python/stutter-inv.ipynb,
tests/python/word.ipynb: Adjust test cases.
* tests/python/formulas.ipynb: Add test for atomic_prop_set.
2018-11-03 07:53:26 +01:00
Alexandre Duret-Lutz
c3b7a691e4 python: add __repr__ for rs_pair
* spot/twa/acc.hh: Hide default constructors, so that we can have
keyword arguments on the main constructor.
* python/spot/impl.i: Add __repr__.
* tests/python/setacc.py: Test it.
2018-11-02 11:10:11 +01:00
Alexandre Duret-Lutz
5bb9c87d4c python: fix return of is_rabin_like() and is_streett_like()
* python/spot/impl.i: Fix instantiation of vector_rs_pairs.
* tests/python/setacc.py: Add test cases.
* NEWS: Mention the bugs.
2018-10-31 19:44:19 +01:00
Alexandre Duret-Lutz
266581b272 python: fix binding of used_inf_fin_sets()
* python/spot/impl.i: Here.
* tests/python/setacc.py: Test it.
* NEWS: Mention the bug.
2018-10-31 15:48:39 +01:00
Alexandre Duret-Lutz
234c9c298f require bison 3.0 and fix obsolete api.location.type usage
* spot/parseaut/parseaut.yy, spot/parsetl/parsetl.yy: Explicitly Bison
3.0, and use a code argument instead of an (deprecated) string
argument for api.location.type.
2018-10-29 15:31:14 +01:00
Alexandre Duret-Lutz
fa24cca76c parseaut: fix signed/unsigned comparison warning
* spot/parseaut/parseaut.yy: Here.
2018-10-29 11:26:25 +01:00
Alexandre Duret-Lutz
e0958ee7c6 python: add xargs support to translate() and postprocess()
Fixes #361.

* python/spot/__init__.py: Implement it.
* tests/python/optionmap.py: Test it.
* NEWS: Mention it.
2018-10-17 18:16:46 +02:00
Alexandre Duret-Lutz
b8e47fdc28 * NEWS: Typo in release date. 2018-10-17 14:17:05 +02:00
Alexandre Duret-Lutz
235508416c Merge branch 'master' into next 2018-10-17 09:35:24 +02:00
Alexandre Duret-Lutz
1878e75ebc bump version to 2.6.3.dev
* NEWS, configure.ac: Here.
2018-10-17 09:34:09 +02:00
Alexandre Duret-Lutz
44283adfc6 Release Spot 2.6.3
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2018-10-17 09:27:22 +02:00
Alexandre Duret-Lutz
31bcb57648 fix ltlfilt --accept-word and --reject-word
* NEWS: Mention the issue.
* bin/ltlfilt.cc: Fix test.
* tests/core/acc_word.test: Test this.
2018-10-15 21:43:47 +02:00
Alexandre Duret-Lutz
34f9fb5d68 option --low should disable gf-guarantee
Fixes #367.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Fix it.
* NEWS: Mention the change.
* tests/core/ltl2tgba2.test: Test this.
2018-10-15 21:43:47 +02:00
Alexandre Duret-Lutz
68a155a818 Büchi translation should not go through fg_safety_to_dca_maybe()
Fixes #366, reported by Simon Jantsch.

* spot/twaalgos/translate.cc: type_&Generic will also match if
type_==BA... use type_==Generic instead.
* tests/core/unambig.test: Add a test corresponding to Simon's report.
* NEWS: Describe the bug.
2018-10-15 21:43:47 +02:00
Alexandre Duret-Lutz
92369d68c6 solve build issue on Debian unstable i386
* tests/python/_product_weak.ipynb: Split large loop in two cells.
2018-10-15 21:42:44 +02:00
Alexandre Duret-Lutz
d94efe9fe1 implement is_liveness() and is_liveness_automaton()
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh,
spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Here.
* bin/ltlfilt.cc (--liveness): New filter.
* NEWS: Mention those.
* tests/core/ltlfilt.test, tests/python/ltlsimple.py: Add test cases.
2018-10-15 21:37:31 +02:00
Alexandre Duret-Lutz
d2316b1428 fix ltlfilt --accept-word and --reject-word
* NEWS: Mention the issue.
* bin/ltlfilt.cc: Fix test.
* tests/core/acc_word.test: Test this.
2018-10-15 21:17:18 +02:00
Alexandre Duret-Lutz
58c1a968c7 option --low should disable gf-guarantee
Fixes #367.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Fix it.
* NEWS: Mention the change.
* tests/core/ltl2tgba2.test: Test this.
2018-10-12 14:08:54 +02:00
Alexandre Duret-Lutz
3c86f034fc Büchi translation should not go through fg_safety_to_dca_maybe()
Fixes #366, reported by Simon Jantsch.

* spot/twaalgos/translate.cc: type_&Generic will also match if
type_==BA... use type_==Generic instead.
* tests/core/unambig.test: Add a test corresponding to Simon's report.
* NEWS: Describe the bug.
2018-10-12 14:08:54 +02:00
Alexandre Duret-Lutz
e5f76b77d4 solve build issue on Debian unstable i386
* tests/python/_product_weak.ipynb: Split large loop in two cells.
2018-10-08 16:03:17 +02:00
Alexandre Duret-Lutz
82a152c38a unabbreviate: add new rules based on eventual/universal arguments
Based on a report by Simon Jantsch.  Fixes #362.

* NEWS, doc/tl/tl.tex: Mention the new rules.
* spot/tl/unabbrev.cc: Implement them.
* tests/core/unabbrevwm.test: Test them.
* tests/python/randltl.ipynb: Adjust.
2018-10-01 17:53:05 +02:00
Alexandre Duret-Lutz
0de334d783 * NEWS: Remove some items from 2.6.2. 2018-10-01 16:44:01 +02:00
Alexandre Duret-Lutz
bfdeadcdbe Merge branch 'master' into next 2018-09-28 10:31:43 +02:00
Alexandre Duret-Lutz
4b2562a33f Bump version to 2.6.2.dev
* NEWS, configure.ac: Here.
2018-09-28 10:12:36 +02:00
Alexandre Duret-Lutz
2828e229bd Release Spot 2.6.2
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
2018-09-28 10:04:39 +02:00
Alexandre Duret-Lutz
5172b9c7d9 org: adjust link to online translator
* doc/org/index.org: Here.
2018-09-28 10:04:17 +02:00
Alexandre Duret-Lutz
3eb26704d6 more gcc-snapshot warnings
* spot/misc/game.hh: Here.
2018-09-27 10:22:49 +02:00