Commit graph

593 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
fbdd146565 simplify: add missing recursion
"1 U (a | Fb)" was not always reduced to "F(a | b)".

Fixes #143.

* spot/tl/simplify.cc: Add the missing recurse() call.
* tests/core/reduc0.test: Add a test.
* NEWS: Mention the bug.
2016-02-12 08:18:39 +01:00
Alexandre Duret-Lutz
992c97151c ltldo, ltl2tgba: support %< and %>
* bin/common_aoutput.hh, bin/common_aoutput.cc,
bin/ltl2tgba.cc, bin/ltldo.cc: Add support for %< and %>.
* tests/core/ltl2tgba.test, tests/core/ltldo.test: Test it.
* NEWS: Mention it.
2016-02-12 08:18:15 +01:00
Alexandre Duret-Lutz
a31793960f * tests/ltsmin/modelcheck.cc: Typo when printing accepting run. 2016-02-09 14:49:28 +01:00
Alexandre Duret-Lutz
e146527852 twa_run: add a highlight method
* spot/twaalgos/emptiness.hh, spot/twaalgos/emptiness.cc: Add
the method.
* tests/python/highlighting.ipynb: Add a small test.
2016-02-06 17:10:55 +01:00
Alexandre Duret-Lutz
77b0b5b3fe dot: add option C(COLOR)
This fixes the output gliches visible in the previous patches,
where highlighting a state would remove its fill color.

* spot/twaalgos/dot.cc, spot/taalgos/dot.cc: Implement option C(COLOR).
* bin/common_aoutput.cc, doc/org/oaut.org: Document it.
* doc/org/.dir-locals.el.in, doc/org/init.el.in,
python/spot/__init__.py: Use it.
* tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/highlighting.ipynb: Test it.
* tests/core/readsave.test: Adjust.
* NEWS: Mention recent changes.
2016-02-05 19:26:38 +01:00
Alexandre Duret-Lutz
23c2cbf46a python: highlighting functions for edges and states
* python/spot/impl.i (highlight_state, highlight_edge): New function.
* python/spot/__init__.py (highlight_states, highlight_edges): New
functions.
* spot/twaalgos/dot.cc: Add a '#' option.
* spot/taalgos/dot.cc: Ignore '#'.
* tests/python/highlighting.ipynb: New file to illustrate everything.
* tests/Makefile.am, doc/org/tut.org: Add it.
2016-02-05 17:29:30 +01:00
Alexandre Duret-Lutz
348f7cce0b parseaut, dot: install a highlighting framework
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll:
Parse "spot.highlight.edges" and "spot.highlight.states" to
fill the "highlight-edges" and "highlight-states" properties.
* spot/twaalgos/dot.cc: Use these properties to highlight states.
* tests/core/readsave.test: Add a small test.
2016-02-04 23:02:28 +01:00
Alexandre Duret-Lutz
91bb93eeaa parse_acc: cleanup error reporting
* spot/twa/acc.cc: Factor all the error reporting code in a single
place, and improve the error message at end of acceptance.
* tests/core/randaut.test: Add more tests.
2016-02-04 10:48:40 +01:00
Alexandre Duret-Lutz
d5bf95c5cb do not build ikwiad, randtgba, and modelcheck by default
Fix #128.

* tests/Makefile.am: Make these check_PROGRAMS.
* bench/emptchk/Makefile.am: Adjust.
* bench/emptchk/README, bench/emptchk/defs.in: Fix paths.
2016-02-03 22:08:02 +01:00
Alexandre Duret-Lutz
22345d0c67 rename parse_print_test as kripkecat
Fixes #135.

* tests/core/parse_print_test.cc: Rename as...
* tests/core/kripkecat.cc: ... this.
* tests/Makefile.am, tests/core/.gitignore, tests/core/kripke.test,
tests/ltsmin/kripke.test: Adjust.
2016-02-03 21:19:30 +01:00
Alexandre Duret-Lutz
af96cbca83 * tests/python/ltsmin.ipynb: Erase the model file. 2016-02-03 08:51:37 +01:00
Alexandre Duret-Lutz
02b5460b91 dot, hoa: default to "k" for kripke structure
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc: If a Kripke
structure is passed, automatically enable the "k" option.
* tests/core/parse_print_test.cc, tests/ltsmin/modelcheck.cc,
tests/python/ltsmin.ipynb: Remove the explicit use of "k".
* NEWS: Mention the change.
2016-02-01 22:12:13 +01:00
Alexandre Duret-Lutz
a9b4560f3d dot: add option "k"
Fixes #134.

* spot/twaalgos/dot.cc: Implement it.
* bin/common_aoutput.cc, spot/twaalgos/dot.hh, NEWS: Document it.
* tests/core/readsave.test, tests/python/ltsmin.ipynb: Test it.
2016-02-01 08:38:45 +01:00
Alexandre Duret-Lutz
5a5f83f468 python: add missing bindings for twa_word and twa_run
Fixes #133.

* python/spot/impl.i: Add bindings for twa_word.  Add a __repr__
for twa_run, and instantiate templates for twa_run's members.
* tests/python/word.ipynb: New file with examples.
* tests/Makefile.am, doc/org/tut.org: Add it.
2016-01-31 21:05:44 +01:00
Alexandre Duret-Lutz
eb0a0b6b34 dot: use circles if state names are all short
* spot/twaalgos/dot.cc: Check for state names sizes.
* tests/core/readsave.test: Test the change.
* tests/core/tgbagraph.test: Adjust.
2016-01-29 13:39:17 +01:00
Alexandre Duret-Lutz
b11c07b351 dot: add a <N option
* spot/twaalgos/dot.cc: Implement it.
* spot/taalgos/dot.cc: Ignore it.
* spot/twaalgos/copy.cc, spot/twaalgos/copy.hh: Add option
to limit the number of states.
* tests/python/ltsmin.ipynb: Improve test case.
* tests/Makefile.am: Cleanup the files generated by ltsmin.ipynb.
* python/spot/__init__.py (setup): Add a max_states argument
that default to 50.
* bin/common_aoutput.cc: Mention the <INT option.
* NEWS: Likewise.
2016-01-29 09:09:05 +01:00
Alexandre Duret-Lutz
4571d6dd3a copy: rewrite as a BFS without using reachiter
* spot/twaalgos/copy.hh: Trim includes.
* spot/twaalgos/copy.cc: Rewrite.
* tests/python/ltsmin.ipynb: Adjust.
2016-01-28 15:37:00 +01:00
Alexandre Duret-Lutz
c968e7b856 ltl2tgba_fm: fix setting of unambiguous property
Report from Joachim Klein.

* spot/twaalgos/ltl2tgba_fm.cc: Set the property, do not read it.
* tests/core/unambig.test: Add a test.
* NEWS: Mention the bug.
2016-01-26 19:38:50 +01:00
Alexandre Duret-Lutz
db1e842a67 ltsmin: add accessors for variable names and types
* spot/ltsmin/ltsmin.hh, spot/ltsmin/ltsmin.cc: Expose more of the
ltsmin interface.
* python/spot/ltsmin.i: Add some helper functions on top of this
new interface.
* tests/python/ltsmin.ipynb: Test them.
* NEWS: Mention it.
2016-01-26 19:21:35 +01:00
Alexandre Duret-Lutz
907b72fbfb ltsmin: implement a two-step loading
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh: Split load_ltsmin() into
ltsmin_model::load() and ltsmin_model::kripke().  Report errors using
exceptions instead of on std::cerr.
* python/spot/ltsmin.i: Deal with exceptions.
* tests/ltsmin/modelcheck.cc, tests/python/ltsmin.ipynb: Adjust.
2016-01-26 19:21:35 +01:00
Alexandre Duret-Lutz
84031d2ae1 more files to ignore
* python/.gitignore, tests/.gitignore: Here.
2016-01-26 19:21:35 +01:00
Alexandre Duret-Lutz
0c2997990d * tests/run.in: Honor PREFIXCMD even without argument. 2016-01-26 19:21:35 +01:00
Alexandre Duret-Lutz
5a9b0aa1c1 python: add bindings for ltsmin
* python/spot/ltsmin.i: New file.
* python/Makefile.am: Add it.
* python/spot/impl.i: Add bindings for kripke and fair_kripke.
* tests/python/ltsmin.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* tests/python/ipnbdoctest.py: Make it possible for notebook
to exit(77).
* debian/control: Make the Python package dependent
on libspotltsmin0.
* python/spot/__init__.py: Typo.
2016-01-26 19:20:53 +01:00
Alexandre Duret-Lutz
215fcb799a Make spot.py a python package instead of a module
* python/spot.py, python/spot_impl.i: Rename as...
* python/spot/__init__.py, python/spot/impl.i: ... these.
* python/Makefile.am, tests/run.in: Adjust for new paths.
* tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/piperead.ipynb,
tests/python/testingaut.ipynb: Adjust messages to refer to spot.impl
instead of spot_impl.
2016-01-26 19:20:26 +01:00
Alexandre Duret-Lutz
c4e9083f4e product: raise an exception if the dict are different
Fixes #132.

* python/spot.py (translate): Allow changing the dictionary.
* tests/python/prodexpt.py: New file.
* tests/Makefile.am: Add it.
* spot/twa/twaproduct.cc, spot/twaalgos/product.cc: Add them.
* NEWS: Mention the change.
2016-01-23 21:28:35 +01:00
Alexandre Duret-Lutz
66d8f3ce09 work around core dump created by running ipython4
* tests/Makefile.am (distclean-local): Erase python/core.
2016-01-14 18:37:48 +01:00
Alexandre Duret-Lutz
51483b9b7f fix complete
Alexandre Lewkowicz reported a case where complete() would peek an
existing state that is accepting, and wrongly use it as a sink.

* spot/twaalgos/complete.cc: Fix the function.
* tests/core/complete.test: Add two more tests.
* NEWS: Mention the bug.
2016-01-14 17:16:17 +01:00
Alexandre Duret-Lutz
6c62362fe9 parseaut: add support for negated properties
* spot/parseaut/parseaut.yy: Here.
* tests/core/parseaut.test: Test it.
* NEWS: Mention it.
2016-01-14 16:58:17 +01:00
Alexandre Duret-Lutz
da391492f3 twa: store property bits as trivals
* spot/twa/twa.hh: Store property bits as trivals.
* NEWS: Mention the change.
* spot/parseaut/parseaut.yy, spot/twaalgos/are_isomorphic.cc,
spot/twaalgos/complete.cc, spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/isdet.cc, spot/twaalgos/isunamb.cc, spot/twaalgos/lbtt.cc,
spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/postproc.cc,
spot/twaalgos/remfin.cc, spot/twaalgos/strength.cc,
spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh,
spot/twaalgos/totgba.cc, tests/core/ikwiad.cc,
tests/python/product.ipynb, tests/python/remfin.py: Adjust.
* doc/org/hoa.org, doc/org/tut21.org: Update documentation.
2016-01-13 17:57:54 +01:00
Alexandre Duret-Lutz
1aeb260adf trival: new class for tri-valued logic
* spot/misc/trival.hh: New file.
* spot/misc/Makefile.am: Add it.
* python/spot_impl.i: Add Python bindings.
* tests/core/trival.cc, tests/core/trival.test,
tests/python/trival.py: New files, testing it.
* tests/Makefile.am: Add them.
2016-01-13 17:57:54 +01:00
Etienne Renault
e764cf6f3b Preserve named-states during defrag
* spot/twa/twagraph.cc, spot/twa/twagraph.hh,
tests/core/tgbagraph.test, tests/core/twagraph.cc,
NEWS: here.
2016-01-12 21:06:46 +01:00
Alexandre Duret-Lutz
d0b38156f3 bin: make HOA the default output
* bin/common_aoutput.cc: Make HOA the default output.
* NEWS: Mention this.
* doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/hoa.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org,
doc/org/satmin.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org,
tests/core/dstar.test, tests/core/ltldo2.test, tests/core/monitor.test,
tests/python/piperead.ipynb: Adjust.
2016-01-08 13:42:57 +01:00
Alexandre Duret-Lutz
9d6727da5c bin: add support for SPOT_DEFAULT_FORMAT
* bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_setup.cc:
Implement it.
* NEWS, bin/man/spot-x.x: Document it.
* tests/core/readsave.test: Test it.
2016-01-06 18:17:06 +01:00
Alexandre Duret-Lutz
cca2022e90 bin: add -d as a shorthand for --dot
* bin/common_aoutput.cc: Here.
* NEWS, doc/org/oaut.org: Mention it.
* tests/core/readsave.test: Use it once.
2016-01-06 16:27:59 +01:00
Alexandre Duret-Lutz
ea5f52ddbb randaut: rename -d as -e
This is so that we can have -d as an alias for --dot everywhere.

* bin/randaut.cc: Rename -d as -e.
* NEWS: Mention the change.
* doc/org/autfilt.org, doc/org/oaut.org, doc/org/randaut.org,
tests/core/parseaut.test, tests/core/readsave.test: Adjust.
2016-01-06 15:54:11 +01:00
Alexandre Duret-Lutz
5232e6a2fb * tests/core/randaut.test: Simplify calls to randaut/autfilt. 2016-01-06 15:17:59 +01:00
Alexandre Duret-Lutz
f470edc6c4 Do not run the Python tests when --disable-python.
* tests/Makefile.am (TESTS_python): Define conditionally.
2016-01-06 14:24:51 +01:00
Alexandre Duret-Lutz
d68db6ad44 use find to clean to test suite temporary directories
* tests/Makefile.am (distclean-local): Here.
2016-01-05 17:20:51 +01:00
Alexandre Duret-Lutz
6e854b6d83 move the sanity tests in tests/sanity/
* spot/sanity/: Move ...
* tests/sanity/: ... here.
* spot/sanity/Makefile.am: Merge with...
* tests/Makefile.am: ... this.
* tests/run.in: Learn to run perl tests.
* README, configure.ac, spot/Makefile.am: Adjust.
* spot/tl/mark.hh: Add missing SPOT_API detected by
fixed private.test.

* spot/twaalgos/weight.cc, spot/twaalgos/weight.hh: Move...
* spot/priv/weight.cc, spot/priv/weight.hh: ... here, as
suggested by fixed private.test.
* spot/twaalgos/tau03opt.cc, spot/twaalgos/Makefile.am,
spot/priv/Makefile.am: Adjust.
2016-01-05 17:20:51 +01:00
Alexandre Duret-Lutz
6b881a2e38 * tests/python/ipnbdoctest.py: 80 columns. 2016-01-05 11:53:03 +01:00
Alexandre Duret-Lutz
ddc424f5a3 move ltsmin tests to tests/ltsmin/
* spot/ltsmin/defs.in: Delete.
* spot/ltsmin/README, spot/ltsmin/beem-peterson.4.dve,
spot/ltsmin/check.test, spot/ltsmin/elevator2.1.pm,
spot/ltsmin/finite.dve, spot/ltsmin/finite.pm, spot/ltsmin/finite.test,
spot/ltsmin/finite2.test, spot/ltsmin/kripke.test,
spot/ltsmin/modelcheck.cc: Move...
* tests/ltsmin/: ... here.
* spot/ltsmin/README: Point to tests/ltsmin/README.
* README, configure.ac, spot/ltsmin/Makefile.am, tests/.gitignore,
tests/Makefile.am, tests/core/defs.in: Adjust.
2016-01-05 11:52:24 +01:00
Alexandre Duret-Lutz
5cb94a1a3f Merge the core and python tests in the tests/ directory
* tests/: Rename as...
* tests/core/: ... this.
* python/tests/: Rename as...
* tests/python/: ... this.
* python/tests/run.in: Move as...
* tests/run.in: This, and adjust.
* tests/Makefile.am: Adjust to run both core and python tests.
* configure.ac, README, debian/python3-spot.examples, debian/rules,
doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.
2016-01-04 16:02:30 +01:00
Alexandre Duret-Lutz
134dfc73de move spot/bin/ and spot/tests/ up by one level
* spot/bin/: Move...
* bin/: ... here.
* spot/tests/: Move...
* tests/: ... here.
* Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc, doc/Makefile.am,
configure.ac, debian/rules, spot/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/style.test, python/tests/run.in:
Adjust.
2015-12-27 20:10:59 +01:00