* spot/twaalgos/game.cc, spot/twaalgos/game.hh (game_info): Move...
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh (synthesis_info): ... here, because this
structure contains only synthesis stuff. Also rename "solver" to
"algo" to match the ltlsynt option.
(solve_game): Move the two argument version of this function here,
since that's the only game-related generic function that use
synthesis_info.
* bin/ltlsynt.cc, tests/core/ltlsynt.test, tests/python/games.ipynb,
tests/python/synthesis.py, NEWS: Adjust all uses and mentions.
* bin/ltlsynt.cc: Implement the new option, and make it default
to bisimulation with output assignment (a.k.a. bwoa).
* NEWS, bin/spot-x.cc, doc/org/ltlsynt.org: Update the documentation.
* spot/twaalgos/game.hh: Make bwoa the default.
* tests/core/ltlsynt.test: Add and adjust test cases.
* tests/python/games.ipynb: Adjust.
* bin/ltlsynt.cc: Implement the option, and enable it by default.
* doc/org/ltlsynt.org, doc/org/ltlsynt.tex, bin/spot-x.cc, NEWS:
Document it.
* tests/core/ltlsynt.test: Adjust test cases.
* spot/tl/simplify.cc (tl_simplifier_cache::as_bdd): Fix the order in
which as_bdd() is called recursively in binary nodes, do not let the
choice to the compiler.
* tests/core/ltlsynt.test: Adjust expected output.
* spot/twaalgos/dtwasat.cc: Do not return a transition-based automaton
when state-based output is requested.
* tests/python/satmin.ipynb, spot/twaalgos/dtbasat.hh: Fix some typos.
* tests/python/satmin.py: Add test cases.
* NEWS: Mention the bugs.
* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Add the
acd_options::ORDER_HEURISTIC and use it by default in
acd_transform_sbacc().
* spot/misc/bitvect.hh (bitvect::count, bitvect::add_common): New
methods.
* tests/python/zlktree.ipynb: Adjust examples and discuss this
heuristic.
Removing this option to guarante that all arenas
are alternating
* spot/twaalgos/synthesis.hh: Here
* spot/twaalgos/synthesis.cc: Here
* spot/twaalgos/mealy_machine.cc: API change
* tests/python/aiger.py: API change
* tests/python/mealy.py: API change
* tests/python/split.py: API change
Fixes#477.
* bin/common_finput.cc (job_processor::process_string): Fix return
value.
* bin/ltlsynt.cc: Fix handling of syntax errors. While we are here,
make sure game_info is destroyed before Spot's globals.
* tests/core/ltlsynt.test: Add a test case.
By default only propositions appearing in the strategy are
treated. By handing over propositions explicitly one
can force their appearance in the aig circuit.
* spot/twaalgos/aiger.cc: Here
* spot/twaalgos/aiger.hh: New doc
* tests/python/games.ipynb: New test
Introducing the new game interface
to ltlsynt.
ltlsynt now also uses direct strategy deduction
and formula decomposition.
* bin/ltlsynt.cc: Here
* spot/twaalgos/aiger.cc
, spot/twaalgos/aiger.hh: Use strategy_like
* spot/twaalgos/game.hh: Minor adaption
* spot/twaalgos/mealy_machine.cc: Use new interface
* spot/twaalgos/synthesis.cc
, spot/twaalgos/synthesis.hh: Spezialised split
* tests/core/ltlsynt.test
, tests/python/games.ipynb: Adapting
Also remove self-loop for sink and make it work for any
acceptance condition.
* spot/twaalgos/synthesis.cc: Here
* tests/core/ltlsynt.test: Adjust tests
* tests/python/split.py: Adjust tests
Introduce a new, uniform way to create and solve
games.
Games can now be created directly from specification
using creat_game, uniformly solved using
solve_game and transformed into a strategy
using create_strategy.
Strategy are mealy machines, which can be minimized.
* bin/ltlsynt.cc: Minor adaption
* spot/twaalgos/game.cc: solve_game, setters and getters
for named properties
* spot/twaalgos/game.hh: Here too
* spot/twaalgos/mealy_machine.cc: Minor adaption
* spot/twaalgos/synthesis.cc: create_game, create_strategy and
minimize_strategy
* spot/twaalgos/synthesis.hh: Here too
* tests/core/ltlsynt.test: Adapting
* tests/python/aiger.py
, tests/python/games.ipynb
, tests/python/mealy.py
, tests/python/parity.py
, tests/python/split.py: Adapting
The merging is (possibly) more expensive but also
merges more states when applied to all states.
* spot/graph/graph.hh: edge sorting
* spot/twa/twagraph.cc,
spot/twa/twagraph.hh: selective state merging
* tests/core/twagraph.cc: Adjusting tests
Aiger circuits noew have their own class.
Monitors can be translated to and obtained
from aiger circuits.
Moreover a step by step evaluation method
is provided.
* spot/twaalgos/aiger.hh,
spot/twaalgos/aiger.cc: Here
* bin/ltlsynt.cc: Adopt new modes
* tests/core/ltlsynt.test: Adapt tests
* python/spot/impl.i: Add python support
* tests/Makefile.am,
tests/python/aiger.py: New test cases
This improves the parsing performance a bit more.
* spot/parseaut/parsedecl.hh, spot/parseaut/parseaut.yy: Here.
* tests/sanity/style.test: Handle parsedecl.hh as a private header.
This version of the generic emptiness-check, using smart selection and
extraction of the Fin (implemented here via fin_one_extract), was
suggested by Jan Strejček on 2020-06-26.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Add the spot210
variant. Also use it for the ACD use-case.
* spot/twaalgos/zlktree.cc (zielonka_tree): Also use the same logic
here.
* tests/python/genem.py: Test the new version as well.
* spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::fin_one_extract,
acc_code::acc_cond::fin_one_extract): New methods.
* python/spot/impl.i: Add support for the return type.
* tests/python/acc_cond.ipynb: Test them.
Reported by Florian.
* spot/twaalgos/zlktree.cc: Handle the case where the condition does
not cover all colors.
* tests/python/zlktree.py: New file.
* tests/Makefile.am: Add it.
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.
This will be handy latter to develop widgets with interactive
highlighting of automata.
* spot/twaalgos/dot.cc: Implement it.
* bin/common_aoutput.cc, NEWS, doc/org/oaut.org,
doc/org/spot.css: Document it.
* tests/core/alternating.test, tests/core/readsave.test,
tests/core/sccdot.test: Test it.
* spot/twaalgos/zlktree.cc (zielonka_tree): Find the models using a
recursive procedure on the acceptance condition, without conversion to
BDD.
* tests/python/_zlktree.ipynb: Adjust to a different order of nodes.
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.
* spot/twaalgos/zlktree.hh,
spot/twaalgos/zlktree.cc (zielonka_tree_transform): New function.
* tests/python/_zlktree.ipynb: Test it on three examples.
* spot/twa/twagraph.cc (merge_states): Return the number
of removed states, and use that to decide if defrag_states
is needed.
* spot/twa/twagraph.hh, NEWS: Document that.
* tests/core/tgbagraph.test, tests/core/twagraph.cc: Adjust test case.
Fixes#468.
* python/spot/__init__.py: Add wrapper around twa::acc() and
twa::get_acceptance() to store the automaton into the acceptance
proxy, therefore ensuring that the automaton survives that proxy.
* tests/python/setacc.py: Test it.
It was noted in #470 that make_twa_graph did not copy named
properties. Let's fix that.
* spot/twa/twa.hh, spot/twa/twa.cc (copy_named_properties_of): New
method.
* spot/twa/twagraph.hh (make_twa_graph): Add an extra argument to
call copy_named_properties_of() optionally.
* python/spot/__init__.py (twa_graph.__copy__): Use it.
* tests/python/twagraph.py: Test that.
* tests/sanity/namedprop.test: Ensure copy_named_properties_of copies
all known named properties.
Fixes#470, suggested by Cambridge Yang.
* python/spot/__init__.py (twa_graph.__copy__): Call make_twa_graph.
* tests/python/twagraph.py: Test it.
* NEWS: Mention it.
Fixes#471, reported by Cambridge Yang.
* spot/twa/twa.cc (intersecting_run): Disable the product
optimization for weak automata.
* tests/python/471.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
Part of #471.
* spot/twaalgos/emptiness.cc: Throw an exception if
the cycle is rejecting.
* spot/twaalgos/emptiness.hh: Document this behavior.
* tests/python/except.py: Test it.
This fixes#469.
* spot/misc/bitset.hh (bitset::operator-): Rewrite.
I cannot follow the logic of the old implementation.
* tests/python/setacc.py: Add a test case, inspired from #469.
