1. 30 Dec, 2016 2 commits
  2. 29 Dec, 2016 9 commits
    • Alexandre Duret-Lutz's avatar
      support for semi-deterministic property · 4b013878
      Alexandre Duret-Lutz authored
      * spot/twa/twa.hh (prop_semi_deterministic): New methods.
      * spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the
      semi-deterministic property.
      * doc/org/concepts.org, doc/org/hoa.org: Document it.
      * spot/twaalgos/isdet.cc,
      spot/twaalgos/isdet.hh (is_semi_deterministic): New function.
      * bin/autfilt.cc: Add --is-semi-deterministic.
      * bin/common_aoutput.cc: Add --check=semi-deterministic.
      * tests/core/semidet.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/parseaut.test, tests/core/readsave.test: Adjust.
      4b013878
    • Alexandre Duret-Lutz's avatar
      twa_graph: add a merge_univ_dests() method · 12f6c8cf
      Alexandre Duret-Lutz authored
      and call it after parsing
      
      * spot/twa/twagraph.cc, spot/twa/twagraph.hh
      (twa_graph::merge_univ_dests): New method.
      * spot/parseaut/parseaut.yy: Call it.
      * spot/twaalgos/dot.cc: Improve output, now that
      several edges can use the same universal destination.
      * tests/core/alternating.test, tests/core/complete.test,
      tests/core/parseaut.test, tests/python/_altscc.ipynb,
      tests/python/alternating.py, tests/python/alternation.ipynb: Adjust
      test case.
      * doc/org/tut24.org: Adjust example.
      12f6c8cf
    • Alexandre Duret-Lutz's avatar
      remfin: call remove_alternation if needed · f5b261d8
      Alexandre Duret-Lutz authored
      * spot/twaalgos/remfin.cc: Here.
      * tests/core/alternating.test: Add a test case.
      f5b261d8
    • Alexandre Duret-Lutz's avatar
      complete: add support for alternating autamata · 071d819c
      Alexandre Duret-Lutz authored
      * spot/twaalgos/complete.cc: Do not use the initial
      state as a sink if it is universal.
      * tests/core/complete.test: Add a test case.
      071d819c
    • Alexandre Duret-Lutz's avatar
      postproc: preliminary support for alternating automata · f1b8d5f1
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc: Call remove_alternation().
      * tests/core/alternating.test: Additional test.
      f1b8d5f1
    • Alexandre Duret-Lutz's avatar
      twaalgos: add many guards against alternation · 9f6924cc
      Alexandre Duret-Lutz authored
      * spot/twa/twagraph.hh, spot/twaalgos/are_isomorphic.cc,
      spot/twaalgos/canonicalize.cc, spot/twaalgos/couvreurnew.cc,
      spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/isunamb.cc,
      spot/twaalgos/isweakscc.cc, spot/twaalgos/mask.hh,
      spot/twaalgos/minimize.cc, spot/twaalgos/product.cc,
      spot/twaalgos/randomize.cc, spot/twaalgos/sbacc.cc,
      spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc:
      Throw a runtime_error if the input is alternating.
      9f6924cc
    • Alexandre Duret-Lutz's avatar
      stats: add a variant for twa_graph_ptr · 543e0db9
      Alexandre Duret-Lutz authored
      This is faster than using the abstract interface, and it also supports
      alternating automata.  (This will be tested in the tests for
      ltlcross's support for alternating automata.)
      
      * spot/twaalgos/stats.cc (stats_reachable, sub_stats_reachable):
      Add code specific to twa_graph_ptr.
      543e0db9
    • Alexandre Duret-Lutz's avatar
      remfin: ignore unreachable states in remove_fin_weak() · 64fa6c00
      Alexandre Duret-Lutz authored
      * spot/twaalgos/remfin.cc (remove_fin_weak): Ignore unreachable
      states.  This caused crashes in the test cases for the
      upcoming alternation support in ltlcross.
      64fa6c00
    • Alexandre Duret-Lutz's avatar
      alternation: implement remove_alternation() for weak alt automata · fa06cfa3
      Alexandre Duret-Lutz authored
      This mixes the subset construction (for 1-state rejecting SCCs) and
      the breakpoint construction (for larger rejecting SCCs).  The
      algorithm should probably be rewritten in a cleaner and more efficient
      way, but that should do for a first version.  It should be easy to
      extend it to support Büchi acceptance (since the breakpoint
      construction works for this) when we need it.
      
      * spot/twaalgos/alternation.hh,
      spot/twaalgos/alternation.cc (remove_alternation): New function.
      * tests/python/alternation.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      fa06cfa3
  3. 27 Dec, 2016 6 commits
    • 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
    • Alexandre Duret-Lutz's avatar
      sccinfo: adjust to work with alternating automata · a4ce9994
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.cc: Consider universal edges as if they were
      existential edges.
      * spot/twaalgos/sccinfo.hh: Document that.
      * spot/twaalgos/dot.cc: Allow option 's' again, for easy testing.
      * tests/core/alternating.test: Adjust tests.
      * tests/python/_altscc.ipynb: New file (more tests).
      * tests/Makefile.am: Add it.
      a4ce9994
    • Alexandre Duret-Lutz's avatar
      alternation: add a states_and algorithm · 27ab631c
      Alexandre Duret-Lutz authored
      This should will come handy to implement the convertion from LTL to
      alternating automata, and to handle automata with multiple initial
      states.
      
      * spot/twaalgos/alternation.hh, spot/twaalgos/alternation.cc: New files.
      * spot/twaalgos/Makefile.am: Add them.
      * python/spot/impl.i: Add bindings.
      * tests/python/alternating.py: Test states_and.
      27ab631c
    • Alexandre Duret-Lutz's avatar
      twa_graph: add support for universal initial states · 48c812a5
      Alexandre Duret-Lutz authored
      The only missing point is that the HOA parser cannot deal with multiple
      universal initial states, as seen in parseaut.test.
      
      * spot/graph/graph.hh (new_univ_dests): New function, extracted from...
      (new_univ_edge): ... this one.
      * spot/twa/twagraph.hh (set_univ_init_state): Implement using
      new_univ_dests.
      * spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, python/spot/impl.i:
      Add support for universal initial states.
      * spot/parseaut/parseaut.yy: Add preliminary support for
      universal initial states.  Multiple universal initial states
      are still not supported.
      * tests/core/alternating.test, tests/core/parseaut.test,
      tests/python/alternating.py: Adjust tests and exercise this new feature.
      48c812a5
    • Alexandre Duret-Lutz's avatar
      dot: add support for alternating automata · d5c9c345
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Handle universal destinations.
      Ignore option 's' for alternating automata.
      * tests/core/alternating.test: New file.
      * tests/Makefile.am: Add it.
      d5c9c345
    • Alexandre Duret-Lutz's avatar
      print_hoa: add support for universal branches · 56df459c
      Alexandre Duret-Lutz authored
      * spot/twaalgos/hoa.cc: Implement it.
      * tests/python/alternating.py: Test it.
      56df459c
  4. 24 Dec, 2016 1 commit
  5. 16 Dec, 2016 1 commit
  6. 13 Dec, 2016 1 commit
    • Maximilien Colange's avatar
      Add a new, parameterized, version of the Couvreur emptiness check. · 1a08eca8
      Maximilien Colange authored
      This version has optimization for explicit twa, and also for weak and
      terminal (depending on whether an accepting run is requested) automata.
      
      * spot/twaalgos/couvreurnew.hh, spot/twaalgos/couvreurnew.cc,
        spot/twaalgos/Makefile.am: New files for the new algorithm.
      * spot/twaalgos/emptiness.cc, tests/core/randtgba.cc:
        Register new algorithm.
      1a08eca8
  7. 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
  8. 30 Nov, 2016 1 commit
  9. 29 Nov, 2016 1 commit
    • Maximilien Colange's avatar
      Automata with no state are no longer allowed. · b3ee6831
      Maximilien Colange authored
      * NEWS, spot/twa/twa.hh: Document the change.
      * spot/twa/twagraph.hh, spot/kripke/kripkegraph.hh:
        Add an exception in get_init_state_number().
        get_init_state() now calls get_init_state_number().
      * spot/twa/twagraph.cc, spot/twaalgos/simulation.cc,
        spot/twaalgos/powerset.cc, spot/twaalgos/complete.cc,
        spot/twaalgos/sccfilter.cc: Remove now useless tests.
      * spot/twaalgos/hoa.cc: Remove now useless comment.
      * spot/twaalgos/minimize.cc: Never return an automaton with no state.
      b3ee6831
  10. 28 Nov, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      strength: fix is_terminal() · 341eeb2b
      Alexandre Duret-Lutz authored
      Fix #198.  Reported by Maximilien Colange.
      
      * spot/twaalgos/strength.cc (is_terminal): Test that no accepting
      transition lead to a rejecting SCC.
      * tests/core/strength.test: Add test case.
      * spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org:
      Adjust documentation.
      * NEWS: Mention the fix.
      341eeb2b
    • Alexandre Duret-Lutz's avatar
      strength: fix is_terminal() · 9bc978a9
      Alexandre Duret-Lutz authored
      Fix #198.  Reported by Maximilien Colange.
      
      * spot/twaalgos/strength.cc (is_terminal): Test that no accepting
      transition lead to a rejecting SCC.
      * tests/core/strength.test: Add test case.
      * spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org:
      Adjust documentation.
      * NEWS: Mention the fix.
      9bc978a9
  11. 24 Nov, 2016 2 commits
  12. 23 Nov, 2016 1 commit
    • Etienne Renault's avatar
      Prefer emplace_back to push_back · 43ec36cd
      Etienne Renault authored
      * spot/graph/ngraph.hh, spot/ltsmin/ltsmin.cc,
      spot/misc/bitvect.hh, spot/misc/intvcomp.cc,
      spot/misc/satsolver.cc, spot/priv/weight.cc,
      spot/ta/taexplicit.cc, spot/taalgos/minimize.cc,
      spot/taalgos/reachiter.cc, spot/tl/exclusive.cc,
      spot/tl/formula.cc, spot/tl/formula.hh,
      spot/tl/mark.cc, spot/tl/mutation.cc,
      spot/tl/relabel.cc, spot/tl/remove_x.cc,
      spot/tl/simplify.cc, spot/twa/acc.cc,
      spot/twa/acc.hh, spot/twa/formula2bdd.cc,
      spot/twa/taatgba.cc, spot/twa/taatgba.hh,
      spot/twa/twa.hh, spot/twa/twagraph.cc,
      spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc,
      spot/twaalgos/compsusp.cc, spot/twaalgos/copy.cc,
      spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/emptiness.cc, spot/twaalgos/gv04.cc,
      spot/twaalgos/hoa.cc, spot/twaalgos/ltl2taa.cc,
      spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc,
      spot/twaalgos/mask.hh, spot/twaalgos/minimize.cc,
      spot/twaalgos/powerset.cc, spot/twaalgos/product.cc,
      spot/twaalgos/randomgraph.cc, spot/twaalgos/reachiter.cc,
      spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/sccfilter.cc, spot/twaalgos/se05.cc,
      spot/twaalgos/simulation.cc, spot/twaalgos/stutter.cc,
      spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc,
      spot/twaalgos/word.cc, tests/core/bitvect.cc: here.
      43ec36cd
  13. 11 Nov, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      scc_filter: preserve state names and highlighted states · 85f6e0e1
      Alexandre Duret-Lutz authored
      Suggested by Juraj Major.
      
      * spot/twaalgos/sccfilter.cc: Here.
      * tests/python/sccfilter.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the news.
      85f6e0e1
    • Alexandre Duret-Lutz's avatar
      remfin: fix handling of weak automata · a70589fe
      Alexandre Duret-Lutz authored
      * spot/twaalgos/remfin.cc: Do not add a sink states to deterministic
      weak automata, and actually apply the "weak" Fin-removal to any weak
      automaton.
      * tests/core/explprod.test: Add a test case for the previous patch,
      but that used to fail because of this bug.
      * NEWS: Mention the bug.
      a70589fe
  14. 09 Nov, 2016 1 commit
  15. 08 Nov, 2016 1 commit
    • Alexandre GBAGUIDI AISSE's avatar
      spot: Add %R, %[..]R common option. · 6ed38070
      Alexandre GBAGUIDI AISSE authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      For #189.
      
      * NEWS: Update.
      * bin/autfilt.cc: Replace stopwatch with process_timer.
      * bin/dstar2tgba.cc: Replace stopwatch with process_timer.
      * bin/ltl2tgba.cc: Replace stopwatch with process_timer.
      * bin/ltlcross.cc: Replace stopwatch with process_timer.
      * bin/ltldo.cc: Replace stopwatch with process_timer.
      * bin/randaut.cc: Replace stopwatch with process_timer.
      * bin/common_aoutput.hh: Implement process_timer, integrate it.
      * bin/common_aoutput.cc: Integrate process_timer and implement new
      print method.
      * spot/misc/timer.hh: Modify timer class and timeinfo struct
      i.e. add cutime (children_utime) and cstime (children_stime).
      * spot/misc/timer.cc: Help code to behave as before all this.
      * spot/twaalgos/dtbasat.cc: Help print_log to behave as before
      all this.
      * spot/twaalgos/dtwasat.cc: Help print_log to behave as before
      all this.
      * spot/misc/formater.hh: Add operator<< for spot::timer.
      6ed38070
  16. 01 Nov, 2016 2 commits
  17. 29 Oct, 2016 5 commits