* 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/twaalgos/game.hh, spot/twaalgos/synthesis.hh,
spot/twaalgos/aiger.hh: Declare new Doxygen groups for games and
synthesis.
* doc/spot.bib: Cleanup.
This addresses a few points from #479.
* doc/org/ltlsynt.tex: New file.
* doc/Makefile.am: Add it.
* doc/org/ltlsynt.org: Show the architecture, and mention more
options.
* bin/spot-x.cc: Document ltlsynt's -x options.
* bin/ltlsynt.cc: Fix default value of --aiger, and typo in its
documentation.
* 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/zlktree.cc, spot/twaalgos/zlktree.hh (acd::build_):
When processing a node identical to a node previously seen, simply
copy the children of that other node, and share its vectors.
* doc/org/tut40.org: Add more explanations and some cleanup.
* python/spot/__init__.py (set_state_players, get_state_winners,
get_state_players, set_state_player, get_state_winner,
get_state_player, get_strategy): Add these methods to the twa_graph
class for convenience.
* NEWS, doc/org/tut.org: Mention tut40.org.
* doc/org/tut40.org: Add a documentation on how to use games in a
pratical case. In this example, we compute simulation using
games. Fixes#445.
* doc/Makefile.am: Add tut40.org.
* 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.
These occur when Spot is compiled with --enable-optimizations and
--disable-assert.
* spot/mc/unionfind.cc, spot/twaalgos/mealy_machine.cc,
spot/twaalgos/aiger.cc: Work around warnings about variables that are
only used in assert.
* spot/misc/common.hh [NDEBUG] (SPOT_ASSUME): Do not define
as assert() when it is disabled.
* spot/twaalgos/alternation.cc: Use insert instead of emplace
to work around a spurious possible nullptr dereference.
* spot/twaalgos/ltl2taa.cc, spot/twaalgos/ndfs_result.hxx,
spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc:
Work around spurious possible nullptr dereference.
* spot/twaalgos/sbacc.cc: Work around spurious "maybe uninitialized"
warning.
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
Split a LTL formula to a set of formula that don't share
output proposition. It allows to create multiple
strategies in ltlsynt.
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: here
* doc/spot.bib: Add reference
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
The only difference with upstream is that we keep std::malloc() as
malloc() to avoid issues with gnulib that sometimes redefine malloc to
rpl_malloc with a macro without defining std::rpl_malloc.
* spot/priv/robin_hood.hh, debian/copyright: Update.
* spot/priv/Makefile.am (update): Rename std::malloc to malloc.
* spot/parseaut/scanaut.ll: One or two digits numbers can be safely
converted to integer without risking overflow, so do that without
calling strtoul(). This simple change halves the number of calls
to strtoul() on the example automaton of issue #476.
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.
On a debug build with the automaton from #476, the gain seems to be
about 33% of the parsing time.
* spot/parseaut/parseaut.yy, spot/parseaut/parsedecl.hh,
spot/parseaut/scanaut.ll: Share a hash map of string->BDD
between the scanner and parser so that [labels] can be looked
up by the scanner if they have already been parsed once.
* NEWS: Mention it.
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.
On the example from previous patch, the number of instruction fetches
goes from 18490399159 down to 18248898077.
* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh (acd): Use
bitvect instead of std::vector<bool> in nodes. This make is easier to
update an edge of a bitvector shared by multiple nodes set after
pruning non-maximal sets from an SCC. Also compute the set of states
hit by the edges at the very end, once all nodes are known.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh,
spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Adjust to work with
bitvect as filter.
