1. 10 Nov, 2015 1 commit
  2. 09 Nov, 2015 1 commit
  3. 08 Nov, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      Add a notebook illustrating decompose_strength() · 104a372c
      Alexandre Duret-Lutz authored
      * wrap/python/tests/decompose.ipynb: New file.
      * wrap/python/tests/Makefile.am: Add it.
      * src/twaalgos/strength.cc: Fix corner cases.
      * src/tests/strength.test: Adjust corner case.
      * NEWS, doc/org/tut.org: Mention the notebook.
      104a372c
    • Alexandre Duret-Lutz's avatar
      Add a decompose_strength() function. · a7db0b54
      Alexandre Duret-Lutz authored
      * src/twaalgos/strength.cc, src/twaalgos/strength.hh
      (decompose_stregth): New function.
      * src/bin/autfilt.cc: Add a --decompose-strength option.
      * src/bin/man/autfilt.x: Add bibliography.
      * src/tests/strength.test: Test it.
      * NEWS: Mention it.
      a7db0b54
  4. 07 Nov, 2015 5 commits
    • 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
    • Alexandre Duret-Lutz's avatar
      autfilt: Add --is-terminal and --is-weak. · f4cf0f40
      Alexandre Duret-Lutz authored
      Fixes #47.
      
      * src/twaalgos/strength.cc, src/twaalgos/strength.hh
      (is_weak_automaton): New function.
      (is_terminal_automaton): Generalize slightly.
      * src/bin/autfilt.cc: Add options --is-terminal and --is-weak.
      * src/tests/readsave.test: Add a test.
      * NEWS: Update.
      f4cf0f40
    • Alexandre Duret-Lutz's avatar
      rename safety.hh as strength.hh · 81cfa05a
      Alexandre Duret-Lutz authored
      * src/twaalgos/safety.cc, src/twaalgos/safety.hh: Rename as ...
      * src/twaalgos/strength.cc, src/twaalgos/strength.hh: ... these.
      * src/bin/ltlfilt.cc, src/tests/ikwiad.cc, src/twaalgos/Makefile.am,
      src/twaalgos/compsusp.cc, src/twaalgos/minimize.cc,
      wrap/python/spot_impl.i: Adjust.
      81cfa05a
    • Alexandre Duret-Lutz's avatar
      rename is_guarantee_automaton() as is_terminal_automaton() · 8a8ec21d
      Alexandre Duret-Lutz authored
      * src/twaalgos/safety.hh, src/twaalgos/safety.cc: Here.
      * src/bin/ltlfilt.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc,
      wrap/python/ajax/spotcgi.in: Adjust.
      * NEWS: Mention the change.
      8a8ec21d
    • Alexandre Duret-Lutz's avatar
      add support for the "terminal" property · 0c5f87b4
      Alexandre Duret-Lutz authored
      * src/twa/twa.hh: Store the terminal property.
      * src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O for "terminal".
      * src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/minimize.cc: Set terminal
      as apropriate.
      * src/twaalgos/safety.cc: Use it.
      * doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
      * src/tests/complement.test, src/tests/monitor.test,
      wrap/python/tests/automata-io.ipynb: Adjust.
      0c5f87b4
  5. 06 Nov, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      add support for the weak property · 65488871
      Alexandre Duret-Lutz authored
      This fixes #119.
      
      * doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
      * src/twa/twa.hh: Support it in automata.
      * src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O support.
      * src/twaalgos/minimize.cc, src/twaalgos/totgba.cc: Set weak
      automata on output.
      * src/tests/complement.test, src/tests/parseaut.test,
      src/tests/readsave.test, src/tests/remfin.test, src/tests/sccsimpl.test,
      src/tests/wdba2.test, wrap/python/tests/automata-io.ipynb: Adjust.
      65488871
  6. 05 Nov, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      hoa: output "unambiguous" only for non-deterministic automata by default · 33c234da
      Alexandre Duret-Lutz authored
      * src/twaalgos/hoa.cc: Output do not output "unambiguous" if the
      automaton is deterministic.  Add option "v" to cancel this restriction,
      and also output "no-univ-branch".
      * src/twaalgos/hoa.hh: Document the "v" option.
      * src/tests/readsave.test: Test it.
      * src/tests/unambig.test: Adjust for unambiguous not being output
      if the automaton is deterministic.
      * src/bin/common_aoutput.cc, NEWS: Document it.
      * doc/org/hoa.org: Add a summary table about how properties are handled.
      * src/twa/twa.hh (prop_deterministic): Setting this should also
      set the unambiguous property.
      * src/twaalgos/isunamb.cc: Simplify the property check.
      33c234da
    • Alexandre Duret-Lutz's avatar
      twa: rename the is_* getters as prop_* · cbb2e64e
      Alexandre Duret-Lutz authored
      This fixes #116.
      
      * src/twa/twa.hh: Rename those methods.
      * NEWS: Document the renamings.
      * doc/org/hoa.org, doc/org/tut21.org, src/parseaut/parseaut.yy,
      src/tests/ikwiad.cc, src/twa/twagraph.hh,
      src/twaalgos/are_isomorphic.cc, src/twaalgos/complete.cc,
      src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc,
      src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/isdet.cc,
      src/twaalgos/isunamb.cc, src/twaalgos/lbtt.cc,
      src/twaalgos/minimize.cc, src/twaalgos/postproc.cc,
      src/twaalgos/product.cc, src/twaalgos/randomgraph.cc,
      src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc,
      src/twaalgos/simulation.cc, src/twaalgos/stutter.cc,
      src/twaalgos/totgba.cc: Adjust.
      cbb2e64e
  7. 04 Nov, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      twa: no default argument for property setters · 8ea5f73c
      Alexandre Duret-Lutz authored
      This is a preliminary for the renaming suggested in #116.
      
      * src/twa/twa.hh (prop_state_based_acc, prop_inherently_weak,
      prop_deterministic, prop_unambiguous, prop_stutter_invariant,
      prop_stutter_sensitive): Do not default the argument to true.
      * src/parseaut/parseaut.yy, src/twaalgos/degen.cc,
      src/twaalgos/dtbasat.cc, src/twaalgos/dtgbasat.cc,
      src/twaalgos/minimize.cc, src/twaalgos/randomgraph.cc,
      src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc,
      src/twaalgos/simulation.cc, src/twaalgos/totgba.cc,
      wrap/python/tests/remfin.py: Adjust.
      8ea5f73c
    • Alexandre Duret-Lutz's avatar
      parseaut: do not ignore the "unambiguous" property · bf574918
      Alexandre Duret-Lutz authored
      Fixes #115.
      
      * src/parseaut/parseaut.yy: Set the property on the output automaton.
      * src/tests/unambig.test: Add a test case.
      * NEWS: Mention the fix.
      bf574918
  8. 29 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: fix output of twa_run · aaff42ee
      Alexandre Duret-Lutz authored
      * src/twaalgos/emptiness.hh, src/twaalgos/emptiness.cc: Declare the
      operator<< for twa_run, not for twa_run_ptr (the shared_ptr
      automatically forward operator<<).
      * wrap/python/spot_impl.i: Add __str__ to twa_run, not twa_run_ptr.
      aaff42ee
  9. 28 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      twa_succ_iterator: rename accessors · f6af2a84
      Alexandre Duret-Lutz authored
      * src/twa/twa.hh, src/ta/ta.hh (current_state,
      current_acceptance_conditions, current_condition): Rename as...
      (dst, acc, cond): ... these.
      * iface/ltsmin/ltsmin.cc, src/kripke/fairkripke.cc,
      src/kripke/fairkripke.hh, src/kripke/kripke.cc,
      src/kripke/kripke.hh, src/kripke/kripkeexplicit.cc,
      src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.cc,
      src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
      src/ta/taproduct.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
      src/taalgos/dot.cc, src/taalgos/emptinessta.cc,
      src/taalgos/minimize.cc, src/taalgos/reachiter.cc,
      src/taalgos/tgba2ta.cc, src/twa/taatgba.cc, src/twa/taatgba.hh,
      src/twa/twagraph.hh, src/twa/twaproduct.cc,
      src/twa/twasafracomplement.cc, src/twaalgos/bfssteps.cc,
      src/twaalgos/bfssteps.hh, src/twaalgos/compsusp.cc,
      src/twaalgos/copy.cc, src/twaalgos/emptiness.cc,
      src/twaalgos/gtec/gtec.cc, src/twaalgos/gv04.cc,
      src/twaalgos/lbtt.cc, src/twaalgos/ltl2tgba_fm.cc,
      src/twaalgos/magic.cc, src/twaalgos/minimize.cc,
      src/twaalgos/ndfs_result.hxx, src/twaalgos/reachiter.cc,
      src/twaalgos/se05.cc, src/twaalgos/stats.cc,
      src/twaalgos/stutter.cc, src/twaalgos/tau03.cc,
      src/twaalgos/tau03opt.cc, wrap/python/tests/interdep.py: Adjust.
      * NEWS: Mention the renamings.
      f6af2a84
  10. 27 Oct, 2015 1 commit
  11. 26 Oct, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      bin: factor handling of -B/-C/-D/... output options · 71979840
      Alexandre Duret-Lutz authored
      * src/bin/common_post.cc: Handle the options
      for BA/TGBA/Monitor as well as Complete/SBAcc here,
      and in the same group.  Rename "Translation intent"
      and "Optimization level" to "Simplification goal" and
      "Simplification level" so that it makes sense even
      in autfilt.
      * src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
      src/bin/ltl2tgba.cc: Remove common code.
      * doc/org/autfilt.org, doc/org/dstar2tgba.org,
      doc/org/ltl2tgba.org: Adjust sed invocations.
      71979840
    • Alexandre Duret-Lutz's avatar
      parse_aut: simplify the interface · dee73ee3
      Alexandre Duret-Lutz authored
      * src/parseaut/public.hh, src/parseaut/parseaut.yy,
      src/parseaut/fmterror.cc: Add a raise_errors options.  Remove the
      parse_strict() method.  Store parse errors and filename in the output
      parsed_aut to simplify usage.
      * doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org,
      src/bin/autfilt.cc, src/bin/common_hoaread.cc, src/bin/dstar2tgba.cc,
      src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/complementation.cc,
      src/tests/ikwiad.cc, src/tests/ltlcross3.test, src/tests/ltldo.test,
      wrap/python/spot.py, wrap/python/tests/parsetgba.py: Adjust usage.
      * NEWS: Mention the changes.
      dee73ee3
  12. 25 Oct, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      twa_run: swallow reduce_run, replay_twa_run, twa_run_to_tgba · 99c967f0
      Alexandre Duret-Lutz authored
      These now become twa_run::reduce, twa_run::replay, and
      twa_run::as_twa.
      
      * src/twaalgos/reducerun.cc, src/twaalgos/reducerun.hh,
      src/twaalgos/replayrun.cc, src/twaalgos/replayrun.hh: Delete.
      * src/twaalgos/Makefile.am: Adjust.
      * src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh: Move
      the above functions here, as method of twa_run.
      * src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
      src/tests/emptchk.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc,
      wrap/python/ajax/spotcgi.in, iface/ltsmin/modelcheck.cc: Adjust.
      * NEWS: List the renamings.
      99c967f0
    • Alexandre Duret-Lutz's avatar
      twa_run: keep a pointer to the automaton · 63917def
      Alexandre Duret-Lutz authored
      This simplify all laters invocations, because we do not have to pass
      the automaton the run was generated on.
      
      This fixes #113 by allowing the __str__ function to be implemented on
      runs.
      
      * src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh (twa_run):
      Store the automaton.
      (prin_twa_run): Rewrite as an overloaded <<.
      * src/twaalgos/reducerun.cc, src/twaalgos/reducerun.hh (reduce_run):
      Do not like the automaton as a parameter.
      * src/twaalgos/replayrun.cc, src/twaalgos/replayrun.hh (replay_twa_run):
      Likewise.
      * src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
      src/tests/complementation.cc, src/tests/ikwiad.cc,
      src/tests/randtgba.cc, src/twaalgos/gtec/ce.cc, src/twaalgos/gv04.cc,
      src/twaalgos/magic.cc, src/twaalgos/ndfs_result.hxx,
      src/twaalgos/se05.cc, src/twaalgos/projrun.cc: Adjust.
      * wrap/python/ajax/spotcgi.in: Add a __str__ function to twa_run_ptr.
      * wrap/python/spot_impl.i: Adjust.
      63917def
    • Alexandre Duret-Lutz's avatar
  13. 24 Oct, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      rename tgba_run as twa_run · 4221e68d
      Alexandre Duret-Lutz authored
      Part of #113.
      
      * src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh (tgba_run):
      Rename as ...
      (twa_run): ... this.
      * NEWS: Mention it.
      * iface/ltsmin/modelcheck.cc, src/tests/complementation.cc,
      src/tests/emptchk.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc,
      src/twa/twa.hh, src/twaalgos/bfssteps.cc, src/twaalgos/bfssteps.hh,
      src/twaalgos/gtec/ce.cc, src/twaalgos/gtec/ce.hh,
      src/twaalgos/gv04.cc, src/twaalgos/magic.cc, src/twaalgos/minimize.cc,
      src/twaalgos/ndfs_result.hxx, src/twaalgos/projrun.cc,
      src/twaalgos/projrun.hh, src/twaalgos/reducerun.cc,
      src/twaalgos/reducerun.hh, src/twaalgos/replayrun.cc,
      src/twaalgos/replayrun.hh, src/twaalgos/se05.cc, src/twaalgos/word.cc,
      src/twaalgos/word.hh, wrap/python/ajax/spotcgi.in,
      wrap/python/spot_impl.i: Adjust.
      4221e68d
    • Alexandre Duret-Lutz's avatar
      stats: rename structures and attribute for concistency · 4a91fccc
      Alexandre Duret-Lutz authored
      * src/taalgos/stats.cc, src/taalgos/stats.hh
      (tgba_statistics::transitions, tgba_sub_statistics::sub_transitions):
      Rename ...
      (twa_statistics::edges, twa_sub_statistics::transitions): ... to
      these.
      * NEWS: Mention it.
      * src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
      src/tests/checkta.cc, src/tests/complementation.cc,
      src/tests/ikwiad.cc, src/tests/ltl2tgba.test,
      src/tests/neverclaimread.test, src/tests/randtgba.cc,
      src/tests/renault.test, src/tests/wdba2.test, src/twaalgos/dtbasat.cc,
      src/twaalgos/dtgbasat.cc, src/twaalgos/stats.cc,
      src/twaalgos/stats.hh, wrap/python/ajax/spotcgi.in: Adjust.
      4a91fccc
    • Alexandre Duret-Lutz's avatar
      f7c4ca81
    • Alexandre Duret-Lutz's avatar
      db99f3bd
  14. 23 Oct, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      doc: show more metadata about automata · 84f9be9e
      Alexandre Duret-Lutz authored
      * src/twa/bdddict.hh (varnum): New method.
      * doc/org/tut21.org: Show more metadata.
      84f9be9e
    • Alexandre Duret-Lutz's avatar
      parseaut: Add a trust_hoa option. · 51a75a31
      Alexandre Duret-Lutz authored
      Fixes #114.
      
      * src/parseaut/public.hh: Add support for a trust_hoa option.
      * src/parseaut/parseaut.yy: If trust_hoa is set, recognize the
      "inherently-weak" and "stutter-invariant" properties.
      * src/bin/common_conv.cc, src/bin/common_conv.hh (read_automaton):
      Move...
      * src/bin/common_hoaread.cc, src/bin/common_hoaread.hh: ... in this
      new file, that also handle the --trust-hoa option.
      * src/bin/Makefile.am: Add them.
      * src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
      src/bin/ltldo.cc: Use them.
      * src/tests/parseaut.test, src/tests/ltldo.test: Adjust, and test
      --trust-hoa=no.
      * src/tests/complement.test, src/tests/prodor.test,
      src/tests/sbacc.test: Adjust.
      * wrap/python/spot.py (automata): Add option trust_hoa.
      * NEWS: Update.
      51a75a31
    • Alexandre Duret-Lutz's avatar
      parseaut: change the interface to allow new options · 585e29e7
      Alexandre Duret-Lutz authored
      * src/parseaut/public.hh, src/parseaut/parseaut.yy: Make it easier to
      pass new options to the parser.
      * src/tests/ikwiad.cc, wrap/python/spot.py: Adjust.
      585e29e7
  15. 21 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      fix "input buffer overflow, can't enlarge buffer..." · 64df4fbc
      Alexandre Duret-Lutz authored
      This occured when parsing the HOA automaton generated by Rabinizer3 for
      a very long LTL formula with many nested U.  State labels could easily
      be more than 40k characters.
      
      * src/parseaut/scanaut.ll: Fix that.
      * src/tests/parseaut.test: New test case.
      * NEWS: Mention the fix.
      64df4fbc
  16. 20 Oct, 2015 1 commit
  17. 19 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      fix unabbreviate · e1ddf978
      Alexandre Duret-Lutz authored
      This is a bug:
      
          % ltlfilt -f 'a W b' --unabbreviate=WR
          a U (b | (a W b))
      
      * src/tl/unabbrev.cc: Here.
      * src/tests/unabbrevwm.test: Harden test case.
      * wrap/python/tests/randltl.ipynb: Adjust expected output.
      * NEWS: Mention the fix.
      e1ddf978
  18. 18 Oct, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      tl: rename ltl_simplifier to tl_simplifier · 176c9e2e
      Alexandre Duret-Lutz authored
      * doc/org/tut01.org, doc/tl/tl.tex, src/bin/common_r.hh,
      src/bin/ltlfilt.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
      src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
      src/tl/nenoform.cc, src/tl/randomltl.cc, src/tl/randomltl.hh,
      src/tl/simplify.cc, src/tl/simplify.hh, src/twaalgos/ltl2tgba_fm.cc,
      src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/stutter.cc,
      src/twaalgos/translate.cc, src/twaalgos/translate.hh,
      wrap/python/ajax/spotcgi.in, wrap/python/spot.py,
      wrap/python/tests/interdep.py: Rename ltl_simplifier to tl_simplifier.
      * NEWS: Mention it.
      176c9e2e
    • Alexandre Duret-Lutz's avatar
      * src/tl/simplify.hh: Fix comment. · 21be883c
      Alexandre Duret-Lutz authored
      21be883c
  19. 17 Oct, 2015 1 commit
  20. 15 Oct, 2015 5 commits
    • Alexandre Duret-Lutz's avatar
      parseaut: better diagnostic of unsupported versions · 9e7d0677
      Alexandre Duret-Lutz authored
      * src/parseaut/parseaut.yy: Add and the a check_version() function.
      * src/tests/parseaut.test: Test it.
      * NEWS: Mention it.
      9e7d0677
    • Alexandre Duret-Lutz's avatar
      ltlgrind: fix handling of FILENAME/COL · 0671d628
      Alexandre Duret-Lutz authored
      This additionally fixes #107.
      
      * src/bin/ltlgrind.cc: Fix handling for FILEANAME/COL.  Document FORMAT
      in --help.  Assume -F for arguments given without options.
      * src/tests/ltlgrind.test: Add two tests.
      * NEWS: Mention this.
      0671d628
    • Alexandre Duret-Lutz's avatar
      autfilt: easier simplification defaults · e3682a23
      Alexandre Duret-Lutz authored
      This is motivated by an email from Fanda.
      
      * src/bin/common_post.cc, src/bin/common_post.hh: Add variables to
      detect when level or pref are sets.
      * src/bin/autfilt.cc: Adjust default for pref/sets.
      * src/tests/readsave.test: Add test cases.
      * NEWS: Mention it.
      e3682a23
    • 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
    • Alexandre Duret-Lutz's avatar
      fix crash of randaut -Q0 · 6cf807da
      Alexandre Duret-Lutz authored
      * src/twaalgos/randomgraph.cc: Replace an assertion by an exception.
      * src/bin/randaut.cc: Diagnose -Q0.
      * src/tests/randaut.test: Test it.
      * NEWS: Mention the bug.
      6cf807da