alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
4014 commits 6 branches 0 tags 36 MiB
Commit graph

43 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
1afb76a630 split ltsmin/check.test in three files 
Fixes #195.

* tests/ltsmin/check.test: Extract the spins and gal checks
and move them to...
* tests/ltsmin/check2.test, tests/ltsmin/check3.test: ... these files.
* tests/Makefile.am: Adjust.
 2016-11-24 11:36:26 +01:00
Maximilien Colange
c9aabcddab Add support to load GAL models. 
* spot/ltsmin/ltsmin.cc: Handle GAL models.
* tests/Makefile.am: Test the new feature.
* tests/ltsmin/check.test: Also check GAL.
* tests/ltsmin/beem-peterson.4.gal: A new GAL model for tests.
* tests/ltsmin/finite.gal: A new GAL model for tests.
* tests/ltsmin/finite3.test: A new test for GAL.
 2016-11-23 11:03:30 +01:00
Alexandre Duret-Lutz
85f6e0e158 scc_filter: preserve state names and highlighted states 
Suggested by Juraj Major.

* spot/twaalgos/sccfilter.cc: Here.
* tests/python/sccfilter.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the news.
 2016-11-11 15:21:17 +01:00
Alexandre Duret-Lutz
dd706d7847 twa: do not set prop_state_acc in set_acceptance 
Reported by Juraj Major.

* spot/twa/twa.hh: check num_sets() in prop_state_acc() so we do not
have to set it in set_acceptance(), causing trouble if set_acceptance()
is called multiple times.
* tests/python/setacc.py: New test case.
* tests/Makefile.am: Add it.
* THANKS: Add Juraj.
* NEWS: Mention the bug.
 2016-11-11 15:20:56 +01:00
Alexandre Duret-Lutz
75c33defb3 attempt to mitigate our Debian build failures 
* tests/Makefile.am: Run Python tests before other tests.
* tests/python/ipnbdoctest.py: Add some debug.
 2016-11-09 05:55:02 +01:00
Alexandre Duret-Lutz
2e69e04583 from_ltlf: new LTL transformation. 
Fixes #187.

* spot/tl/ltlf.cc, spot/tl/ltlf.hh: New files.
* spot/tl/Makefile.am: Add them.
* bin/ltlfilt.cc: Add a new option.
* bin/man/ltlfilt.x: Add bibliographic reference.
* tests/core/ltlfilt.test: Add more tests.
* tests/python/ltlf.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i: Python bindings.
* NEWS: Mention it.
 2016-11-05 22:59:02 +01:00
Alexandre Duret-Lutz
d919b78c89 simulation: do not purge unreachable states when recording implications 
This fixes the incorrect output of tgba_determinize() reported yesterday
by Reuben Rowe.

* spot/twaalgos/simulation.cc: Do not purge unreachable states when
recording implications.
* tests/python/bugdet.py: New test case.
* tests/Makefile.am: Add it.
* THANKS: Add Reuben.
* NEWS: Mention the bug.
 2016-11-01 09:29:55 +01:00
Alexandre Duret-Lutz
926ffbf965 bin: %a,%b,%s format specs for LTL output 
* NEWS: Mention those.
* bin/common_output.cc, bin/common_output.hh: Implement them.
* bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Update
--help.
* tests/core/format.test: New file.
* tests/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org: Update documentation.
 2016-08-15 16:09:53 +02:00
Alexandre Duret-Lutz
e97ea5fa74 bin: diagnose more write errors 
* tests/core/full.test: New file.
* tests/Makefile.am: Add it.
* bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh,
bin/common_file.cc, bin/common_file.hh, bin/genltl.cc, bin/ltlcross.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Add diagnostics.
* NEWS: Mention the fix.
 2016-08-14 18:18:20 +02:00
Alexandre Duret-Lutz
14bee1ae7f implement conversion to GRA and GSA 
Fixes #174.

* spot/twaalgos/totgba.hh, spot/twaalgos/totgba.cc
(to_generalized_streett, to_generalized_rabin): New functions.
* spot/twa/acc.hh: Declare more methods as static.
* bin/autfilt.cc: Implement --generalized-rabin and
--generalized-streett options.
* NEWS: Mention these.
* tests/core/gragsa.test: New file.
* tests/Makefile.am: Add it.
 2016-08-04 22:24:30 +02:00
Alexandre Duret-Lutz
a7842ac47f tests: disable ltsmin tests if --disable-shared 
* configure.ac (USE_LTSMIN): New.
* tests/Makefile.am: Use it.
 2016-07-27 19:47:34 +02:00
Alexandre Duret-Lutz
b136b81c6d new test case to improve coverage stats 
The streett_to_generalized_buchi() function was not tested unless
ltl2dstar is installed.

* tests/core/streett.test: New file.
* tests/Makefile.am: Add it.
 2016-07-19 13:35:47 +02:00
Alexandre Duret-Lutz
57f47c16e7 genltl: support --positive and --negative 
* bin/genltl.cc: Implement these options.
* NEWS: Mention them.
* tests/core/genltl.test: New file with test cases.
* tests/Makefile.am: Add it.
 2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
e419150c30 option_map: Diagnose unused option on request 
* spot/misc/optionmap.hh, spot/misc/optionmap.cc (report_unused_options,
set_, set_set_): New methods.
* bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc,
bin/ltl2tgta.cc: Call report_unused_options().
* tests/core/ltlcross2.test, tests/core/readsave.test: Fix typos in
options.
* tests/core/minusx.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention this.
 2016-06-22 20:57:53 +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
f46d39f852 * tests/Makefile.am: Distribute elevator2.1.pm. 2016-06-14 12:02:41 +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
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
50c2192edf tests: correctly declare word.ipynb 
Fixes #158, reported by Laurent Xu.

* tests/Makefile.am (TESTS_python): Move word.ipynb...
(TESTS_ipython): ... here.
 2016-03-17 18:07:45 +01:00
Amaury Fauchille
1c82444376 autfilt: add new option --accept-word 
Suggested by Matthias Heizmann. Fixes #109.

* NEWS: notify the new option
* THANKS: add Matthias Heizmann
* bin/autfilt.cc: add new option --accept-word=WORD which filters
automata that accept WORD
* doc/org/autfilt.org: add an example of the new option
* tests/Makefile.am: add core/acc_word.test to the list of test files
* tests/core/acc_word.test: test some uses of the new option
 2016-03-07 22:19:25 +01:00
Alexandre Duret-Lutz
cbfca2291e * tests/Makefile.am: Move ltsmin.ipynb to TESTS_ipython. 2016-02-17 13:43:28 +01:00
Alexandre Duret-Lutz
b56aec242a debian: do not distribute _*.ipynb files 
* tests/Makefile.am (nb-html): Only work on the subset of the notebooks
we want to show.
* debian/python3-spot.examples: Ignore _*.ipynb files.
 2016-02-17 08:53:02 +01:00
Alexandre Duret-Lutz
3a3913cf50 otf_product: fix deletion of iter_cache_ 
Fixes #152, reported by Valentin Iovene.

* spot/twa/twaproduct.cc (~twa_product): Delete iter_cache_.
* tests/python/otfcrash.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
 2016-02-16 17:26:41 +01:00
Alexandre Duret-Lutz
22af7aefdf python: report dot errors 
* python/spot/aux.py: Catch errors from dot and signal them.
* tests/python/_aux.ipynb: New file.
* tests/Makefile.am: Add it.
* tests/sanity/ipynb.pl: Support the convention that tests starting with
'_' should not be published on the web site.
 2016-02-16 14:34:57 +01:00
Alexandre Duret-Lutz
021921f0c3 autfilt: add --included-in filter 
* bin/autfilt.cc: Implement the option.
* tests/core/included.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the new option.
 2016-02-12 17:46:38 +01:00
Alexandre Duret-Lutz
6a662a6d8e get read of twa_safra_complement 
* spot/twa/twasafracomplement.cc, spot/twa/twasafracomplement.hh,
tests/core/complementation.cc: Delete.
* tests/Makefile.am, spot/twa/Makefile.am: Adjust.
* tests/core/complementation.test: Rewrite using the new determinization
code.
* python/spot/impl.i: Do not mention twa_safra_complement anymore.
* NEWS: Mention the removal.
 2016-02-12 15:09:37 +01:00
Alexandre Lewkowicz
8068cfad93 safra: Add complete option and rename files 
* src/tests/safra.cc, src/twaalgos/safra.cc,
src/twaalgos/safra.hh, src/tests/safra.test: Rename as...
* spot/twaalgos/safra.cc, spot/twaalgos/safra.hh, tests/core/safra.cc
tests/core/safra.test: ... these.
* tests/Makefile.am: Update.
 2016-02-12 14:07:28 +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
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
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
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
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
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
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
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
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
Renamed from spot/tests/Makefile.am (Browse further)