Commit graph

9 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
a3753e608b improve support for LTLf semantics
* spot/twaalgos/remprop.cc, spot/twaalgos/remprop.hh (to_finite): New
function.
* bin/autfilt.cc (--to-finite): Add it.
* doc/org/tut12.org: Update to use it.
* spot/twa/twagraph.cc (purge_dead_states): Also remove false edges.
* spot/parseaut/parseaut.yy: Do not ignore false self-loops, and
add false self-loop on accepting states without successors.
* NEWS: List the above changes.
* tests/core/ltlf.test: New file.
* tests/Makefile.am: Add it.
* tests/core/complete.test: Adjust expected output.
2022-02-07 16:41:59 +01:00
Maximilien Colange
1b2f2a79c1 Fix a bug in spot.complete()
spot.complete() could complete an empty co-Büchi automaton into an
automaton accepting everything.

* NEWS: Document it
* spot/twaalgos/complete.cc: Fix it
* tests/core/complete.test, tests/core/prodor.test: Test it
2017-08-28 17:55:32 +02:00
Alexandre Duret-Lutz
d3607a7ce3 hoa: fix I/O of determinism
Fixes #212.

* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Recognize
exist-branch, and adjust printer to the 1.1 semantics.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/det.test, tests/core/explsum.test,
tests/core/parseaut.test, tests/core/readsave.test,
tests/core/sbacc.test, tests/core/tgbagraph.test,
tests/python/alternating.py, tests/python/dualize.py: Adjust test
cases.
* NEWS: Mention the change.
2017-07-31 22:33:56 +02:00
Alexandre Duret-Lutz
1e9daa73f3 complete: merge edges going to the sink
* spot/twaalgos/complete.cc: Here.
* tests/python/dualize.py, tests/core/complete.test: Adjust test cases.
2017-07-24 16:44:54 +02:00
Alexandre Duret-Lutz
77ce4170dc autfilt: add --is-alternating
* bin/autfilt.cc: Implement --is-alternating.
* tests/core/complete.test: Test it.
* NEWS: Mention it.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
12f6c8cf10 twa_graph: add a merge_univ_dests() method
and call it after parsing

* spot/twa/twagraph.cc, spot/twa/twagraph.hh
(twa_graph::merge_univ_dests): New method.
* spot/parseaut/parseaut.yy: Call it.
* spot/twaalgos/dot.cc: Improve output, now that
several edges can use the same universal destination.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/parseaut.test, tests/python/_altscc.ipynb,
tests/python/alternating.py, tests/python/alternation.ipynb: Adjust
test case.
* doc/org/tut24.org: Adjust example.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
071d819c49 complete: add support for alternating autamata
* spot/twaalgos/complete.cc: Do not use the initial
state as a sink if it is universal.
* tests/core/complete.test: Add a test case.
2016-12-29 12:57:53 +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
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
Renamed from tests/complete.test (Browse further)