1. 21 Jun, 2017 1 commit
    • Thomas Medioni's avatar
      streett_like: clear the pair vector when non Streett-like · fc609057
      Thomas Medioni authored
      When an acceptance condition is not Streett-like, is_streett_like
      now clears the rs_pair vector parameter before returning. Fixes #270.
      
      * spot/twa/acc.cc: Clear the pair vector.
      * spot/twaalgos/totgba.cc: Stop calling streett_to_generalized_buchi()
        when the acceptance condition is not Streett-like.
      fc609057
  2. 20 Jun, 2017 4 commits
  3. 19 Jun, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      doc: Jessie -> Stretch · 85e4cf51
      Alexandre Duret-Lutz authored
      * doc/org/install.org: Update.
      85e4cf51
    • Alexandre Duret-Lutz's avatar
      stats: fix slow %s and inappropriate %S output · 413d2d6a
      Alexandre Duret-Lutz authored
      Fixes #269.
      
      * spot/twaalgos/stats.cc: Use twa_statistics instead of
      twa_sub_statistics when %t is not used.
      * bin/common_aoutput.cc: Likewise, also fix %S to use twa_statistics
      instead of num_states(), and document that %s,%t,%e all return
      statistics about the reachable part of the automaton.
      * tests/core/format.test: Add more tests.
      * NEWS: Document the issue.
      413d2d6a
  4. 08 Jun, 2017 6 commits
  5. 07 Jun, 2017 4 commits
    • Alexandre Duret-Lutz's avatar
      libtool: surrender to Debian's castrated libtool · 1042a8da
      Alexandre Duret-Lutz authored
      The libtool version distributed by Debian is patched to *not* propagate
      dependencies (i.e., if libA depends on libB, then linking against libA
      will not automatically link against libB, it has to be explicit),
      contrary to what the Libtool manual document.  So now we explicitly
      link against both libA and libB in such case.
      
      * configure.ac: Remove the workaround that does not work for
      MinGW.
      * doc/org/compile.org: Mention the issue.
      * bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am,
      spot/gen/Makefile.am, doc/org/g++wrap.in: Make the dependencies
      explicit.
      1042a8da
    • Etienne Renault's avatar
      ikwiad: fix accepting run printing · 4de44b42
      Etienne Renault authored
      * tests/core/ikwiad.cc: here.
      4de44b42
    • Alexandre Duret-Lutz's avatar
      * AUTHORS: Add Henrich Lauko. · 0e039a36
      Alexandre Duret-Lutz authored
      0e039a36
    • Henrich Lauko's avatar
      remfin: Make removing of fins more modular. · 784681d8
      Henrich Lauko authored and Henrich Lauko's avatar Henrich Lauko committed
      * spot/twaalgos/remfin.cc: Refactore remove_fin implementation. Enable
      filtering of strategies used for fin removing.
      * spot/priv/enumflags.hh: Add support for enum flags from brick-types.
      * spot/priv/Makefile.am: Add enumflags.hh to make.
      * debian/copyright: Update copyright with bricks library license.
      784681d8
  6. 05 Jun, 2017 1 commit
  7. 03 Jun, 2017 1 commit
  8. 02 Jun, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      work around change in pandas 0.20 · dbcde8e3
      Alexandre Duret-Lutz authored
      * tests/core/ltlcross4.test: Replace describe() by agg() to work
      around a backward incompatible change in pandas 0.20.
      dbcde8e3
    • Alexandre Duret-Lutz's avatar
      simulation: do not depend on bdd numbers for ordering classes · 9ab4b840
      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
      report.
      * tests/core/complement.test, tests/core/det.test,
      tests/core/parseaut.test, tests/core/prodor.test, tests/core/scc.test,
      tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
      tests/python/decompose.ipynb, tests/python/decompose_scc.py,
      tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
      tests/python/sccinfo.py, tests/python/simstate.py,
      tests/python/testingaut.ipynb, tests/python/word.ipynb: Update
      test case for new order of states.
      9ab4b840
  9. 31 May, 2017 7 commits
    • Alexandre Duret-Lutz's avatar
      sanity: ensure that all environment variables are documented · 101c2533
      Alexandre Duret-Lutz authored
      * tests/sanity/getenv.test: New file.
      * tests/Makefile.am: Add it.
      * bin/man/spot-x.x: Document SPOT_STUTTER_CHECK and SPOT_DEBUG_PARSER.
      101c2533
    • Alexandre Duret-Lutz's avatar
      sanity: catch undocumented named properties · 93969758
      Alexandre Duret-Lutz authored
      * tests/sanity/namedprop.test: New file.
      * tests/Makefile.am: Add it.
      * doc/org/concepts.org: Add documentation for degen-levels and
      simulated-states.
      93969758
    • Alexandre Duret-Lutz's avatar
      dot: fix printing of alternating automata · 97f3efab
      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.
      97f3efab
    • Alexandre Duret-Lutz's avatar
      scc_info: keep track of common acceptance sets · 617a7187
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Do it.
      * tests/core/sccdot.test: Add a test case.
      * NEWS: Mention it.
      617a7187
    • Alexandre Duret-Lutz's avatar
      acc: add a maybe_accepting() method · 78add1d4
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh: Implement the new method, and
      use it to implement inf_accepting().
      * tests/python/accparse2.py: Add some tests.
      78add1d4
    • Maximilien Colange's avatar
      Degeneralization keeps track of levels. · f7d14ab5
      Maximilien Colange authored
      * NEWS: Document this.
      * spot/twa/twagraph.cc: `copy_state_names_from` handles this new info.
      * spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it.
      * tests/python/origstate.py, tests/python/simstate.py: Update tests to
        reflect the change.
      f7d14ab5
    • Maximilien Colange's avatar
      Simulation keeps track of simulated states in the input automaton. · 7b5ab545
      Maximilien Colange authored
      * NEWS: Document the change.
      * spot/twaalgos/simulation.cc: Implement the change.
      * spot/twa/twagraph.cc: `copy_state_names_from` uses simulated states
        info if present.
      * spot/twaalgos/determinize.cc: Pretty-print in determinization follows
        simulated states, avoiding possible confusion.
      * tests/Makefile.am, tests/python/simstate.py: Add a test.
      7b5ab545
  10. 30 May, 2017 2 commits
  11. 29 May, 2017 1 commit
    • Thomas Medioni's avatar
      rs_like: fix bug to accept Fin | Fin , Inf & Inf · 4da6a5cd
      Thomas Medioni authored
      co-Büchi is now recognized as Streett-like, Büchi as Rabin-like.
      Also recognized Inf & Inf & Inf... as Streett-like and
      Fin | Fin | Fin... as Rabin-like.
      
      * spot/twa/acc.cc: Fix the bug
      * tests/python/rs_like.py: Add some test case
      4da6a5cd
  12. 18 May, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: release all subformulas between runs · acdaaac4
      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.
      acdaaac4
  13. 11 May, 2017 4 commits
  14. 10 May, 2017 4 commits
    • Alexandre Duret-Lutz's avatar
      parseaut: misc cleanups · 866263ec
      Alexandre Duret-Lutz authored
      * spot/parseaut/parseaut.yy: Remove extra ;.
      * spot/parseaut/scanaut.ll: Use nullptr instead of 0.
      866263ec
    • 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.
      762dd455
    • 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.
      aa404823
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: clear simplification cache between translations · f07fbbae
      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.
      f07fbbae