* spot/parsetl/scantl.ll: Diagnose delays (##n) larger than
unbounded(). Remove all checks for delays with 1 or 2 characters.
* tests/core/parseerr.test: Add a test case.
* NEWS: Mention this fix.
* spot/kripke/kripkegraph.hh, spot/misc/hash.hh, spot/twa/taatgba.cc,
spot/twa/twagraph.hh, tests/core/ngraph.cc: Replace subtraction of
pointeur minus nullptr by an explicit cast to size_t.
* spot/twa/acc.hh: Add explicit default copy assignment operator for
rs_pair.
Reported by Yuri Victorovich, on FreeBSD.
* configure.ac: Test for them.
* spot/mc/mc_instanciator.hh: Only use them if they are present.
* NEWS: Mention the fix.
* spot/twaalgos/sbacc.cc (sbacc): Define the original-states
property on the created automaton.
* spot/twaalgos/sbacc.hh: Improve documentation.
* tests/python/sbacc.py: Update test cases.
For issue #485.
* spot/tl/formula.cc, spot/tl/formula.hh: Catch min/max overflow
when the operators are constructed. Also disable travial
simplification rules that would create such overflow.
For instance x[*200][*2] will not become x[*400] anymore.
* python/spot/impl.i: Catch std::overflow_error.
* tests/core/equals.test, tests/python/except.py: Add test cases.
* spot/twaalgos/mealy_machine.cc (is_split_mealy_specialization): Hide
spl in NDEBUG.
* spot/twaalgos/synthesis.cc (apply_strategy): sp is not always used.
* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc: Fix prototypes, as
well as several error messages.
* python/spot/impl.i: Implement an ad-hoc conversion for
std::vector<const_twa_graph_ptr>.
* tests/python/synthesis.ipynb: Use it to simplify the example.
Adjust some comments.
"Strategy" was used for mealy machines and game strategies a like.
Introduced the notion of mealy machine in three different flavors:
mealy machine: twa_graph with synthesis-outputs
separated mealy machine: mealy machine and all transitions
have conditions of the form (bdd over inputs)&(bdd over outputs)
split mealy machine: mealy machine that alternates between
env and player states. Needs state-players
* bin/ltlsynt.cc: renaming
* python/spot/impl.i: Add vector for const_twa_graph_ptr
* spot/twaalgos/aiger.cc,
spot/twaalgos/aiger.hh: Adapting functions
* spot/twaalgos/mealy_machine.cc,
spot/twaalgos/mealy_machine.hh: Add test functions and
propagate properties correctly. Adjust for names
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Removing unnecessary functions
and adapt to new names
* tests/python/aiger.py,
tests/python/_mealy.ipynb,
tests/python/mealy.py,
tests/python/synthesis.ipynb: Adjust
* spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh (parse_aag_impl_): Do
not display source filename in user facing errors. Use GNU-style
"file:line: " prefixes for locations. Adjust all sscanf() calls
to check for ignored trailing data. Add some missing checks about the
order of input and output names, checks that output names do no
intersect input names. Fix incorrect line number for unexpected
input variable number, and avoid using std::stoi as that throws
an std::invalid_argument on parse error.
* tests/python/aiger.py: Add test cases for each error message.
* spot/twaalgos/synthesis.cc: here
* spot/twaalgos/synthesis.hh: introduce a realizability_code
* bin/ltlsynt.cc, spot/twaalgos/aiger.cc: use this enum
* tests/core/ltlsynt.test: update tests
* spot/twaalgos/dot.cc: Improve the aiger printer by using a more
traditional dot syntax, indenting the output, adding some hard-coded
colors, fixing a bug in the negation of latch inputs, and rotating the
triangles for horizontal output.
* tests/python/synthesis.ipynb: Adjust expected output, and add
an example of horizontal layout.
* spot/twaalgos/dot.cc (print_dot): Add some detection of Mealy
machines, and some code to render its I/O in a <table>.
* tests/python/synthesis.ipynb: Adjust expected output.
* tests/python/_mealy.ipynb: New file.
* tests/Makefile.am: Add python/_mealy.ipynb.
* NEWS: Mention the new feature.
* 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.
* spot/twaalgos/game.hh, spot/twaalgos/synthesis.hh,
spot/twaalgos/aiger.hh: Declare new Doxygen groups for games and
synthesis.
* doc/spot.bib: Cleanup.
* 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.
* 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
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
