1. 11 May, 2017 1 commit
  2. 10 May, 2017 1 commit
    • 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.
  3. 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.
  4. 04 May, 2017 1 commit
  5. 26 Apr, 2017 1 commit
  6. 19 Apr, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      sbacc: fix a serious bug · f02ca87f
      Alexandre Duret-Lutz authored
      Reported by Thibaud Michaud
      * spot/twaalgos/sbacc.cc: Do not label rejecting SCCs with the empty
      mark, as it might be accepting.
      * tests/core/sbacc.test: Add test cases.
      * NEWS: Mention the bug.
  7. 11 Apr, 2017 2 commits
  8. 07 Apr, 2017 5 commits
  9. 31 Mar, 2017 1 commit
    • 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.
  10. 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.
  11. 28 Mar, 2017 1 commit
  12. 22 Mar, 2017 2 commits
  13. 15 Mar, 2017 2 commits
  14. 10 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      emptiness checks: replace assert-preconditions by exceptions · d6d987bd
      Alexandre Duret-Lutz authored
      * spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc,
      spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance
      condition is not satisfied.
      * tests/python/misc-ec.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the change.
  15. 08 Mar, 2017 3 commits
  16. 07 Mar, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      twa_graph: more test coverage · cd4c326f
      Alexandre Duret-Lutz authored
      The goal is to improve coverage stats, but I discovered two issues
      while doing so.
      * tests/python/twagraph.py: New test case.
      * tests/Makefile.am: Add it.
      * spot/twa/twagraph.hh: Add fix typos in error messages.
      * python/spot/impl.i: Fix broken wrappers for state_from_number and
    • Alexandre Duret-Lutz's avatar
      twa_graph: fix set_univ_init_state() with initializer_list · 650bb7ed
      Alexandre Duret-Lutz authored
      Reported by Thomas Medioni.
      * spot/twa/twagraph.hh (set_univ_init_state): Remove the bogus
      template parameter.
      * tests/core/twagraph.cc, tests/core/tgbagraph.test: Test the method.
      * NEWS: Mention the bug.
  17. 03 Mar, 2017 4 commits
    • Alexandre Duret-Lutz's avatar
      monitor: fix -MD/-M difference in property output · 0621e0e9
      Alexandre Duret-Lutz authored
      Fixes #241.
      * spot/twaalgos/postproc.cc: Use the deterministic monitor if it
      has as many states as the non-deterministic one.
      * spot/twaalgos/minimize.cc (minimize_monitor): Quickly check
      for terminal automata.
      * spot/twaalgos/stripacc.cc: Set the weak property.
      * spot/twaalgos/stripacc.hh: Improve documentation.
      * tests/core/monitor.test, tests/core/sbacc.test: Update.
      * NEWS: Mention the issue.
    • Alexandre Duret-Lutz's avatar
      doc: add an example about how to build monitor in shell/python/C++ · 0df785bc
      Alexandre Duret-Lutz authored
      Part of #239.
      * doc/org/tut11.org: New file.
      * doc/org/ltl2tgba.org, doc/org/hierarchy.org: Add some anchors we can
      link to in tut11.org.
      * doc/org/tut.org, doc/Makefile.am: Add tut11.org.
      * NEWS: Mention the new page.
    • Alexandre Duret-Lutz's avatar
      postproc: fix monitor code · 9defdad2
      Alexandre Duret-Lutz authored
      Fixes #240.
      * spot/twaalgos/postproc.cc: Do not call do_simul on the output of
      minimize_monitor(), and do not skip complete() when PREF_==Any.
      * tests/core/monitor.test: Add a test case.
      * NEWS: Mention the bug.
      * doc/org/ltl2tgba.org: Document complete monitors.
    • Alexandre Duret-Lutz's avatar
      sbacc: fix a typo and remove some useless code · 57ea6d96
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sbacc.cc: Do not assign to one_in twice, and
      fix the value of init_acc.
      * tests/core/sbacc.test: Add a test case.
      * NEWS: Mention the bug.
  18. 02 Mar, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      remove options -! and -" from genltl · e826710c
      Alexandre Duret-Lutz authored
      Fixes #237.
      * bin/genltl.cc: Fix the numbering of options.
      * NEWS: Mention the bugs.
    • Alexandre Duret-Lutz's avatar
      add options to %x to list atomic propositions · dfe02f72
      Alexandre Duret-Lutz authored
      * bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc,
      bin/common_output.hh: Add options to %x to list atomic propositions
      with various quoting scheme.  Deprecate --format=%a in favor of the
      new --format=%x for consistency with --stats=%x.
      * tests/core/format.test, tests/core/remprop.test: Adjust and add more
      * NEWS: Mention these changes.
  19. 28 Feb, 2017 3 commits
  20. 20 Feb, 2017 2 commits
  21. 17 Feb, 2017 1 commit
  22. 16 Feb, 2017 2 commits
    • Arthur Remaud's avatar
      autfilt: Better display of cluster when universal edge loops in it · f7bbfd28
      Arthur Remaud authored
      Fixes #208
      * NEWS: Informations about the modifications
      * spot/twaalgos/dot.cc (print): Gestion of cluster for
      universal transitions
      * tests/core/alternating.test: tests added
      * tests/core/neverclaimread.test: tests changed for
      new dot format
      * tests/core/readsave.test: tests changed
      * tests/core/sccdot.test: tests changed
      * tests/python/_altscc.ipynb: tests changed
      * tests/python/decompose.ipynb: tests changed
    • Arthur Remaud's avatar
      autfilt: add option (y) to --dot to split universal transitions · 34859568
      Arthur Remaud authored
      Fixes #207
      * NEWS: Informations about the option 'y' for --dot added
      * bin/common_aoutput.cc: Documentation for the option 'y'
      for --dot added
      * spot/twaalgos/dot.cc (print_dst, process_link): Functions
      modified for the new option
      * tests/core/alternating.test: Tests added