1. 04 May, 2018 1 commit
  2. 03 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      improve gf_guarantee_to_ba · b0b431a5
      Alexandre Duret-Lutz authored
      * spot/twaalgos/gfguarantee.cc: Combine the last letter read
      with the first one of the next pass when doing transition-based
      acceptance.  Also move the initial states to the source of any
      accepting transition if the input is deterministic.
      * tests/core/ltl2tgba2.test, tests/core/satmin.test,
      tests/python/stutter-inv.ipynb: Reduce expected sizes of a few
      automata.
      b0b431a5
  3. 30 Apr, 2018 1 commit
    • Maximilien Colange's avatar
      ltlsynt: improve construction of turn-based games · 1fdc32f9
      Maximilien Colange authored
      Improve the way transitions are duplicated when preparing the turn-based
      game for synthesis. The resulting arena should now be deterministic on
      nodes owned by the environment. Also move the code to another file, so
      that it is easier to test (e.g. in Python).
      
      * bin/ltlsynt.cc: move the code
      * spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and
        implement the improvements
      * tests/Makefile.am, tests/python/split.py: test it
      * tests/core/ltlsynt.test: update existing tests to reflect the changes
      1fdc32f9
  4. 27 Apr, 2018 1 commit
  5. 23 Apr, 2018 4 commits
  6. 20 Apr, 2018 4 commits
  7. 15 Apr, 2018 2 commits
    • Alexandre Duret-Lutz's avatar
      is_unambiguous: fix false negatives again · 965ae855
      Alexandre Duret-Lutz authored
      Reported by Simon Jantsch and David Müller.
      
      * spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite wihtout assuming
      that the product of two accepting SCCs is accepting,  Also use
      the result of is_accepting_scc()/is_rejectng_scc() when available.
      * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Make it
      possible to check the acceptance of a unique SCC.
      * tests/core/unambig.test: Add more test cases.
      965ae855
    • Alexandre Duret-Lutz's avatar
      is_unambiguous: fix false negatives again · 2fe67769
      Alexandre Duret-Lutz authored
      Reported by Simon Jantsch and David Müller.
      
      * spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite wihtout assuming
      that the product of two accepting SCCs is accepting,  Also use
      the result of is_accepting_scc()/is_rejectng_scc() when available.
      * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Make it
      possible to check the acceptance of a unique SCC.
      * tests/core/unambig.test: Add more test cases.
      2fe67769
  8. 10 Apr, 2018 1 commit
  9. 09 Apr, 2018 4 commits
  10. 07 Apr, 2018 5 commits
    • Alexandre Duret-Lutz's avatar
      dot: name the digraph · 6cec4329
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Here.
      * NEWS: Mention the change.
      * tests/core/alternating.test, tests/core/det.test,
      tests/core/dstar.test, tests/core/monitor.test,
      tests/core/neverclaimread.test, tests/core/readsave.test,
      tests/core/sccdot.test, tests/core/tgbagraph.test,
      tests/python/_altscc.ipynb, tests/python/_autparserr.ipynb,
      tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
      tests/python/atva16-fig2b.ipynb, tests/python/automata-io.ipynb,
      tests/python/automata.ipynb, tests/python/decompose.ipynb,
      tests/python/gen.ipynb, tests/python/highlighting.ipynb,
      tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
      tests/python/parity.ipynb, tests/python/product.ipynb,
      tests/python/randaut.ipynb, tests/python/satmin.ipynb,
      tests/python/stutter-inv.ipynb, tests/python/testingaut.ipynb,
      tests/python/word.ipynb: Adjust test cases.
      6cec4329
    • Alexandre Duret-Lutz's avatar
      dot: use tooltips with option "1" · 2775b0ab
      Alexandre Duret-Lutz authored
      Fixes #327.
      
      * spot/twaalgos/dot.cc: Emit a tooltip="..." for state names and
      labels that are disabled by option "1".
      * doc/org/tut51.org, tests/python/product.ipynb, NEWS: Discuss this.
      * tests/core/readsave.test, tests/python/alternation.ipynb,
      tests/python/automata.ipynb: Adjust test cases.
      2775b0ab
    • Alexandre Duret-Lutz's avatar
      org: adjust to org-mode 9.1 · 99876048
      Alexandre Duret-Lutz authored
      This is needed so that SVG files are included as an <object...> rather
      than as an <img...>, which in turn is needed to ensure SVG tooltips
      will work.  We do not explicitly require org-mode 9.1, but we install
      it if it is not present.
      
      * HACKING: Mention the requirement.
      * doc/org/.dir-locals.el.in, doc/org/init.el.in, doc/org/spot.css:
      Adjust to org-mode 9.1.
      * doc/Makefile.am: Run emacs with the site-lisp libraries, in
      case it contains a more recent org-mode.
      * elisp/ob-dot.el: Delete, this was a work around older versions.
      * elisp/Makefile.am: Adjust.
      99876048
    • Alexandre Duret-Lutz's avatar
      org: fix broken links · 309eb0bb
      Alexandre Duret-Lutz authored
      * doc/org/upgrade2.org, doc/org/ioltl.org, doc/org/concepts.org: Here.
      * doc/org/tut51.org: Fix example output.
      309eb0bb
    • Alexandre Duret-Lutz's avatar
      gitlab-ci: skip org-mode in mingw builds · be9096a5
      Alexandre Duret-Lutz authored
      * .gitlab-ci.yml: Here.
      * doc/Makefile.am: Make sure the svg files are only rebuilt when org
      files are processed.
      be9096a5
  11. 03 Apr, 2018 2 commits
  12. 02 Apr, 2018 1 commit
  13. 30 Mar, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      sat_minimize: improve logs and document Python bindings · c766f58d
      Alexandre Duret-Lutz authored
      * spot/priv/satcommon.cc, spot/priv/satcommon.hh: Make it possible to
      set the log file without setting the environment variable.  Adjust
      print_log to take the input state and print it as a new column.
      * spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Adjust all
      calls to print_log.  Fix log output for incremental approaches.
      Prefer purge_unreachable_states() over stats_reachable().  Do
      not call scc_filter() on colored automata.
      * spot/twaalgos/dtwasat.hh: Document the new "log" option.
      * NEWS: Mention the changes.
      * tests/python/satmin.ipynb: New file.
      * tests/Makefile.am: Add it.
      * doc/org/satmin.org, doc/org/tut.org: Link to it.
      * doc/org/satmin.org, bin/man/spot-x.x: Adjust description
      of CSV files.
      * bench/dtgbasat/gen.py, bench/dtgbasat/tabl.pl,
      bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl,
      bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Adjust for
      the new column.
      * spot/misc/satsolver.cc, spot/misc/satsolver.hh (stats): Make it
      const.
      * python/spot/__init__.py (sat_minimize): Add display_log and
      return_log options.
      * tests/python/ipnbdoctest.py: Adjust to not compare SAT-minimization
      logs as they contain timings.
      c766f58d
  14. 29 Mar, 2018 1 commit
  15. 28 Mar, 2018 11 commits