1. 13 Jul, 2020 15 commits
    • Florian Renkin's avatar
      ltlsynt: Add more elements in csv · 8ac24acb
      Florian Renkin authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * bin/ltlsynt.cc: Add the number of states of the dpa
      and of the parity game in the csv.
    • Florian Renkin's avatar
      ltlsynt: Add -x option for translation · 7c09f64c
      Florian Renkin authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * bin/ltlsynt.cc: ltlsynt can use extra options for translator.
    • Alexandre Duret-Lutz's avatar
      work around diagnostic changes in Bison 3.6 · e06f8a3e
      Alexandre Duret-Lutz authored
      Bison <3.6 used to complain about "$undefined", while Bison >=3.6 now
      write "invalid token".
      * tests/core/parseaut.test, tests/core/parseerr.test,
      tests/core/sugar.test: Adjust expected diagnostics to match Bison pre
      and post 3.6.
    • Alexandre Duret-Lutz's avatar
      ltlsynt: add --algo=ps · 16540869
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc: Implement this.
      * tests/core/ltlsynt.test: Add a test case.
      * NEWS: Mention it.
    • Alexandre Duret-Lutz's avatar
      simplify_acc: perform unit-propagation earlier · b434ac7f
      Alexandre Duret-Lutz authored
      Closes #405.   This shows no difference on the test suite,
      but that is thanks to the previous patch: without it, an
      example in automata.ipynb would have an extra edge.
      * spot/twaalgos/cleanacc.cc (simplify_acceptance): Call
      unit_propagation() before simplify_complementary_marks_here() and
      fuse_marks_here(), because that is simpler to perform.
    • Alexandre Duret-Lutz's avatar
      remfin: do not clone transitions that are accepting in main · b762f542
      Alexandre Duret-Lutz authored
      * spot/twaalgos/remfin.cc (default_strategy): Detect transitions
      from the main copy that are completely accepting and that do not
      need to be repeated in the clones.
      * tests/python/remfin.py: Add a test case.
      * tests/core/ltl2dstar4.test: Improve expected results.
      * NEWS: Mention the change.
    • Alexandre Duret-Lutz's avatar
      improve fuse_marks_here by detecting more patterns · c005041e
      Alexandre Duret-Lutz authored
      This remove some restrictions that prevented fuse_marks_here from
      simplifying certain patterns, as noted in the first comment of
      issue #405.
      * spot/twaalgos/cleanacc.cc (find_interm_rec, find_fusable): Remove
      some unnecessary restrictions to singleton marks, and replace the hack
      put one non-singleton mark at the beginning of the singleton list by a
      * tests/python/simplacc.py: Add two test cases.
      * tests/python/automata.ipynb, tests/core/remfin.test: Improve
      expected results.
      * NEWS: Mention the bug.
    • Alexandre Duret-Lutz's avatar
      fixpool: allocate a new chunk on creation · ce695e67
      Alexandre Duret-Lutz authored
      Allocate the first chunk when the fixpool is created.  This avoid a
      undefined behavior reported in issue #413 without requiring an extra
      comparison in allocate().
      * spot/misc/fixpool.hh, spot/misc/fixpool.cc (new_chunk_): New method
      extracted from allocate().  Use it in the constructor as well.
      * NEWS: Mention the bug.
    • Alexandre Duret-Lutz's avatar
      postproc: option to wdba-minimize only when sure · 64aee87d
      Alexandre Duret-Lutz authored
      Fixes #15.
      * spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
      (minimize_obligation_garanteed_to_work): New function.
      * spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
      wdba-minimize=1.  Handle new default for wdba-minimize.
      * NEWS, bin/spot-x.cc: Document those changes.
      * tests/core/ltl2tgba2.test: Add some test cases.
      * tests/core/genltl.test: Improve expected results.
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      stats: speed up the computation of transitions · d25fcb23
      Alexandre Duret-Lutz authored
      Juraj Major reported a case with 32 APs where ltlcross would take
      forever to gather statistics.  It turns out that for each edge,
      twa_sub_statistics was enumerating all compatible assignments of 32
      APs.  This uses bdd_satcountset() instead, and also store the result
      in a long long to avoid overflows.
      * spot/twaalgos/stats.cc (twa_sub_statistics): Improve the code for
      counting transitions.
      * bin/common_aoutput.hh, bin/ltlcross.cc, spot/twaalgos/stats.hh:
      Store transition counts are long long.
      * tests/core/readsave.test: Add test case.
      * NEWS: Mention the bug.
    • Alexandre Duret-Lutz's avatar
      [buddy] avoid cache errors in bdd_satcount() and friends · 4608d9a5
      Alexandre Duret-Lutz authored
      * src/bddop.c (bdd_satcount, bdd_satcountln): If the number of
      declared variables changed since we last used it, reset misccache.
      Otherwise, bdd_satcount() and friends might return incorrect results
      after the number of variable is changed.  These is needed for the next
      patch in Spot to pass all tests.
      (misccache_varnum): New global variable to track that.
      (bdd_satcountset): Make sure that bdd_satcountset(bddtrue, bddtrue)
      return 1.0 and not 0.0.
    • Alexandre Duret-Lutz's avatar
      ltlsynt: make sure the previous Xor optimization actually works · fc1c17b9
      Alexandre Duret-Lutz authored
      * spot/tl/simplify.hh, spot/tl/simplify.cc,
      spot/twaalgos/translate.cc: Update the tl_simplification
      options after all preferences have been given.
      * bin/ltlsynt.cc: Display the size of the translation output.
      * tests/core/ltlsynt.test: Add test case.
    • Alexandre Duret-Lutz's avatar
      translate: improve handling of Xor and Equiv at top-level for -G -D · 6ec61504
      Alexandre Duret-Lutz authored
      * spot/tl/formula.hh: Add variant of formula::is that support 4
      * spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
      to preserve Xor and Equiv at the top-level.
      * spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
      Equiv for the -D -G case.
      * NEWS: Mention that.
      * tests/core/ltl2tgba2.test: Add test case.
      * tests/python/simstate.py: Adjust expected result.
    • Alexandre Duret-Lutz's avatar
      product: add product_xor() and product_xnor() · 822b7491
      Alexandre Duret-Lutz authored
      * spot/twaalgos/product.cc, spot/twaalgos/product.hh: Add those
      * tests/python/_product_weak.ipynb, tests/python/except.py: Test them.
      * NEWS: Mention them.
  2. 30 Apr, 2020 5 commits
  3. 29 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      dot: fix #393 · a7051b32
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Add support for option 'E', and default to
      rectangle nodes for large labels.
      * bin/common_aoutput.cc, NEWS: Document it.
      * tests/core/alternating.test, tests/core/dstar.test,
      tests/core/readsave.test, tests/core/sccdot.test,
      tests/core/tgbagraph.test, tests/python/_product_weak.ipynb,
      tests/python/alternation.ipynb, tests/python/atva16-fig2b.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/pdegen.py,
      tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb: Adjust all
      test cases.
    • Alexandre Duret-Lutz's avatar
      dot: fix #392 · 3ea63e9a
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Add tooltips to "..." states and edges.
      * tests/core/readsave.test: Test this.
      * tests/python/highlighting.ipynb: Adjust.
  4. 25 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      postproc: fix issue #402 · 67060420
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/translate.cc: Introduce a gen-reduce-parity option and
      use it on sub-automata built by ltl-split.
      * bin/spot-x.cc: Document it.
      * tests/core/ltl2tgba2.test: Add test case reported by Juraj Major.
    • Alexandre Duret-Lutz's avatar
      ltlsynt: fix lar.old implementation · fe340ae8
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc: Make sure to_parity_old() receive a deterministic
      automaton, for correctness.   Also call reduce_parity() afterward,
      to match what was done in 2.8.7.
      * tests/core/ltlsynt.test: Include lar.old in the comparison of all
      results to make sure it give the same result as the other 3
  5. 20 Apr, 2020 1 commit
  6. 19 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      avoid mark_t::count() when possible · cc12d514
      Alexandre Duret-Lutz authored
      count() may be implemented using a loop, so using it touch
      check count() == 1 or count() > 1 is not advisable.
      * spot/twa/acc.hh (mark_t::is_singleton, mark_t::has_many): Introduce
      these two methods to replace count()==1 and count()>1
      * spot/twa/acc.cc, spot/twaalgos/cleanacc.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/iscolored.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/toparity.cc: Adjust usage.
  7. 18 Apr, 2020 4 commits
  8. 17 Apr, 2020 7 commits
    • Alexandre Duret-Lutz's avatar
      to_parity: only call reduce_parity() when prefix_parity is enabled · fd0d752b
      Alexandre Duret-Lutz authored
      Calling reduce_parity() in to_parity() is confusing, because then
      running to_parity() on one SCC does not necessarily produce the same
      output as running to_parity() on the entire automaton.  However it is
      necessary for the implementation of parity_prefix.  As a compromise,
      disable reduce_parity() when parity_prefix is disabled, this way we
      can use that to demonstrate how the algorithm works.
      * spot/twaalgos/toparity.hh, spot/twaalgos/toparity.cc: Do not
      call reduce_parity() when parity_prefix is disabled.
      * tests/python/toparity.py: Adjust.
    • Alexandre Duret-Lutz's avatar
      simplify_acc: loop over the simplifications · 102ef043
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Run the
      simplifications in a loop until the condition does not change anymore.
      * tests/python/simplacc.py, tests/core/accsimpl.test,
      tests/core/remfin.test, tests/python/merge.py,
      tests/python/simplacc.py, tests/python/toparity.py: Update expected
      * tests/python/automata.ipynb: Update the failing example to a more
      interesting one, matching the one in doc/org/autfilt.org.
    • Alexandre Duret-Lutz's avatar
      simplify_acc: fix an infinite loop · b62e1bb1
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cleanacc.cc (fuse_mark_here): Fix incorrect cancelling
      of n-ary subterms, causing an invalid acceptance condition, and then
      an infinite loop.
      * tests/python/simplacc.py: Add test case.
    • Florian Renkin's avatar
      to_parity: Correct the expected number of states · 68012e6a
      Florian Renkin authored
      * tests/python/toparity.py: here.
    • Florian Renkin's avatar
      to_parity: Add an option to force degeneralization · 685d6d8b
      Florian Renkin authored
      * spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh:
      Don't try to run the algorithm without degeneralization
      with the option force_degen.
    • Florian Renkin's avatar
      to_parity: Remove merge_states · 527b62c5
      Florian Renkin authored
      * spot/twaalgos/toparity.cc: Remove merge_states.
      * tests/python/automata.ipynb, tests/python/toparity.py: Update tests.
    • Florian Renkin's avatar
      unit_propagation: Add a test with multiple unit clauses · 142f1afa
      Florian Renkin authored
      * tests/core/acc.cc, tests/core/acc.test: here.
  9. 16 Apr, 2020 2 commits