1. 19 Jan, 2017 1 commit
  2. 18 Jan, 2017 2 commits
  3. 16 Jan, 2017 1 commit
    • Alexandre GBAGUIDI AISSE's avatar
      TYPOS · 4eebe94a
      Alexandre GBAGUIDI AISSE authored
      * NEWS: typo.
      * bench/dtgbasat/config.bench: typo.
      * bench/dtgbasat/gen.py: typo.
      * bench/dtgbasat/stat-gen.sh: typo.
      * doc/org/concepts.org: typo.
      4eebe94a
  4. 14 Jan, 2017 4 commits
  5. 13 Jan, 2017 3 commits
  6. 12 Jan, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      org: some doc about the hierarchy · 8754cea2
      Alexandre Duret-Lutz authored
      * doc/org/hierarchy.org, doc/org/hierarchy.tex: New files.
      * doc/Makefile.am, doc/org/tools.org, NEWS: Add them.
      8754cea2
    • Alexandre Duret-Lutz's avatar
      minimize_wdba: fix handling of input with useless SCCs · c9918f64
      Alexandre Duret-Lutz authored
      * spot/twaalgos/minimize.cc (minimize_wdba): Diminish the color of
      terminal SCCs that are incomplete, as if they had a non-accepting
      sink as successor.
      * spot/twaalgos/strength.hh, spot/twaalgos/strength.cc
      (is_terminal_automaton): Add an option to ignore trivial SCC as we did
      before, since it matters for deciding membership to the guarantee
      class.
      (is_safety_mwdba): Rewrite as ...
      (is_safety_automaton): ... generalizating to any acceptance, and
      ignoring trivial SCCs.
      * bin/ltlfilt.cc, python/ajax/spotcgi.in, spot/tl/hierarchy.cc,
      tests/core/ikwiad.cc: Adjust usage of is_terminal_automaton and
      is_safety_automaton().
      * tests/core/hierarchy.test: Add a problematic formula as test-case.
      * NEWS: Mention the bug.
      c9918f64
  7. 10 Jan, 2017 3 commits
  8. 06 Jan, 2017 3 commits
  9. 30 Dec, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      twa: add prop_set::improve_det · 684c9c47
      Alexandre Duret-Lutz authored
      Algorithms that remove transitions can turn a non-deterministic
      automaton into a deterministic one, so we need to be able to specify
      that determinism can be improved (as opposed to preserved).
      
      * spot/twa/twa.hh (twa::prop_set::improve_det): New attribute.
      (twa::prop_keep, twa::prop_copy): Honor it.
      * spot/tl/exclusive.cc, spot/twaalgos/alternation.cc,
      spot/twaalgos/complete.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/mask.cc,
      spot/twaalgos/minimize.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc,
      spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc,
      spot/twaalgos/strength.cc, spot/twaalgos/stutter.cc,
      spot/twaalgos/totgba.cc: Adjust calls to prop_keep() and
      prop_copy().
      684c9c47
  10. 29 Dec, 2016 7 commits
  11. 27 Dec, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      twa: add support for very-weak property · 582d455c
      Alexandre Duret-Lutz authored
      * spot/twa/twa.hh: Implement the property.
      * spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input
      and output for it.
      * spot/twaalgos/strength.cc,
      spot/twaalgos/strength.hh (is_very_weak_automaton): New function.
      * tests/core/alternating.test: Add a test for --check=strength
      on an alternating automaton.
      * tests/core/strength.test, tests/core/parseaut.test: Adjust expected
      output.
      * NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it.
      582d455c
  12. 16 Dec, 2016 2 commits
  13. 15 Dec, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      spotcgi: correctly kill ltl3ba on timeout · 38fdb40e
      Alexandre Duret-Lutz authored
      * python/spot/__init__.py (automata): Do not create a session for
      every command, this is only needed if automata() is run with a timeout
      parameter.
      * python/ajax/spotcgi.in: Adjust exclude the main process from
      the process group, so that only children are killed on SIGALRM.
      * NEWS: Mention the bug.
      38fdb40e
    • Alexandre Duret-Lutz's avatar
      spotcgi: correctly kill ltl3ba on timeout · cd348275
      Alexandre Duret-Lutz authored
      * python/spot/__init__.py (automata): Do not create a session for
      every command, this is only needed if automata() is run with a timeout
      parameter.
      * python/ajax/spotcgi.in: Adjust exclude the main process from
      the process group, so that only children are killed on SIGALRM.
      * NEWS: Mention the bug.
      cd348275
  14. 14 Dec, 2016 1 commit
  15. 13 Dec, 2016 2 commits
  16. 10 Dec, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlf: ensure alive holds initially · 15709084
      Alexandre Duret-Lutz authored
      Reported by Shufang Zhu.
      
      * spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion
      and update the comments.
      * tests/core/ltlfilt.test: Adjust test cases.
      * NEWS: Mention the fix.
      * THANKS: Add Shufang Zhu.
      15709084
  17. 09 Dec, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlf: ensure alive holds initially · 413eab1d
      Alexandre Duret-Lutz authored
      Reported by Shufang Zhu.
      
      * spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion
      and update the comments.
      * tests/core/ltlfilt.test: Adjust test cases.
      * NEWS: Mention the fix.
      * THANKS: Add Shufang Zhu.
      413eab1d
  18. 02 Dec, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      install back the safety check of includes.test · 7824005d
      Alexandre Duret-Lutz authored
      Compilation of each header file alone, as a safety check, was removed
      when introducing "#pragma once" because we did not have to check for
      possible double inclusion.  However we still need to compile each
      header to make sure they are self-contained.
      
      * tests/sanity/includes.test: Compile each header.
      * tests/run.in: Export various compiler and directory flags.
      * spot/twaalgos/emptiness_stats.hh, spot/misc/mspool.hh,
      spot/misc/fixpool.hh: Include <spot/misc/common.hh>.
      * spot/misc/common.hh: Include <cassert>.
      * NEWS: Mention the fixed headers.
      7824005d
    • Alexandre Duret-Lutz's avatar
      install back the safety check of includes.test · 0ab8dc06
      Alexandre Duret-Lutz authored
      Compilation of each header file alone, as a safety check, was removed
      when introducing "#pragma once" because we did not have to check for
      possible double inclusion.  However we still need to compile each
      header to make sure they are self-contained.
      
      * tests/sanity/includes.test: Compile each header.
      * tests/run.in: Export various compiler and directory flags.
      * spot/twaalgos/emptiness_stats.hh, spot/misc/mspool.hh,
      spot/misc/fixpool.hh: Include <spot/misc/common.hh>.
      * spot/misc/common.hh: Include <cassert>.
      * NEWS: Mention the fixed headers.
      0ab8dc06
  19. 01 Dec, 2016 1 commit