Commit graph

14 commits

Author SHA1 Message Date
Arthur Remaud
f7bbfd2812 autfilt: Better display of cluster when universal edge loops in it
Fixes #208

* NEWS: Informations about the modifications
* spot/twaalgos/dot.cc (print): Gestion of cluster for
universal transitions
* tests/core/alternating.test: tests added
* tests/core/neverclaimread.test: tests changed for
new dot format
* tests/core/readsave.test: tests changed
* tests/core/sccdot.test: tests changed
* tests/python/_altscc.ipynb: tests changed
* tests/python/decompose.ipynb: tests changed
2017-02-16 18:53:18 +01:00
Arthur Remaud
34859568cd autfilt: add option (y) to --dot to split universal transitions
Fixes #207

* NEWS: Informations about the option 'y' for --dot added
* bin/common_aoutput.cc: Documentation for the option 'y'
for --dot added
* spot/twaalgos/dot.cc (print_dst, process_link): Functions
modified for the new option
* tests/core/alternating.test: Tests added
2017-02-16 18:52:37 +01:00
Alexandre Duret-Lutz
15c6fd9562 alternation: fix detection of non-weak automata
Fixes #218.

* spot/twaalgos/alternation.cc: Adjust check.
* tests/core/alternating.test: Add test case from #218.
* NEWS: Mention the bug.
2017-02-12 01:37:52 +01:00
Alexandre Duret-Lutz
3ff2acb397 alternation: better detection of non-weak alternating automata
* spot/twaalgos/alternation.cc: Fix the code to also check the
weakness of single-state SCCs.
* tests/core/alternating.test: Add a test from ltl3hoa.
2017-01-14 10:02:37 +01:00
Alexandre Duret-Lutz
12ecb3febf twagraph: fix purge_dead_states on alternating automata
* tests/core/alternating.test: Run some of the test through
valgrind to exhibit the bug.
* spot/twa/twagraph.cc: Fix it.
2017-01-10 10:29:32 +01:00
Alexandre Duret-Lutz
db5d9780f1 twa_graph: support alternation in remove_dead/unreachable_states
* spot/graph/graph.hh (internal::univ_dest_mapper): New helper class.
* spot/twa/twagraph.cc (merge_univ_dests): Simplify using
univ_dest_mapper.
(purge_unreachable_states, purge_dead_states): Add support for
alternation.
* tests/core/alternating.test: More tests.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
096c78a3f8 autfilt: handle alternation with --equivalent-to and friends
* bin/autfilt.cc (ensure_deterministic): Remove alternation on demand.
(process_automaton): Prefer twa::intersects() over
product()/is_empty().
* spot/twa/twa.cc (remove_fin_maybe): Also remove alternation.
* tests/core/alternating.test: More tests.
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
f5b261d80e remfin: call remove_alternation if needed
* spot/twaalgos/remfin.cc: Here.
* tests/core/alternating.test: Add a test case.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
f1b8d5f1d4 postproc: preliminary support for alternating automata
* spot/twaalgos/postproc.cc: Call remove_alternation().
* tests/core/alternating.test: Additional test.
2016-12-29 12:57:53 +01:00
Alexandre Duret-Lutz
582d455c23 twa: add support for very-weak property
* spot/twa/twa.hh: Implement the property.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input
and output for it.
* spot/twaalgos/strength.cc,
spot/twaalgos/strength.hh (is_very_weak_automaton): New function.
* tests/core/alternating.test: Add a test for --check=strength
on an alternating automaton.
* tests/core/strength.test, tests/core/parseaut.test: Adjust expected
output.
* NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it.
2016-12-27 12:36:38 +01:00
Alexandre Duret-Lutz
a4ce999402 sccinfo: adjust to work with alternating automata
* spot/twaalgos/sccinfo.cc: Consider universal edges as if they were
existential edges.
* spot/twaalgos/sccinfo.hh: Document that.
* spot/twaalgos/dot.cc: Allow option 's' again, for easy testing.
* tests/core/alternating.test: Adjust tests.
* tests/python/_altscc.ipynb: New file (more tests).
* tests/Makefile.am: Add it.
2016-12-27 12:36:38 +01:00
Alexandre Duret-Lutz
48c812a595 twa_graph: add support for universal initial states
The only missing point is that the HOA parser cannot deal with multiple
universal initial states, as seen in parseaut.test.

* spot/graph/graph.hh (new_univ_dests): New function, extracted from...
(new_univ_edge): ... this one.
* spot/twa/twagraph.hh (set_univ_init_state): Implement using
new_univ_dests.
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, python/spot/impl.i:
Add support for universal initial states.
* spot/parseaut/parseaut.yy: Add preliminary support for
universal initial states.  Multiple universal initial states
are still not supported.
* tests/core/alternating.test, tests/core/parseaut.test,
tests/python/alternating.py: Adjust tests and exercise this new feature.
2016-12-27 12:36:38 +01:00
Alexandre Duret-Lutz
d5c9c34514 dot: add support for alternating automata
* spot/twaalgos/dot.cc: Handle universal destinations.
Ignore option 's' for alternating automata.
* tests/core/alternating.test: New file.
* tests/Makefile.am: Add it.
2016-12-27 12:36:38 +01:00