1. 03 Jan, 2015 13 commits
    • Alexandre Duret-Lutz's avatar
      More files to ignore. · 3b7b5202
      Alexandre Duret-Lutz authored
      3b7b5202
    • Alexandre Duret-Lutz's avatar
      bin: --dot=s display SCCs · b048f65d
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.cc: Add option 's' to display SCCs.
      * src/bin/dstar2tgba.cc, src/bin/common_aoutput.cc: Document it.
      * src/tgbatest/neverclaimread.test: Test it.
      b048f65d
    • Alexandre Duret-Lutz's avatar
      bin: use common_aoutput in ltl2tgba · 40fb80ea
      Alexandre Duret-Lutz authored
      * src/bin/common_aoutput.hh, src/bin/common_aoutput.cc: Adjust to
      support three kind of statistics printer, depending on whether the
      tool input formulas, automata, or nothing.
      * src/bin/randaut.cc, src/bin/autfilt.cc: Adjust.
      * src/bin/ltl2tgba.cc: Use the common_aoutput printers.  The
      --csv-escape option disappeared along the way, but it was not honored
      anyway...
      40fb80ea
    • Alexandre Duret-Lutz's avatar
      bin: factor output options of autfilt and randaut · 72737dfe
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Move output options handling...
      * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh:... here.
      * src/bin/randaut.cc: Use them.
      * src/tgbatest/randaut.test: Test --name and --stats for randaut.
      72737dfe
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      ltlgrind: cosmetics · cf65f606
      Alexandre Duret-Lutz authored
      * src/bin/ltlgrind.cc: Adjust help text to match other tools.
      cf65f606
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: rename --hoa to --hoaf · 06b8118d
      Alexandre Duret-Lutz authored
      for consistency with autfilt, randaut, and dstar2tgba
      
      * src/bin/ltl2tgba.cc: Here.
      06b8118d
    • Alexandre Duret-Lutz's avatar
      autfilt, randaut: rename --uniq to --unique · a7c1d4c4
      Alexandre Duret-Lutz authored
      for consistency with ltlfilt
      
      * src/bin/autfilt.cc, src/bin/randaut.cc: Here.
      a7c1d4c4
    • Alexandre Duret-Lutz's avatar
      bin: tooling and documentation about option names · 18d8c3ef
      Alexandre Duret-Lutz authored
      * src/bin/options.py: New file.
      * src/bin/Makefile.am: Distribute it.
      * src/bin/README: New file.
      18d8c3ef
    • Alexandre Duret-Lutz's avatar
      randaut: fix --uniq · 21dcc73d
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Also accept '-u' for '--uniq'.
      * src/bin/randaut.cc: Likewise, plus fix the unicity check.
      * src/tgbatest/uniq.test: Really test it.
      21dcc73d
    • Alexandre Duret-Lutz's avatar
      autfilt: move output functions to a separate file · 36f99565
      Alexandre Duret-Lutz authored
      * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: New files...
      * src/bin/autfilt.cc: ... extracted from here.
      * src/bin/Makefile.am: Add them.
      36f99565
    • Alexandre Duret-Lutz's avatar
      tgba_digraph: force selection of properties kept on copy · 87c2b291
      Alexandre Duret-Lutz authored
      * src/tgba/tgba.hh: Declare a prop_set to specify the types.
      * src/tgba/tgbagraph.hh: Use prop_set for all copy constructors.
      * iface/ltsmin/ltsmin.cc, src/bin/autfilt.cc, src/bin/randaut.cc,
      src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/closure.cc,
      src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dtgbacomp.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stutterize.cc, src/tgbatest/checkpsl.cc,
      src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
      wrap/python/spot.i,src/graphtest/tgbagraph.test: Adjust all uses.
      87c2b291
    • Alexandre Duret-Lutz's avatar
      dotty: switch to horizontal output and add options · 0f178288
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Add an options
      parameter.
      * src/bin/randaut.cc, src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
      src/bin/ltl2tgba.cc, wrap/python/ajax/spot.in: Use it.
      * src/tgbatest/det.test, src/tgbatest/dstar.test,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/monitor.test,
      src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test,
      src/graphtest/tgbagraph.test: Adjust
      because automata are now output horizontally.
      * NEWS: Mention the change.
      0f178288
  2. 23 Dec, 2014 1 commit
  3. 17 Dec, 2014 6 commits
    • Thibaud Michaud's avatar
      option --uniq in autfilt and randaut · a989d41b
      Thibaud Michaud authored
      * src/bin/autfilt.cc: add option --uniq.
      * src/bin/randaut.cc: add option --uniq.
      * src/tgbatest/uniq.test: Test it.
      a989d41b
    • Thibaud Michaud's avatar
      Wrap are_isomorphic inside a class and optimize when deterministic · 17687855
      Thibaud Michaud authored
      * src/bin/autfilt.cc: Use isomorphism_checker.
      * src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh: Wrap
      are_isomorphic inside a class to keep the canonic version of the first
      automaton between two calls, and use a more efficient algorithm in case
      both automata are deterministic.
      * src/tgbatest/isomorph.test: Add tests for deterministic automata.
      17687855
    • Thibaud Michaud's avatar
      Adding function to canonicalize an automaton. · 1995602d
      Thibaud Michaud authored
      * src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
      src/bin/autfilt.cc: are_isomorphic now uses canonicalize. It returns a
      bool, because the mapping cannot be deduced easily from the
      canonicalized automaton.
      * src/graph/graph.hh: Add equality operator to trans_storage_t
      for easy comparison of transition vectors.
      * src/tgba/tgbagraph.hh: Add equality operator to tgba_graph_trans_data
      and to tgba_digraph.
      * src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh:
      New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatest/isomorph.test: Test them.
      1995602d
    • Alexandre Duret-Lutz's avatar
      autfilt: %w shows an accepting word · b83d6d7f
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Support %w.
      * src/tgbatest/readsave.test: Test it.
      b83d6d7f
    • Alexandre Duret-Lutz's avatar
      autfilt: --instut, --destut, --is-empty · a626a32d
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Add these new options.
      * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh: Make it
      possible to call sl() and sl2() without passing the set of atomic
      propositions.
      * src/tgbatest/stutter.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      a626a32d
    • Alexandre Duret-Lutz's avatar
      merge transitions: also merge transitions with same conditions · 8e9c4317
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.cc (merge_transition): Do it.
      * src/tgbatest/readsave.test: Test it.
      * src/bin/autfilt.cc: Fix statistics about the original
      automaton when using --stats or --name.
      8e9c4317
  4. 16 Dec, 2014 3 commits
  5. 15 Dec, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      autfilt: --count · 0d710f96
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Add a --count option.
      * src/tgbatest/randaut.test: Test autfilt's --count and --states.
      0d710f96
    • Alexandre Duret-Lutz's avatar
      autfilt: --states=RANGE · cad4d94c
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Add a --states=RANGE option.
      * src/bin/common_range.cc, src/bin/common_range.hh: Generalize
      range_parse to allow an optional upper bound.
      cad4d94c
  6. 11 Dec, 2014 4 commits
  7. 10 Dec, 2014 5 commits
  8. 09 Dec, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      tgba: simplify usage of named properties · 61edf7f4
      Alexandre Duret-Lutz authored
      * src/tgba/tgba.hh, src/tgba/tgba.cc (set_named_prop): Add a template
      version.
      (get_named_prop): Hide the old version, and supply a template version
      that casts.
      * src/bin/ltlcross.cc, src/hoaparse/hoaparse.yy, src/tgbaalgos/hoa.cc,
      src/tgbaalgos/product.cc: Adjust usage.
      61edf7f4
  9. 08 Dec, 2014 1 commit
  10. 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
  11. 04 Dec, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      hoa: swallow the neverclaim parser · e1bba500
      Alexandre Duret-Lutz authored
      This way we can easily parse a stream of HOAs intermixed with
      neverclaims.
      
      * src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll: Add rules
      for neverclaims, adjusted from src/neverparse/neverclaimparse.yy
      and src/neverparse/neverclaimparse.ll.
      * src/hoaparse/public.hh, NEWS: Update documentation.
      * src/neverparse/: Remove this directory.
      * README, configure.ac, src/Makefile.am: Adjust accordingly.
      * src/tgbatest/ltl2tgba.cc, src/bin/ltlcross.cc: Use HOA
      parser to read neverclaims.
      * src/tgbatest/hoaparse.test, src/tgbatest/neverclaimread.test: Adjust.
      e1bba500
  12. 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
  13. 30 Nov, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      defaultenv: simplify usage · 4f1535c8
      Alexandre Duret-Lutz authored
      * src/ltlenv/defaultenv.hh, src/ltlenv/defaultenv.cc (require): Return
      an atomic_prop*, not a formula*.
      * src/bin/randaut.cc, src/bin/randltl.cc, src/ltlvisit/apcollect.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Do not cast
      the return of require().
      4f1535c8