1. 27 Dec, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      move spot/bin/ and spot/tests/ up by one level · 134dfc73
      Alexandre Duret-Lutz authored
      * spot/bin/: Move...
      * bin/: ... here.
      * spot/tests/: Move...
      * tests/: ... here.
      * Makefile.am, README, bench/stutter/Makefile.am,
      bench/stutter/stutter_invariance_formulas.cc, doc/Makefile.am,
      configure.ac, debian/rules, spot/Makefile.am, spot/ltsmin/Makefile.am,
      spot/ltsmin/kripke.test, spot/sanity/style.test, python/tests/run.in:
      Adjust.
      134dfc73
  2. 04 Dec, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      rename src/ as spot/ and use include <spot/...> · f120dd32
      Alexandre Duret-Lutz authored
      * NEWS: Mention the change.
      * src/: Rename as ...
      * spot/: ... this, adjust all headers to include <spot/...> instead of
      "...", and adjust all Makefile.am to search headers from the top-level
      directory.
      * HACKING: Add conventions about #include.
      * spot/sanity/style.test: Add a few more grep to catch cases
      that do not follow these conventions.
      * .gitignore, Makefile.am, README, bench/stutter/Makefile.am,
      bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
      debian/rules, doc/Doxyfile.in, doc/Makefile.am,
      doc/org/.dir-locals.el.in, doc/org/g++wrap.in, doc/org/init.el.in,
      doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
      doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
      doc/org/tut22.org, doc/org/tut30.org, iface/ltsmin/Makefile.am,
      iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc,
      iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc,
      wrap/python/Makefile.am, wrap/python/ajax/spotcgi.in,
      wrap/python/spot_impl.i, wrap/python/tests/ltl2tgba.py,
      wrap/python/tests/randgen.py, wrap/python/tests/run.in: Adjust.
      f120dd32
  3. 28 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      rewrite explicit Kripke structures and their parser · afbaa54d
      Alexandre Duret-Lutz authored
      Fixes #4 and fixes #5.
      
      * NEWS: Mention the change.
      * src/kripkeparse/: Delete.
      * README, src/Makefile.am, configure.ac: Adjust.
      * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: Delete.
      * src/kripke/kripkegraph.hh: New file.
      * src/kripke/Makefile.am: Adjust.
      * src/parseaut/parseaut.yy, src/parseaut/public.hh: Add
      an option to read kripke structures.
      * src/tests/bad_parsing.test: Delete.
      * src/tests/Makefile.am: Adjust.
      * src/tests/kripke.test, src/tests/parse_print_test.cc: Rewrite.
      * src/tests/ikwiad.cc, src/tests/parseaut.test,
      iface/ltsmin/modelcheck.cc, wrap/python/spot_impl.i: Adjust.
      afbaa54d
  4. 07 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      Add support for --check=strength · 3428fb32
      Alexandre Duret-Lutz authored
      * src/twaalgos/strength.cc, src/twaalgos/strength.hh (check_strength):
      New function.
      * src/bin/common_aoutput.cc: Add --check=strength.
      * src/tests/strength.test: New file.
      * src/tests/Makefile.am: Add it.
      * doc/org/hoa.org, NEWS: Document it.
      3428fb32
  5. 15 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: implement --complement · 2ae1b6a6
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Add option --complete.
      * src/twaalgos/complete.cc: Better handling of 0-edge automata.
      * src/tests/complement.test: New file.
      * src/tests/Makefile.am: Add it.
      2ae1b6a6
  6. 26 Sep, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      product: add a product_or variant · 51a3cfce
      Alexandre Duret-Lutz authored
      * src/twaalgos/product.cc, src/twaalgos/product.hh: Implement
      the variance.
      * src/bin/autfilt.cc: Expose it.
      * src/tests/prodor.test: New file.
      * src/tests/Makefile.am: Add it.
      * NEWS: Mention it.
      51a3cfce
  7. 20 Aug, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      remove algorithms that where only used by dstar's dra2ba conversion · 62f5b976
      Alexandre Duret-Lutz authored
      Since we just removed that conversion, those can go as well.  Yay!
      
      * src/tests/kv.test, src/twa/twamask.cc,
      src/twa/twamask.hh, src/twa/twaproxy.cc,
      src/twa/twaproxy.hh, src/twaalgos/scc.cc,
      src/twaalgos/scc.hh: Delete.
      * src/twaalgos/Makefile.am, src/twa/Makefile.am,
      src/tests/Makefile.am, src/tests/ikwiad.cc: adjust.
      62f5b976
  8. 17 Aug, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      merge tunnabrev/lunnabrev/wmunabbrev into a single function · d1f915c7
      Alexandre Duret-Lutz authored
      * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh: Delete.
      * src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: New files.
      * src/ltlvisit/Makefile.am: Adjust.
      * src/ltlvisit/print.cc, src/tests/equalsf.cc, src/tests/Makefile.am,
      src/twaalgos/ltl2taa.cc, wrap/python/spot_impl.i, src/bin/ltlfilt.cc:
      Adjust callers.
      * src/ltlvisit/contain.cc, src/tests/syntimpl.cc: Remove useless
      include.
      * wrap/python/tests/formulas.ipynb: New test cases.
      * doc/tl/tl.tex: Group all rules in a single section.
      * NEWS: Mention it.
      d1f915c7
  9. 10 Jul, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      new conversion for Streett->GBA · d8a1dafa
      Alexandre Duret-Lutz authored
      * src/twaalgos/totgba.hh, src/twaalgos/totgba.cc: Implement
      the new function.
      * NEWS: Mention this new function.
      * src/bin/man/spot-x.x: Document SPOT_STREETT_CONV_MIN.
      * src/tests/ltl2dstar4.test: Add tests.
      * src/tests/Makefile.am: Add it.
      * src/bin/autfilt.cc: Do do call remove_fin explicitely
      when --tgba is used, let the postprocessor do it.
      * src/twa/acc.hh: Add shift operators for acceptance marks.
      * src/twaalgos/remfin.cc: Use the new algorithm.
      * src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Add
      a new method to supply the acceptance sets visited by an SCC.
      d8a1dafa
  10. 15 Jun, 2015 1 commit
  11. 12 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      Rename src/tests/ltl2tgba as src/tests/ikwiad. · 17dc2f86
      Alexandre Duret-Lutz authored
      Fixes #23.
      
      * src/tests/ltl2tgba.cc: Rename as ...
      * src/tests/ikwiad.cc: ... this.
      * src/tests/Makefile.am, src/tests/babiak.test, src/tests/checkta.cc,
      src/tests/complementation.test, src/tests/cycles.test,
      src/tests/dbacomp.test, src/tests/degendet.test,
      src/tests/degenid.test, src/tests/det.test, src/tests/dfs.test,
      src/tests/dstar.test, src/tests/dupexp.test, src/tests/emptchke.test,
      src/tests/kv.test, src/tests/ltl2neverclaim-lbtt.test,
      src/tests/ltl2neverclaim.test, src/tests/ltl2tgba.test,
      src/tests/ltlcounter.test, src/tests/ltlcross.test,
      src/tests/neverclaimread.test, src/tests/obligation.test,
      src/tests/parseaut.test, src/tests/randaut.test,
      src/tests/randpsl.test, src/tests/renault.test,
      src/tests/satmin2.test, src/tests/sccsimpl.test, src/tests/sim2.test,
      src/tests/simdet.test, src/tests/spotlbtt.test, src/tests/wdba.test,
      src/tests/wdba2.test, bench/emptchk/README, bench/emptchk/defs.in,
      bench/ltlclasses/run, bench/ltlcounter/run, bench/wdba/run: Adjust.
      17dc2f86
  12. 11 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      hoaparse: rename to parseaut · a86391ab
      Alexandre Duret-Lutz authored
      Because this parser is not specific to HOA anymore.
      
      * src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
      src/hoaparse/hoaparse.yy, src/hoaparse/parsedecl.hh,
      src/parseaut/public.hh, src/hoaparse/hoascan.ll,
      src/tests/hoaparse.test: Rename to...
      * src/parseaut/Makefile.am, src/parseaut/fmterror.cc,
      src/parseaut/parseaut.yy, src/parseaut/parsedecl.hh,
      src/hoaparse/public.hh, src/parseaut/scanaut.ll,
      src/tests/parseaut.test: ... these, and also adjust the name internally.
      For instance hoa_aut_ptr is now parsed_aut_ptr; hoa_stream_parser is now
      automaton_stream_parser, and hoa_parse() has become parse_aut().
      * NEWS, README, configure.ac, doc/org/tut20.org, src/Makefile.am,
      src/bin/autfilt.cc, src/bin/common_aoutput.cc,
      src/bin/common_aoutput.hh, src/bin/common_conv.cc,
      src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/Makefile.am,
      src/tests/complementation.cc, src/tests/ltl2tgba.cc,
      src/tests/readsave.test, wrap/python/ajax/spot.in,
      wrap/python/spot.py, wrap/python/spot_impl.i,
      wrap/python/tests/automata-io.ipynb, wrap/python/tests/parsetgba.py:
      Adjust.
      a86391ab
  13. 14 May, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      simulation: work on TωA · 80808133
      Alexandre Duret-Lutz authored
      * src/twaalgos/simulation.cc, src/twaalgos/simulation.hh: Adjust
      to work on TωA.  This only require separate acceptance sets.
      * src/tests/sim3.test: New test.
      * src/tests/Makefile.am: Add it.
      80808133
    • Alexandre Duret-Lutz's avatar
      autfilt: new --separate-sets option · 3d1ccdc4
      Alexandre Duret-Lutz authored
      * src/twaalgos/sepsets.cc, src/twaalgos/sepsets.hh: New files.
      * src/twaalgos/Makefile.am: Add them.
      * src/twa/acc.hh (get_acceptance): Add a non-const version.
      * src/bin/autfilt.cc: Add the --separate-sets option.
      * src/tests/sepsets.test: New file.
      * src/tests/Makefile.am: Add it.
      3d1ccdc4
  14. 12 May, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      Add an is_unambiguous() function, use it in ltlcross and autfilt · 98de84f3
      Alexandre Duret-Lutz authored
      * src/twaalgos/isunamb.hh, src/twaalgos/isunamb.cc: New files.
      * src/twaalgos/Makefile.am: Add them.
      * src/tests/unambig.test: New file.
      * src/tests/Makefile.am: Add it.
      * src/bin/ltlcross.cc: Record whether each produced automaton is
      ambiguous.
      * src/bin/autfilt.cc: Add a --is-unambiguous option.
      * NEWS: Mention it.
      98de84f3
  15. 05 May, 2015 1 commit
  16. 24 Apr, 2015 3 commits
    • Etienne Renault's avatar
      Merge kripketest, graphtest and ltltest into tests · 66bd8f34
      Etienne Renault authored
      * README, configure.ac, iface/ltsmin/Makefile.am,
      src/tests/defs.in, src/tests/.gitignore, src/tests/Makefile.am,
      src/Makefile.am: update references.
      * src/kripketest/.gitignore, src/kripketest/Makefile.am,
      src/kripketest/defs.in, src/graphtest/.gitignore,
      src/graphtest/Makefile.am,
      src/graphtest/defs.in, src/ltltest/.cvsignore,
      src/ltltest/.gitignore, src/ltltest/Makefile.am,
      src/ltltest/defs.in:: remove files.
      * src/kripketest/bad_parsing.test, src/kripketest/kripke.test,
      src/kripketest/origin, src/kripketest/parse_print_test.cc,
      src/ltltest/bare.test, src/ltltest/consterm.cc,
      src/ltltest/consterm.test, src/tests/defs.in,
      src/ltltest/equals.test, src/ltltest/equalsf.cc,
      src/ltltest/eventuniv.test, src/ltltest/exclusive-ltl.test,
      src/graphtest/graph.cc, src/graphtest/graph.test,
      src/ltltest/isop.test, src/ltltest/kind.cc,
      src/ltltest/kind.test, src/ltltest/latex.test,
      src/ltltest/lbt.test, src/ltltest/length.cc,
      src/ltltest/length.test, src/ltltest/lenient.test,
      src/ltltest/ltlcrossgrind.test, src/ltltest/ltlfilt.test,
      src/ltltest/ltlgrind.test, src/ltltest/ltlrel.cc,
      src/ltltest/ltlrel.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/graphtest/ngraph.cc,
      src/graphtest/ngraph.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/rand.test,
      src/ltltest/readltl.cc, src/ltltest/reduc.cc,
      src/ltltest/reduc.test, src/ltltest/reduc0.test,
      src/ltltest/reduccmp.test, src/ltltest/reducpsl.test,
      src/ltltest/remove_x.test, src/ltltest/stutter-ltl.test,
      src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test,
      src/graphtest/tgbagraph.test, src/ltltest/tostring.cc,
      src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test, src/graphtest/twagraph.cc,
      src/ltltest/unabbrevwm.test,src/ltltest/utf8.test,
      src/ltltest/uwrm.test: rename as...
      * src/tests/bad_parsing.test, src/tests/kripke.test,
      src/tests/origin, src/tests/parse_print_test.cc,
      src/tests/bare.test, src/tests/consterm.cc,
      src/tests/consterm.test, src/tests/equals.test,
      src/tests/equalsf.cc, src/tests/eventuniv.test,
      src/tests/exclusive-ltl.test, src/tests/graph.cc,
      src/tests/graph.test, src/tests/isop.test,
      src/tests/kind.cc, src/tests/kind.test,
      src/tests/latex.test, src/tests/lbt.test,
      src/tests/length.cc, src/tests/length.test,
      src/tests/lenient.test, src/tests/ltlcrossgrind.test,
      src/tests/ltlfilt.test, src/tests/ltlgrind.test,
      src/tests/ltlrel.cc, src/tests/ltlrel.test,
      src/tests/lunabbrev.test, src/tests/nenoform.test,
      src/tests/ngraph.cc, src/tests/ngraph.test,
      src/tests/parse.test, src/tests/parseerr.test,
      src/tests/rand.test, src/tests/readltl.cc,
      src/tests/reduc.cc, src/tests/reduc.test,
      src/tests/reduc0.test, src/tests/reduccmp.test,
      src/tests/reducpsl.test, src/tests/remove_x.test,
      src/tests/stutter-ltl.test, src/tests/syntimpl.cc,
      src/tests/syntimpl.test, src/tests/tgbagraph.test,
      src/tests/tostring.cc, src/tests/tostring.test,
      src/tests/tunabbrev.test, src/tests/tunenoform.test,
      src/tests/twagraph.cc, src/tests/unabbrevwm.test,
      src/tests/utf8.test, src/tests/uwrm.test: ...these!
      66bd8f34
    • Etienne Renault's avatar
      Rename tgbatest into tests. · bd57f7a9
      Etienne Renault authored
      * src/Makefile.am, README, configure.ac: update references.
      * src/tgbatest/: rename as...
      * src/tests/: ...this!
      bd57f7a9
    • Etienne Renault's avatar
      Ensure that all tests have different names. · 8c4a3c01
      Etienne Renault authored
      * src/ltltest/Makefile.am, src/tgbatest/Makefile.am: update references.
      * src/ltltest/exclusive.test, src/ltltest/stutter.test,
      src/tgbatest/exclusive.test, src/tgbatest/stutter.test: rename as...
      * src/ltltest/exclusive-ltl.test, src/ltltest/stutter-ltl.test,
      src/tgbatest/exclusive-tgba.test,
      src/tgbatest/stutter-tgba.test: ...these
      8c4a3c01
  17. 25 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      complete: Fix completion of automata using Fin-acceptance · 23bcbb5b
      Alexandre Duret-Lutz authored
      * src/tgba/acc.cc, src/tgba/acc.hh: Add a way to extract
      an unstatisfiable mark, and fix the eval() function for
      Fin acceptance.
      * src/tgbaalgos/complete.cc: Label the sink state using
      an unsatisfiable mark.  Do not assume generalized Büchi.
      * src/tgbatest/complete.test: New test.
      * src/tgbatest/Makefile.am: Add it.
      23bcbb5b
  18. 24 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: add a --remove-ap option · 4553ac06
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/remprop.cc, src/tgbaalgos/remprop.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatest/remprop.test: New test.
      * src/tgbatest/Makefile.am: Add it.
      * src/bin/autfilt.cc: Implement the option.
      * doc/org/autfilt.org: Document it.
      4553ac06
  19. 23 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: add a --exclusive-ap option · fb7b7a94
      Alexandre Duret-Lutz authored
      * src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh: Implement
      constrain() for automata.
      * src/bin/autfilt.cc: Add --exclusive-ap option.
      * src/tgba/bdddict.cc, src/tgba/bdddict.hh: Add a
      has_registered_proposition() method.
      * src/tgbatest/exclusive.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      fb7b7a94
  20. 03 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      sccinfo: introduce is_rejecting() · ebe4ffc5
      Alexandre Duret-Lutz authored
      Because scc_info does not perform a full emptiness check, it is not
      always able to tell whether an SCC is accepting if the acceptance
      condition use Fin primitives.  This introduce is_rejecting_scc() in
      addition to to is_accepting_scc().  Only one of them may be true, but
      they can both be false if scc_info has no idea whether the SCC is
      accepting.
      
      * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: Implement
      is_rejecting_scc().
      * src/bin/ltlcross.cc, src/tgba/acc.cc, src/tgba/acc.hh,
      src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/remfin.cc, src/tgbaalgos/safety.cc,
      src/tgbaalgos/sccfilter.cc: Use it.
      * src/tgbaalgos/dotty.cc: Use is_rejecting_scc() and is_accepting_scc()
      to color SCCs.
      * doc/org/oaut.org: Document the colors used.
      * src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Adjust
      tests.
      * src/tgbatest/sccdot.test: New test case.
      * src/tgbatest/Makefile.am: Add it.
      ebe4ffc5
  21. 26 Feb, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      ltlcross: adjust to work with generic acceptance · 717c8577
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Remove Fin-acceptance before
      doing checks.  More --verbose output.
      * src/tgba/acc.cc, src/tgba/acc.hh: Add an eval_sets() function
      to find the set of acceptance sets needed to satisfy the condition
      in an accepting SCC.
      * src/tgbaalgos/gtec/ce.cc: Use eval_sets() when computing
      a counter example.
      * src/tgbaalgos/gtec/gtec.cc: Raise an exception when called
      on an acceptance that contains Fin.
      * src/tgbatest/ltl2dstar3.test, src/tgbatest/ltlcrossce2.test:
      New files.
      * src/tgbatest/Makefile.am: Add them.
      * src/tgba/tgba.cc (is_empty): Call remove_fin if needed.
      * src/tgbaalgos/product.cc, src/tgbaalgos/dtgbacomp.cc: Adjust
      to work with generic acceptance.
      717c8577
    • Alexandre Duret-Lutz's avatar
      Add a remove_fin() algorithm · 85508a0e
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Add remove_fin().
      * src/tgba/acc.cc, src/tgba/acc.hh: Add is_dnf() and simplify eval().
      * src/tgbaalgos/remfin.cc, src/tgbaalgos/remfin.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatest/remfin.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      85508a0e
  22. 23 Feb, 2015 1 commit
  23. 16 Feb, 2015 1 commit
    • Alexandre Lewkowicz's avatar
      maskkeep: Add a tgba_digraph version · dcad10fc
      Alexandre Lewkowicz authored
      * src/bin/autfilt.cc: Add option --keep-states.
      * src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh: Keep the selected states
      and update the initial state.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/maskkeep.test: New file.
      dcad10fc
  24. 03 Feb, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: add a --sbacc option · acb67c1b
      Alexandre Duret-Lutz authored
      ... to force automata into state-based acceptance.
      
      * src/tgbaalgos/sbacc.cc, src/tgbaalgos/sbacc.hh,
      src/tgbatest/sbacc.test: New files.
      * src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am: Add
      them.
      * src/tgba/tgbagraph.hh (copy_acceptance_conditions_of):
      Call set_acceptance_conditions().
      * src/bin/autfilt.cc: Add option --sbacc.
      acb67c1b
  25. 31 Jan, 2015 3 commits
  26. 27 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      ltldo: new binary · 16a8c031
      Alexandre Duret-Lutz authored
      * src/bin/common_trans.cc, src/bin/common_trans.hh: New files,
      extracted from...
      * src/bin/ltlcross.cc: ... here, so that ltldo can use them.
      * src/bin/ltldo.cc: New file.
      * src/bin/Makefile.am: Adjust.
      * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: Make
      it possible to add new statistics.
      * doc/org/ltldo.org: New file.
      * doc/Makefile.am, doc/org/tools.org: Adjust.
      * src/bin/man/ltldo.x: New file.
      * src/bin/man/Makefile.am: Adjust.
      * src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x: Mention ltldo(1).
      * src/tgbatest/ltldo.test, src/tgbatest/ltldo2.test: New files.
      * src/tgbatest/Makefile.am: Add them.
      * NEWS: Mention ltldo.
      16a8c031
  27. 19 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      simulation: get rid of the "don't care" simulation reductions · 01590273
      Alexandre Duret-Lutz authored
      Those where never really publicized because they were slow and we failed
      to fix what we hopped to fix with them.  They where never used by
      default.  Getting rid of them will make it easier to cleanup the
      simulation code.
      
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Remove
      the simulation code.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
      src/tgbatest/ltl2tgba.cc: Do not call it.
      * src/bin/spot-x.cc: Update doc.
      * src/tgbatest/sim.test: Delete this file.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/spotlbtt.test, bench/ltl2tgba/tools.sim:
      Remove uses to don't care simulation.
      01590273
  28. 17 Dec, 2014 2 commits
  29. 10 Dec, 2014 1 commit
    • Thibaud Michaud's avatar
      Adding function to test if two büchi automata are isomorphic. · 97fdea9d
      Thibaud Michaud authored
      And add the corresponding --isomorphic=FILENAME option to autfilt.
      
      * src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh:
      New.
      * src/tgbaalgos/Makefile.am: Add it.
      * src/bin/autfilt.cc: Add --isomorphic option.
      * src/tgbatest/isomorph.test: Test it.
      * src/tgbatest/Makefile.am: Add it.
      97fdea9d
  30. 07 Dec, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: add a --product option · 8014833a
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Implement the --product option.
      * src/tgbatest/explprod.cc, src/tgbatest/tripprod.cc: Delete.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
      src/tgbatest/tripprod.test: Rewrite using autfilt --product.
      8014833a
  31. 03 Dec, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      randomize: new function · c0e98912
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/randomize.cc, src/tgbaalgos/randomize.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/graph/graph.hh (rename_states_): New method.
      * src/bin/autfilt.cc: Add options --randomize and --seed.
      * src/tgbatest/randomize.test: Test them.
      * src/tgbatest/Makefile.am: Add randomize.test.
      * NEWS: Mention randomize().
      c0e98912
  32. 29 Nov, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      randaut: new binary · c5842c3a
      Alexandre Duret-Lutz authored
      * src/bin/randaut.cc, src/bin/man/randaut.x: New files.
      * src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust.
      * src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomgraph.cc:
      Add an option to output state-based acceptance, and update
      the TGBA properties.
      * src/tgbatest/randaut.test: New test.
      * src/tgbatest/Makefile.am: Add it.
      c5842c3a
  33. 20 Nov, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      monitor: add a few tests · 392c527d
      Alexandre Duret-Lutz authored
      * src/tgbatest/monitor.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      * src/tgbaalgos/minimize.cc (minimize_monitor): Mark
      the output automaton as state-based.
      * src/tgba/tgbagraph.hh: Assume automata with 0 acceptance sets are also
      state-based.
      392c527d