Commit graph

25 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
4ab51e1c88 toparity: cover more options
* tests/python/toparity.py: Augment test cases.
2022-10-04 09:24:03 +02:00
Florian Renkin
6dd99e049b to_parity: Rewrite the function and add new transformations
* spot/twaalgos/synthesis.cc: Now needs to call reduce_parity.
* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: here.
* spot/twaalgos/zlktree.hh: make zielonka_node public
* tests/core/ltlsynt.test, tests/python/games.ipynb,
  tests/python/synthesis.ipynb, tests/python/toparity.py:
  update tests
2022-07-07 20:43:21 +02:00
Alexandre Duret-Lutz
530cf7ca47 tests: replace all "assert" by unittest assertions
If the assert fails because of a comparison, it is useful that the
test suite log contains a comparison of these values.
unittest.assertEqual() and friends do that for us.

* HACKING: Add a section about Python tests.
* tests/sanity/style.test: Forbid the use of "assert" in
Python tests.
* tests/python/298.py, tests/python/341.py, tests/python/471.py,
tests/python/accparse2.py, tests/python/aiger.py,
tests/python/aliases.py, tests/python/alternating.py,
tests/python/bdddict.py, tests/python/bdditer.py,
tests/python/bugdet.py, tests/python/complement_semidet.py,
tests/python/declenv.py, tests/python/decompose_scc.py,
tests/python/det.py, tests/python/dualize.py, tests/python/ecfalse.py,
tests/python/except.py, tests/python/game.py, tests/python/gen.py,
tests/python/genem.py, tests/python/implies.py,
tests/python/intrun.py, tests/python/kripke.py,
tests/python/langmap.py, tests/python/ltl2tgba.py,
tests/python/ltlf.py, tests/python/ltlparse.py,
tests/python/ltlsimple.py, tests/python/mealy.py,
tests/python/merge.py, tests/python/mergedge.py,
tests/python/misc-ec.py, tests/python/optionmap.py,
tests/python/origstate.py, tests/python/otfcrash.py,
tests/python/parity.py, tests/python/parsetgba.py,
tests/python/pdegen.py, tests/python/prodexpt.py,
tests/python/randgen.py, tests/python/relabel.py,
tests/python/remfin.py, tests/python/removeap.py,
tests/python/rs_like.py, tests/python/satmin.py,
tests/python/sbacc.py, tests/python/sccfilter.py,
tests/python/sccinfo.py, tests/python/sccsplit.py,
tests/python/semidet.py, tests/python/setacc.py,
tests/python/setxor.py, tests/python/simplacc.py,
tests/python/simstate.py, tests/python/sonf.py, tests/python/split.py,
tests/python/streett_totgba.py, tests/python/streett_totgba2.py,
tests/python/stutter.py, tests/python/sum.py,
tests/python/synthesis.py, tests/python/toparity.py,
tests/python/toweak.py, tests/python/tra2tba.py,
tests/python/trival.py, tests/python/twagraph.py,
tests/python/zlktree.py: Replace all occurrences of "assert" by calls
to unittest.TestCase methods.
2022-03-07 09:03:21 +01:00
Alexandre Duret-Lutz
170d839c4b acd: remove redundant nodes
Reported by Florian Renkin.

* spot/twaalgos/zlktree.cc (acd::_build): Use a sorted list to remove
redundant children, has done in zielonka_tree.
* tests/python/zlktree.ipynb: Add Florian's test case.
* tests/python/toparity.py: Adjust, and revert some tests
uncommented by mistake in a previous patch.
2021-09-05 20:50:33 +02:00
Alexandre Duret-Lutz
26f2179805 zlktree: implement ACD and its transform
A quick and dirty implementation of the Alternating Cycle
Decomposition of the casares.21.icalp paper.

* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh
(maximal_accepting_loops_for_scc): New function.
* spot/twaalgos/sccinfo.cc,
spot/twaalgos/sccinfo.hh (scc_and_mark_filter): Add a possibility to
specify a mask of transition to filter.
* spot/twaalgos/zlktree.hh, spot/twaalgos/zlktree.cc (acd): New class.
(acd_transform): New function.
* python/spot/__init__.py: Add SVG rendering for acd.
* tests/python/_zlktree.ipynb: Play with acd and acd_transform.
* tests/python/toparity.py: Add more tests to compare the
sizes of acd_transform and to_parity.
* NEWS: Mention this new feature.
2021-08-30 10:27:06 +02:00
Alexandre Duret-Lutz
93d8f43285 translate: speed up some -G -D cases
When gf-guarentee works and produce a deterministic automaton, use it
right away without comparing it with the automaton produced by the
regular translation.  This used to be the case for all -D scenarios
except -G -D.

Reported by Florian Renkin.

* spot/twaalgos/translate.cc: Use the result of
gf_guarantee_to_ba_maybe() or fg_safety_to_dca_maybe() whenever -D is
used.
* spot/twaalgos/postproc.cc: Call remove_unused_ap() in finalize(), to
iron out some slight output differences.
* tests/core/ltl2tgba2.test, tests/python/toparity.py: Lower expected
results in the test cases.
* tests/python/automata.ipynb, tests/core/prodor.test: Adjust to new
order.
2021-01-27 13:26:49 +01:00
Alexandre Duret-Lutz
a375089e52 simplify_acceptance: generalize the complementary mark rewriting
Fixes #403.

* spot/twaalgos/cleanacc.cc (simplify_complementary_marks_here):
Assume that two colors are complementary in a broad sense, i.e., on is
present if (but not only if) the other is missing before applying
those rewritings.  Technically, this is usually not necessary, because
the changes done in #418 will cause such "covering-the-full-automaton"
pair of colors to be disjoint so complementary in a strict sense.  It
might make a difference (this is not tested) in presence of reused
colors which #418 cannot remove.  In any case, it's simply less code
to implement the broad sense.
* tests/python/toparity.py: Add test case from #403, which is
reduced to two states with recent optimizations.
2020-07-29 15:01:55 +02:00
Alexandre Duret-Lutz
0c4b701630 improve acceptance simplifications using useless colors
This fixes issue #418.

* spot/twa/acc.cc,
spot/twa/acc.hh (acc_cond::acc_code::useless_colors_patterns): New
method to detect patterns of colors allowing other colors to be added
or removed at will.
* spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Use the above
patterns to remove some useless colors from transitions and hope that
this can help simplify the acceptance condition.
* spot/twaalgos/degen.cc (propagate_marks_vector): Use the pattern to
add more colors.
* tests/core/ltl2tgba2.test: Add the test case from issue #418.
* tests/core/ltl2dstar4.test, tests/core/satmin3.test,
tests/core/sccdot.test, tests/core/sim3.test,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/merge.py, tests/python/pdegen.py, tests/python/remfin.py,
tests/python/toparity.py, tests/python/tra2tba.py: Adjust all test
cases.
* NEWS: Mention this new feature.
2020-07-28 22:26:28 +02:00
Alexandre Duret-Lutz
c0e1b3e52a cleanacc: keep acceptance order when removing complementary colors
* spot/twaalgos/cleanacc.cc (remove_compl_rec): Rewrite to preserve
the original order of the acceptance condition while rewriting it.
* tests/core/sccdot.test, tests/python/merge.py,
tests/python/simplacc.py, tests/python/toparity.py: Adjust test cases.
2020-04-18 23:02:11 +02:00
Alexandre Duret-Lutz
fd0d752bc3 to_parity: only call reduce_parity() when prefix_parity is enabled
Calling reduce_parity() in to_parity() is confusing, because then
running to_parity() on one SCC does not necessarily produce the same
output as running to_parity() on the entire automaton.  However it is
necessary for the implementation of parity_prefix.  As a compromise,
disable reduce_parity() when parity_prefix is disabled, this way we
can use that to demonstrate how the algorithm works.

* spot/twaalgos/toparity.hh, spot/twaalgos/toparity.cc: Do not
call reduce_parity() when parity_prefix is disabled.
* tests/python/toparity.py: Adjust.
2020-04-17 22:04:32 +02:00
Alexandre Duret-Lutz
102ef04364 simplify_acc: loop over the simplifications
* spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Run the
simplifications in a loop until the condition does not change anymore.
* tests/python/simplacc.py, tests/core/accsimpl.test,
tests/core/remfin.test, tests/python/merge.py,
tests/python/simplacc.py, tests/python/toparity.py: Update expected
results.
* tests/python/automata.ipynb: Update the failing example to a more
interesting one, matching the one in doc/org/autfilt.org.
2020-04-17 21:54:12 +02:00
Florian Renkin
68012e6a85 to_parity: Correct the expected number of states
* tests/python/toparity.py: here.
2020-04-17 16:47:02 +02:00
Florian Renkin
527b62c5ff to_parity: Remove merge_states
* spot/twaalgos/toparity.cc: Remove merge_states.
* tests/python/automata.ipynb, tests/python/toparity.py: Update tests.
2020-04-17 14:59:42 +02:00
Florian Renkin
8c48003943 to_parity: Use merge_states
* spot/twaalgos/toparity.cc: Use merge_states at the end
of to_parity.
* tests/python/toparity.py: Update tests.
2020-04-16 22:10:40 +02:00
Alexandre Duret-Lutz
875846f51f toparity: false transitions are not a problem anymore
* spot/twaalgos/toparity.cc: Do not remove false transitions.
* tests/python/toparity.py: Add a test case with false transitions.
2020-04-16 21:12:30 +02:00
Florian Renkin
0ba1097636 to_parity: Improve to_parity and update tests
* spot/twaalgos/toparity.cc: Use a better search of the
transitions when we search compatible states.
* spot/twaalgos/toparity.hh: Use less that 80 columns.
* tests/python/merge.py, tests/python/toparity.py: Update tests.
2020-04-12 19:44:58 +02:00
Florian Renkin
630b8333fe Impove simplify_acceptance
* spot/twaalgos/cleanacc.cc: Use cleanup_acceptance if
propagate_fin_inf was useful.
* spot/twa/acc.hh: Avoid to reverse the order of the condition in
propagate_fin_inf.
* tests/core/accsimpl.test, tests/core/remfin.test,
tests/python/merge.py, tests/python/automata.ipynb: Update tests.
* tests/python/toparity.py: Update tests and add tests to check the
number of states.
2020-04-12 18:31:28 +02:00
Alexandre Duret-Lutz
1db319267f python: simplify to_parity() interface
* python/spot/__init__.py (to_parity): Iterate over the attributes
of spot.to_parity_options instead of naming each option explicitely,
also accept a to_parity_options() instance as argument.
* tests/python/toparity.py: Add tests for both styles of calls, and
reduce the number of random tests to lower the run time of this test.
2020-04-04 15:44:27 +02:00
Alexandre Duret-Lutz
1750c0fb6d to_parity: improve doc, and rename car_option into to_parity_options
* spot/twaalgos/toparity.hh: Improve doc, and rename car_option into
to_parity_options.
* doc/spot.bib: Add one reference.
* python/spot/__init__.py, spot/twaalgos/toparity.cc,
tests/python/toparity.py: Adjust.
2020-04-04 14:43:47 +02:00
Florian Renkin
75990063f0 Moved IAR and the new version of to_parity in toparity.cc
* python/spot/__init__.py: Use keyword arguments in to_parity()
* python/spot/impl.i: remove useless includes.
* spot/twaalgos/car.cc, spot/twaalgos/car.hh,
spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh,
tests/Makefile.am, spot/twaalgos/Makefile.am:
content moved to toparity.
* spot/twaalgos/postproc.cc: Use the new version of to_parity in
postprocessor::run.
* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: Add the
content of rabin2parity and car.
* tests/python/car.py, tests/python/toparity.py: Moved all tests
from car.py to toparity.py.
* tests/python/except.py: Change iar() to iar_old().
2020-03-24 15:41:02 +01:00
Alexandre Duret-Lutz
b2539e8399 improve to_parity() LAR implementation using SCCs
* spot/twaalgos/toparity.cc (lar_generator): Use scc_info to reset
permutations of edges leaving SCCs.
* tests/python/toparity.py: Add a test case.
2019-10-08 11:27:22 +02:00
Alexandre Duret-Lutz
822fe77891 python: cleanup with autopep8
* tests/python/341.py, tests/python/alarm.py, tests/python/bdddict.py,
tests/python/bddnqueen.py, tests/python/bugdet.py,
tests/python/dualize.py, tests/python/except.py, tests/python/gen.py,
tests/python/genem.py, tests/python/implies.py,
tests/python/interdep.py, tests/python/ipnbdoctest.py,
tests/python/kripke.py, tests/python/ltl2tgba.py,
tests/python/ltlf.py, tests/python/ltlparse.py,
tests/python/ltlsimple.py, tests/python/relabel.py,
tests/python/rs_like.py, tests/python/sccsplit.py,
tests/python/semidet.py, tests/python/setacc.py,
tests/python/setxor.py, tests/python/split.py,
tests/python/streett_totgba.py, tests/python/stutter.py,
tests/python/sum.py, tests/python/toparity.py, tests/python/toweak.py,
tests/python/trival.py, python/spot/__init__.py, python/spot/aux.py,
python/spot/jupyter.py: Reformat with autopep8.

fixup! * spot/tl/simplify.cc: Fix typos in tracing code.
2019-07-05 21:22:29 +02:00
Alexandre Duret-Lutz
c66b3d88d0 toparity: revert symmetry-based optimization of LAR
Fixes #390.

* spot/twaalgos/toparity.cc: Revert the relevant part of 516e9536.
* tests/python/toparity.py: Add test case.
* NEWS: Mention the issue.
2019-06-18 19:12:42 +02:00
Maximilien Colange
516e9536df LAR made smarter with symmetry-based degeneralization
* spot/twaalgos/toparity.cc: here
* spot/twa/acc.hh, spot/twa/acc.cc: compute symmetries of an acceptance
  condition
* tests/python/accparse2.py, tests/python/toparity.py: test it
2018-07-27 00:44:19 +02:00
Maximilien Colange
465536d1fe translate any automaton to a parity automaton
* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: implement it,
  based on last-appearance record (LAR)
* spot/twaalgos/Makefile.am: build it
* NEWS: document it
* python/spot/impl.i: add to python bindings
* tests/Makefile.am, tests/python/toparity.py: test it
2018-07-24 14:58:53 +02:00