Newer Jupyter version are able to capture the system's stdout and
stderr to display it in the notebook. This is done asynchronously,
with a thread polling those file descriptor. While this will help us
debug (finaly we can see the tracing code we put in C++) this causes
two issues for testing. One is the asynchronous behaviour, which
makes it very hard to reproduce notebooks. The second issue is that
older version of Jupyter used to hide some of the prints from the
notebook, so it is hard to accommodate both.
In the case of the ltsmin-pml notebook, loading the PML file from
a filename used to trigger a compilation silently (with output on the
console, but not in the notebook). The newer version had the output
of that compilation spread into two cells.
* python/spot/ltsmin.i: Work around the issue by triggering the
compilation from Python, and capturing its output explicitly, so it
work with all Jupyter versions. Also adjust to use the more recent
and simpler subprocess.run() interface, available since Python 3.5.
* tests/python/ltsmin-pml.ipynb: Adjust expected output.
* tests/python/ipnbdoctest.py (canonicalize): Adjust patterns.
* 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
Fixes#480.
* bin/common_trans.cc (shorthands_ltl, shorthands_autproc): Write
those lists using regexes. Add entries for Owl 21.0.
(show_shorthands, tool_spec): Adjust to use those regexes.
* doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
Update the list of shorthands.
* tests/core/ltldo.test: Add a couple of tests.
* NEWS: Mention this new feature.
* 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.
* 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.
