Skip to content
GitLab
  1. 10 Jul, 2019 2 commits
  3. 09 Jul, 2019 3 commits
  5. 05 Jul, 2019 2 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Fix some typos. · d244ff54
      Alexandre Duret-Lutz authored
      d244ff54
    • Alexandre Duret-Lutz's avatar
      deprecate spot::acc_cond::format() · bfe0ada6
      Alexandre Duret-Lutz authored 
      * NEWS: Mention it.
* spot/twa/acc.hh (spot::acc_cond::format): Deprecate.
(spot::acc_cond::mark_t::as_string): New function.
* spot/taalgos/dot.cc: Use mark_t::as_string().
* spot/priv/satcommon.cc, spot/priv/satcommon.hh,
spot/twaalgos/dtwasat.cc, spot/twaalgos/emptiness.cc,
tests/core/acc.cc, tests/core/acc.test: Adjust to use << directly.
      bfe0ada6
  7. 27 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      doc: add tut90.org about bdd_dict · ad2f5524
      Alexandre Duret-Lutz authored 
      Fixes #372.

* doc/org/tut90.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention it.
* python/spot/__init__.py: Allow make_twa_graph with
default bdd_dict.
      ad2f5524
  9. 21 Jun, 2019 1 commit
  11. 20 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      simulation: improve merging of transiant-SCCs · f3e57901
      Alexandre Duret-Lutz authored 
      * spot/twaalgos/simulation.cc: Code this.
* tests/core/det.test, tests/core/dra2dba.test,
tests/core/satmin.test, tests/core/sim3.test,
tests/python/decompose.ipynb, tests/python/dualize.py: Adjust test
cases.
* NEWS: Mention the optimization.
      f3e57901
  13. 18 Jun, 2019 3 commits
    • Alexandre Duret-Lutz's avatar
      toparity: revert symmetry-based optimization of LAR · c66b3d88
      Alexandre Duret-Lutz authored 
      Fixes #390.

* spot/twaalgos/toparity.cc: Revert the relevant part of 516e9536.
* tests/python/toparity.py: Add test case.
* NEWS: Mention the issue.
      c66b3d88
    • Alexandre Duret-Lutz's avatar
      gfguarantee: fix #357 again · 8df5f513
      Alexandre Duret-Lutz authored 
      The previous patch triggered this issue again, failing
core/ltl2tgba2.test.

* spot/twaalgos/gfguarantee.cc: Separate the replaying of history from
the modification of the automaton.
* NEWS: Mention the bug.
* tests/python/twagraph-internals.ipynb, tests/python/automata.ipynb:
Adjust.
      8df5f513
    • Alexandre Duret-Lutz's avatar
      simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f)) · da5d23f0
      Alexandre Duret-Lutz authored 
      These rules come from Delag's paper, and help some cases
in issue #385.

* spot/tl/simplify.cc: Implement the simplification.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/385.test: New file.
* tests/Makefile.am: Add it.
* tests/core/reduccmp.test: More tests.
* tests/core/ltl2tgba2.test: Adjust one improved case.
* tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
Adjust expected output, as the cnf/dnf reorder some subformulas.
      da5d23f0
  15. 12 Jun, 2019 4 commits
  17. 11 Jun, 2019 1 commit
  19. 07 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      genaut: introduce --m-nba · cba01232
      Alexandre Duret-Lutz authored 
      * bin/genaut.cc: Implement the --m-nba option.
* spot/gen/automata.hh, spot/gen/automata.cc: Add the generation code.
* NEWS, bin/man/genaut.x: Document it.
* doc/org/genaut.org: Update.
* tests/core/genaut.test, tests/core/parity2.test: Add some tests.
      cba01232
  21. 05 Jun, 2019 2 commits
  23. 04 Jun, 2019 4 commits
  25. 02 Jun, 2019 2 commits
  27. 28 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce output_aborter, and use it in ltlcross · a8504509
      Alexandre Duret-Lutz authored 
      * spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
output_aborter argument to abort if the output is too large.
* bin/ltlcross.cc: Use complement() with an output_aborter
so that ltlcross will not attempt to build complement larger
than 500 states or 5000 edges.  Add --determinize-max-states
and --determinize-max-edges options.
* tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/stutter-inv.ipynb: Adjust test cases.
* NEWS: Document this.
* bin/spot-x.cc: Add documentation for postprocessor's
det-max-states and det-max-edges arguments.
* doc/org/ltlcross.org: Update description.
      a8504509
  29. 19 May, 2019 1 commit
  31. 18 May, 2019 4 commits
  33. 06 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      implement SVA's first_match operator · 6fac0264
      Alexandre Duret-Lutz authored 
      * NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document it.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* spot/tl/formula.cc, spot/tl/formula.hh, spot/tl/dot.cc,
spot/tl/mutation.cc, spot/tl/print.cc, spot/tl/randomltl.cc,
spot/twaalgos/ltl2tgba_fm.cc: Adjust to support first_match.
* spot/tl/mark.cc, spot/tl/simplify.cc, spot/tl/snf.cc,
spot/tl/unabbrev.cc, spot/twa/formula2bdd.cc,
spot/twaalgos/ltl2taa.cc: Ignore it.
* tests/core/acc_word.test, tests/core/randpsl.test: Add more tests.
* tests/core/rand.test, tests/core/unambig.test,
tests/python/randltl.ipynb: Adjust.
* tests/python/formulas.ipynb: Show first_match.
      6fac0264
  35. 04 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      tl: add support for ##n and ##[i:j] from SVA · 60d488b3
      Alexandre Duret-Lutz authored 
      * spot/tl/formula.cc, spot/tl/formula.hh (formula::sugar_delay): New
function to implement this operator as syntactic sugar.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* doc/tl/tl.tex: Document the syntactic sugar rules and precedence.
* tests/core/sugar.test: Add tests.
* NEWS: Mention this new feature.
      60d488b3
  37. 27 Apr, 2019 2 commits
  39. 26 Apr, 2019 3 commits