Monitors can now be split AND completed at the same time.
Split can be called on games without providing
"synthesis-outputs" - relying on named prop.
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Here
* tests/python/_synthesis.ipynb: Testing
* doc/org/concepts.org, NEWS: Document it.
* spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/sbacc.cc, spot/twaalgos/sbacc.hh: Use it.
* spot/twa/twagraph.cc: Update it on defrag.
* spot/twa/twa.cc (copy_named_properties_of): Copy it.
* tests/python/det.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i (get_original_states, get_original_classes): New
methods, to help with the tests.
Reported by Reuben Rowe.
* spot/twaalgos/complement.cc (complement): Remove the hard-coded
simul=0 option on automata with >32 states. In 2.10 simul=0 now
implies det-simul=0, causing the regression, and most importantly it
is not needed anymore, because we have other threashold like simul-max
and simul-trans-pruning in place.
* tests/core/complement.test: Add Reuben's automaton as test case.
* NEWS: Mention the fix.
This fixes#492, based on a report from Jérôme Dubois.
* spot/twaalgos/sbacc.cc: If the initial state is in a rejecting
component, start with an initial state whose colors are unsat_mark.
* tests/core/sbacc.test: Add test case.
* tests/python/pdegen.py: Adjust it.
Isomorph but different machines were created
depending on ARM vs Intel
* spot/twaalgos/mealy_machine.cc: Fix here
* tests/python/_synthesis.ipynb: Test here
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Solved game to mealy
now also supports the other mealy formats
* tests/python/_synthesis.ipynb: Test
* tests/Makefile.am: Test
* 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.
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
