This massive set of changes was triggered by issue #546.
In addition to the better handling of !weak, this also adds some
weak properties in a few places.
* spot/twaalgos/product.cc (product_aux): Throw some exception
if an automaton with t or f acceptance has the !weak property. This
is a cheap sanity check to help detect algorithms that incorrectly
assumed !weak input would necessarily become !weak output.
* spot/twaalgos/hoa.cc (print_hoa): Likewise, also do not assume
that terminal implies very-weak.
* spot/parseaut/parseaut.yy: Add several diagnostics for similar
cases. E.g., a one-state automaton cannot be declared as !very-weak.
* tests/core/parseaut.test: Check those new diagnostics.
* spot/twa/twa.cc (twa::intersecting_run): Temporary remove the weak
property by setting it to maybe, not to false.
* spot/twaalgos/minimize.cc, spot/twaalgos/parity.cc,
spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc: Account for
the fact that these algorithm may in fact improve the weakness.
* spot/twaalgos/strength.cc: Only look at colors used by the
acceptance condition when deciding weakness.
* spot/twaalgos/synthesis.cc: Declare the strategy as weak.
* bin/randaut.cc: Add weak to automata with t/f acceptance.
* spot/kripke/kripke.hh: Make kripke structures as weak.
* tests/core/acc_word.test, tests/core/alternating.test,
tests/core/complement.test, tests/core/complete.test,
tests/core/ltlsynt.test, tests/core/randomize.test,
tests/core/readsave.test, tests/core/remfin.test,
tests/core/sccsimpl.test, tests/core/strength.test,
tests/core/wdba2.test, tests/ltsmin/kripke.test,
tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/dbranch.py, tests/python/highlighting.ipynb,
tests/python/kripke.py, tests/python/ltsmin-dve.ipynb,
tests/python/mealy.py, tests/python/simstate.py: Adjust all these test
cases.
* NEWS: Mention the fixes.
This implements the first point of issue #529.
* spot/tl/apcollect.cc, spot/tl/apcollect.hh (collect_litterals): New
function.
* bin/ltlsynt.cc: Implement the --polarity option, use
collect_litterals() to simplify the specification, finally patch the
game, Mealy, or Aiger output.
* spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Take a
relabeling_map has argument to specify extra APs.
* tests/core/ltlsynt.test, tests/core/ltlsynt2.test: Adjust test
cases.
* bin/ltlsynt.cc: Implement these options.
* bin/common_aoutput.hh, bin/common_aoutput.cc (automaton_format_opt):
Make extern.
* NEWS: Mention the new options.
* doc/org/ltlsynt.org: Use dot output in documentation.
* tests/core/ltlsynt.test: Quick test of the new options.
* NEWS: Mention those change.
* spot/twaalgos/game.hh (print_pg): New function.
(pg_print): Mark as deprecated.
* spot/twaalgos/game.cc (pg_print): Redirect to print_pg().
(print_pg): Update to output state names.
* python/spot/__init__.py: Teach to_str() about print_pg().
* bin/ltlsynt.cc: Adjust to call print_pg().
* tests/python/games.ipynb: Add an example.
* tests/core/ltlsynt.test: Adjust to remove the "INIT" note.
With a formula like G(b1) & (GFi <-> GF(b1)), a direct strategy was
created while it is unrealizable.
* spot/twaalgos/synthesis.cc: here.
* tests/core/ltlsynt.test: add tests
Reduce the amount of uncolored transitions
after split_2step by trying to color the env transitions.
This is currently only supported for parity like
acceptance conditions.
* spot/twaalgos/game.cc: Determinizatio of "colored"
game can created trivial self-loops. Fix them
* spot/twaalgos/synthesis.cc: Here
* tests/core/ltlsynt.test,
tests/python/_synthesis.ipynb,
tests/python/games.ipynb,
tests/python/synthesis.ipynb,
tests/python/synthesis.py: New and adjusted tests
Issue #500, reported by Yann Thierry-Mieg.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Use variant
to store a new pnode objects that delays the construction of n-ary
operators.
* spot/parsetl/Makefile.am: Do not distribute stack.hh anymore.
* spot/tl/formula.cc: Fix detection of overflow in Star and FStar.
* HACKING: Update Bison requirements to 3.3.
* tests/core/500.test: New test case.
* tests/Makefile.am: Add it.
* tests/core/ltl2tgba2.test, tests/core/ltlsynt.test,
tests/core/tostring.test: Adjust to new expected order.
* NEWS: Mention the change.
* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: generalize the
bypass and avoid to construct a strategy when we want realizability.
* bin/ltlsynt.cc: adapt for realizability
* tests/core/ltlsynt.test: update tests
* bin/ltlsynt.cc: Add "acd" to the list of possible paritization
algorithms used by ltlsynt
* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Add
ACD as paritisation algorithm
* tests/core/ltlsynt.test: add tests
* spot/twaalgos/synthesis.cc (ltl_to_game): In LAR and LAR_OLD mode,
for max odd and colorize the game after the split, not before. The
previous code used to colorize twice, and could waste up to 4 colors
in the process.
* tests/core/ltlsynt.test, tests/python/_mealy.ipynb,
tests/python/games.ipynb, tests/python/synthesis.ipynb,
tests/python/synthesis.py: Adjust all test cases to reflect the fact
that the game uses fewer colors.
* 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/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.
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.
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
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
* spot/twa/twagraph.cc: Implement it.
* spot/twa/twagraph.hh, NEWS: Document it.
* tests/python/mergedge.py: Test it.
* tests/core/ltlsynt.test, tests/python/games.ipynb: Adjust expectations.
Also have simul-max default to 4096 instead of 512, because it's
really simul-trans-pruning that is very slow and need to be limited.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/simulation.cc, spot/twaalgos/simulation.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh:
Implement the above options.
* bin/spot-x.cc, NEWS: Document them.
* tests/core/ltlsynt.test, tests/core/minusx.test,
tests/core/sim3.test: Add some test cases.
This fixes#452, and also fix a bug related to transiant SCCs
incorrectly merged in cosimulation: the source of the edges was
updated without fixing the chaining of the edges.
* spot/twaalgos/simulation.cc: Fix all the above.
* tests/python/simstate.py: Add test case from issue #452.
* tests/core/det.test, tests/core/ltlsynt.test,
tests/core/satmin.test: Lower expected sizes.
* tests/python/decompose.ipynb: Adjust for changed order.
Related to issue #298.
* spot/twaalgos/determinize.cc: Recognize braces that are temporary
to avoid emitting colors when they become empty.
* tests/python/298.py: New file, showing a reduction of colors.
* tests/Makefile.am: Add it.
* tests/core/ltlsynt.test: Adjust expected output (now smaller).
* tests/core/genltl.test: Adjust one expected output (now larger).
* NEWS: Mention the issue.
* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: New files
regrouping the functionnalities split and apply_strategy for synthesis
* python/spot/impl.i, spot/twaalgos/Makefile.am: Add them.
* spot/twaalgos/split.cc, spot/twaalgos/split.hh: No longer contains
the splits necessary for for synthesis, moved to
spot/twaalgos/synthesis.cc, spot/twaalgos/split.hh Split is now faster
and reduces the number of intermediate states, reducing the overall
size of the arena
* spot/misc/game.cc, spot/misc/game.hh: Renaming propagate_players to
alternate_players.
* tests/core/ltlsynt.test, tests/python/split.py: Update tests.
* bin/ltlsynt.cc: Adjust to new split. Swap order of split and
to_parity for lar.
* spot/misc/game.cc, spot/misc/game.hh: More efficient implementation
of Zielonka's algorithm to solve parity games. Now supports SCC
decomposition and efficient handling of certain special cases.
* doc/org/concepts.org: Document "strategy" and "state-winner"
properties.
* bin/ltlsynt.cc, tests/python/paritygame.ipynb: Adjust.
* tests/core/ltlsynt.test: Add more tests.
* spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Reimplement
print_aiger for speed gain, also heuristics to minimize the number
of gates as well as different encoding types have been added.
* bin/ltlsynt.cc: Make the new options for print-aiger available.
* tests/core/ltlsynt.test: Adjust tests.
* bin/ltlsynt.cc (complete_env): Replace this function by...
* spot/misc/game.hh, spot/misc/game.cc (propagate_players): ... this
new one, hiding the "state-player" business from ltlsynt. Also do not
create a sink states unless necessary.
* tests/core/ltlsynt.test: Adjust expected number of states.
