1. 03 Jun, 2017 3 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      work around change in pandas 0.20 · 526b299d
      Alexandre Duret-Lutz authored
      * tests/core/ltlcross4.test: Replace describe() by agg() to work
      around a backward incompatible change in pandas 0.20.
    • Alexandre Duret-Lutz's avatar
      simulation: do not depend on bdd numbers for ordering classes · ae0e84ac
      Alexandre Duret-Lutz authored
      Fixes #262 again.  Reported by Maximilien Colange.
      * spot/twaalgos/simulation.cc: Use state numbers to order classes, not
      their signatures.  The problem was that even if two simulation of the
      same automaton assign the same signature, the BDD identifier used for
      that signature might be different, and therefore the ordering obtained
      by using BDDs as keys in a map can be different.  A side-effect of
      this change is that the order of states in automata produced by
      simulation-based reduction may change; many tests had to be updated.
      * tests/core/ltl2tgba.test: Add a new test case based on Maximilien's
      * tests/core/complement.test, tests/core/det.test,
      tests/core/parseaut.test, tests/core/prodor.test,
      tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
      tests/python/decompose.ipynb, tests/python/highlighting.ipynb,
      tests/python/piperead.ipynb, tests/python/testingaut.ipynb,
      tests/python/word.ipynb: Update test cases for new order of states.
  2. 02 Jun, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: fix printing of alternating automata · 7b6cfd44
      Alexandre Duret-Lutz authored
      Related to #208.
      * spot/twaalgos/dot.cc: Fix missing definitions of universal nodes,
      and inclusion of universal nodes inside of SCC when none of the
      destination comes back to the SCC.
      * tests/python/_altscc.ipynb: Adjust and add more test cases.
      * tests/core/alternating.test, tests/core/neverclaimread.test,
      tests/core/readsave.test, tests/core/sccdot.test,
      tests/python/decompose.ipynb: Adjust test cases.
      * NEWS: Mention the bug.
  3. 18 May, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: release all subformulas between runs · f6607f1a
      Alexandre Duret-Lutz authored
      Fixes #262, reported by Maximilien Colange.
      * bin/common_output.cc, bin/common_aoutput.cc, bin/common_aoutput.hh:
      Clear the set of atomic propositions if --stats=%[...]x was used.
      * spot/twa/bdddict.cc: Release any formula associated to a BDD when it
      is unregistered, do not wait for the dictionary's destruction.  This
      was the main culprit for #262.
      * tests/core/ltl2tgba.test: Add test cases.
      * NEWS: Mention the bug.
  4. 11 May, 2017 2 commits
  5. 10 May, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      parseaut: misc cleanups · 762dd455
      Alexandre Duret-Lutz authored
      * spot/parseaut/parseaut.yy: Remove extra ;.
      * spot/parseaut/scanaut.ll: Use nullptr instead of 0.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: clear simplification cache between translations · aa404823
      Alexandre Duret-Lutz authored
      The cache used in formula simplification will keep atomic propositions
      defined between several translations, and may impact variable order.
      Reported by Maximilien Colange.
      * spot/tl/simplify.hh, spot/tl/simplify.cc,
      spot/twaalgos/translate.cc, spot/twaalgos/translate.hh (clear_cache):
      New method.
      * bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call it.
      * spot/twaalgos/stats.cc: Do not keep a point to the formula after
      printing statistics.
      * tests/core/ltl2tgba.test: Add a test case.
      * tests/core/readsave.test: Adjust one formula.
      * NEWS: Mention the issue.
  6. 09 May, 2017 1 commit
  7. 08 May, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      simplify: fix related to event_univ handling · 8968bf6c
      Alexandre Duret-Lutz authored
      Fixes #260.  Reported by František Blahoudek.
      The simplification F(f)|q = F(f|q), where q designates an event_univ
      formula, was not always applied because of a couple of issue: (1) the
      mospliter was ignoring event_univ unless favor_event_univ was set, (2)
      when processing formulas from res_EventUniv they were not put back
      into res_F or res_G to be subject to the F/G rules.
      * spot/tl/simplify.cc: Improve handling of the above points.
      * tests/core/reduccmp.test: Adjust and add test case.
      * tests/core/ltl2tgba2.test, tests/python/atva16-fig2a.ipynb: Adjust.
  8. 05 May, 2017 1 commit
  9. 04 May, 2017 5 commits
  10. 26 Apr, 2017 3 commits
  11. 20 Apr, 2017 1 commit
  12. 19 Apr, 2017 3 commits
  13. 11 Apr, 2017 2 commits
  14. 08 Apr, 2017 1 commit
  15. 07 Apr, 2017 7 commits
  16. 31 Mar, 2017 4 commits
    • Thomas Medioni's avatar
      bench: fix stutter bench compiler errors. · 01ee4929
      Thomas Medioni authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * NEWS: mention this fix.
      * bench/stutter/stutter_bench.sh, bench/stutter/user.sh: Path to spot
        binaries would include an inexistant src directory.
      * bench/stutter/stutter_invariance_formulas.cc: Add override qualifier
        to satisfy -Wsuggest-override.
    • Alexandre Duret-Lutz's avatar
      various typos · 1ed6e518
      Alexandre Duret-Lutz authored
      * bench/dtgbasat/gen.py, spot/twaalgos/complement.hh: Fix
      looser->loser and lossing->losing.
      * tests/sanity/style.test: Catch 'an uni[^n]'.
      * spot/ta/ta.hh, spot/taalgos/tgba2ta.cc, spot/taalgos/tgba2ta.hh,
      spot/twa/twagraph.cc, spot/twaalgos/complement.hh,
      spot/twaalgos/sccinfo.cc: Fix various occurences of this pattern.
    • Alexandre Duret-Lutz's avatar
      [buddy] Typos in comments · b910330a
      Alexandre Duret-Lutz authored
      * src/kernel.c (bdd_addref): Fix typo documentation.
      * src/bddop.c (bdd_appall, bdd_appallcomp): Likewise.
    • Alexandre Duret-Lutz's avatar
      python: update some incorrect or obsolete code · f5d53e3a
      Alexandre Duret-Lutz authored
      * tests/python/ipnbdoctest.py: Use importlib instead of imp.
      * tests/python/ltlparse.py: Fix invalid escape sequence.
  17. 29 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      twa_graph: fix purge_unreachable_states on alternating automata · 6623af67
      Alexandre Duret-Lutz authored
      The algorithm had two problems: it was removing only useless
      destination from universal destination (instead of removing the entire
      edge), and it was not properly iterating over the entire reachable
      * spot/twa/twagraph.cc: Fix it.
      * spot/twa/twagraph.hh: Adjust documentation.
      * tests/core/alternating.test: Add more tests.
      * tests/python/twagraph.py: Adjust.
      * NEWS: Mention the bug.
  18. 28 Mar, 2017 1 commit