1. 03 Dec, 2021 2 commits
  2. 02 Dec, 2021 2 commits
  3. 23 Nov, 2021 1 commit
  4. 22 Nov, 2021 2 commits
  5. 19 Nov, 2021 3 commits
  6. 18 Nov, 2021 5 commits
  7. 16 Nov, 2021 6 commits
  8. 15 Nov, 2021 1 commit
    • Alexandre Duret-Lutz's avatar
      ltsmin-pml: work around newer jupyter versions · 186d2063
      Alexandre Duret-Lutz authored
      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.
      186d2063
  9. 14 Nov, 2021 1 commit
  10. 13 Nov, 2021 4 commits
  11. 12 Nov, 2021 3 commits
  12. 11 Nov, 2021 2 commits
    • Philipp Schlehuber's avatar
      Renaming and clean up · 98ebbea1
      Philipp Schlehuber authored
      "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
      98ebbea1
    • Philipp Schlehuber's avatar
      Use generic split after obtaining direct strategy · 6ebe3d74
      Philipp Schlehuber authored
      * bin/ltlsynt.cc: Here
      6ebe3d74
  13. 10 Nov, 2021 2 commits
  14. 06 Nov, 2021 1 commit
    • Florian Renkin's avatar
      Notebooks: correct typos · d4967f20
      Florian Renkin authored
      * tests/python/acc_cond.ipynb, tests/python/contains.ipynb,
      tests/python/decompose.ipynb, tests/python/games.ipynb,
      tests/python/randltl.ipynb, tests/python/synthesis.ipynb,
      tests/python/testingaut.ipynb: here.
      d4967f20
  15. 05 Nov, 2021 5 commits