1. 14 Jun, 2016 2 commits
  2. 01 May, 2016 3 commits
    • Alexandre Duret-Lutz's avatar
      print_hoa: output all registered APs · a1b3b065
      Alexandre Duret-Lutz authored
      Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap()
      so that the methods where this behavior is expected can be fixed.
      
      And fix ltsmin::kripke() which did not register APs.
      
      Part of #170.
      
      * spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs.
      Throw an exception when printing automata using unregistered APs.
      * spot/ltsmin/ltsmin.cc: Call register_ap().
      * spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
      spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap):
      New methods.
      * spot/tl/exclusive.cc, spot/twaalgos/postproc.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them.
      * tests/core/maskacc.test, tests/core/maskkeep.test,
      tests/core/strength.test: Adjust expected results.
      * NEWS: Mention those changes.
      a1b3b065
    • Alexandre Duret-Lutz's avatar
      honor ap() when counting transitions · dad17b36
      Alexandre Duret-Lutz authored
      Fixing this bug alone revealed another bug: parsing never claim or LBTT
      automata did not register APs.  So this fixes both bugs.
      
      This is the first part of #170.
      
      * spot/twa/twa.hh (register_aps_from_dict): New method.
      * spot/parseaut/parseaut.yy: Call it for never claim and LBTT files.
      * spot/twaalgos/stats.cc: Simplify using ap_vars().
      * tests/core/ltl2tgba.test: Add a test case.
      * NEWS: Mention the bugs.
      dad17b36
    • Alexandre Duret-Lutz's avatar
      autfilt: fix simpification of exclusive AP · 4f913c7f
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Here.
      * tests/core/exclusive-tgba.test: Test it.
      * NEWS: Mention the fix.
      4f913c7f
  3. 20 Apr, 2016 1 commit
  4. 09 Apr, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlfilt: implement --reject-word and --accept-word · 59e1f6a3
      Alexandre Duret-Lutz authored
      * bin/common_range.hh: Store the common definition of words.
      * bin/autfilt.cc: Use it.
      * bin/ltlfilt.cc: Likewise, and implement those two options.
      * tests/core/acc_word.test: Test them.
      * doc/org/autfilt.org: Augment the last example to point out
      that it can now be done with ltlfilt.
      * NEWS: Mention the new options.
      59e1f6a3
  5. 13 Mar, 2016 1 commit
  6. 10 Mar, 2016 1 commit
    • Laurent XU's avatar
      sanity: Replace tabulars by spaces in *.cc *.hh *.hxx · f7e7b4f1
      Laurent XU authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh,
      bin/common_finput.cc, bin/common_finput.hh, bin/common_hoaread.cc,
      bin/common_output.cc, bin/common_output.hh, bin/common_post.cc,
      bin/common_post.hh, bin/common_r.hh, bin/common_range.cc,
      bin/common_range.hh, bin/common_setup.cc, bin/common_trans.cc,
      bin/common_trans.hh, bin/dstar2tgba.cc, bin/genltl.cc,
      bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc,
      bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc,
      bin/spot-x.cc, spot/graph/graph.hh, spot/graph/ngraph.hh,
      spot/kripke/kripkegraph.hh, spot/ltsmin/ltsmin.cc,
      spot/ltsmin/ltsmin.hh, spot/misc/bareword.cc, spot/misc/bitvect.cc,
      spot/misc/bitvect.hh, spot/misc/common.hh, spot/misc/escape.cc,
      spot/misc/fixpool.hh, spot/misc/formater.cc, spot/misc/hash.hh,
      spot/misc/intvcmp2.cc, spot/misc/intvcmp2.hh, spot/misc/intvcomp.cc,
      spot/misc/intvcomp.hh, spot/misc/location.hh, spot/misc/minato.cc,
      spot/misc/minato.hh, spo...
      f7e7b4f1
  7. 08 Mar, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      autfilt: add a --reject-word option · 7e2e4df1
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Implement --reject-word.
      * NEWS, doc/org/autfilt.org: More doc.
      * tests/core/acc_word.test: More tests.
      7e2e4df1
    • Alexandre Duret-Lutz's avatar
      autfilt: fix --accept-word · 897a6ddc
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Translate each word as an automaton once,
      and do not make a global product of all of them.
      * spot/twaalgos/word.cc: Register the atomic propositions used by the
      word when converting it into an automaton.
      * tests/core/acc_word.test: Add a test case that used to fail, and
      another test that make sure some words are not accepted.
      897a6ddc
  8. 07 Mar, 2016 1 commit
    • Amaury Fauchille's avatar
      autfilt: add new option --accept-word · 1c824443
      Amaury Fauchille authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      Suggested by Matthias Heizmann. Fixes #109.
      
      * NEWS: notify the new option
      * THANKS: add Matthias Heizmann
      * bin/autfilt.cc: add new option --accept-word=WORD which filters
      automata that accept WORD
      * doc/org/autfilt.org: add an example of the new option
      * tests/Makefile.am: add core/acc_word.test to the list of test files
      * tests/core/acc_word.test: test some uses of the new option
      1c824443
  9. 03 Mar, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      rename two confusing methods of emptiness_check_instantiator · ad08a585
      Alexandre Duret-Lutz authored
      * spot/twaalgos/emptiness.hh (emptiness_check_instantiator): rename
      min_acceptance_conditions and max_acceptance_conditions to
      min_sets and max_sets.
      * spot/twaalgos/emptiness.cc, python/ajax/spotcgi.in,
      tests/core/ikwiad.cc, tests/core/emptchk.cc, tests/core/randtgba.cc:
      Adjust.
      * doc/org/upgrade2.org, NEWS: Mention the change.
      ad08a585
  10. 17 Feb, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      parsetl: change the interface to return a parsed_formula · 22f442f7
      Alexandre Duret-Lutz authored
      This gets the interface of all the functions parsing formula in line
      with the interface of the automaton parser: both return a "parsed_*"
      object (parsed_formula or parsed_automaton) that contains the said
      object and its list of errors.  Doing so avoid having to declare the
      parse_error_list in advance.
      
      * spot/tl/parse.hh, spot/parsetl/parsetl.yy: Do the change.
      * spot/parsetl/fmterror.cc: Adjust the error printer.
      * NEWS: Document it.
      * bin/common_finput.cc, bin/common_finput.hh, bin/ltlcross.cc,
      bin/ltldo.cc, bin/ltlfilt.cc, doc/org/tut01.org, doc/org/tut02.org,
      doc/org/tut10.org, doc/org/tut20.org, python/ajax/spotcgi.in,
      python/spot/impl.i, spot/parseaut/parseaut.yy, tests/core/checkpsl.cc,
      tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
      tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
      tests/core/length.cc, tests/core/ltlprod.cc, tests/core/ltlrel.cc,
      tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc,
      tests/core/safra.cc, tests/core/syntimpl.cc, tests/core/tostring.cc,
      tests/ltsmin/modelcheck.cc, tests/python/alarm.py,
      tests/python/interdep.py, tests/python/ltl2tgba.py,
      tests/python/ltlparse.py: Adjust all uses.
      22f442f7
  11. 15 Feb, 2016 6 commits
  12. 12 Feb, 2016 13 commits
  13. 05 Feb, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: add option C(COLOR) · 77b0b5b3
      Alexandre Duret-Lutz authored
      This fixes the output gliches visible in the previous patches,
      where highlighting a state would remove its fill color.
      
      * spot/twaalgos/dot.cc, spot/taalgos/dot.cc: Implement option C(COLOR).
      * bin/common_aoutput.cc, doc/org/oaut.org: Document it.
      * doc/org/.dir-locals.el.in, doc/org/init.el.in,
      python/spot/__init__.py: Use it.
      * tests/python/automata-io.ipynb, tests/python/automata.ipynb,
      tests/python/highlighting.ipynb: Test it.
      * tests/core/readsave.test: Adjust.
      * NEWS: Mention recent changes.
      77b0b5b3
  14. 04 Feb, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      parseaut, dot: install a highlighting framework · 348f7cce
      Alexandre Duret-Lutz authored
      * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll:
      Parse "spot.highlight.edges" and "spot.highlight.states" to
      fill the "highlight-edges" and "highlight-states" properties.
      * spot/twaalgos/dot.cc: Use these properties to highlight states.
      * tests/core/readsave.test: Add a small test.
      348f7cce
    • Alexandre Duret-Lutz's avatar
      parse_acc: cleanup error reporting · 91bb93ee
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc: Factor all the error reporting code in a single
      place, and improve the error message at end of acceptance.
      * tests/core/randaut.test: Add more tests.
      91bb93ee
  15. 03 Feb, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      rename parse_print_test as kripkecat · 22345d0c
      Alexandre Duret-Lutz authored
      Fixes #135.
      
      * tests/core/parse_print_test.cc: Rename as...
      * tests/core/kripkecat.cc: ... this.
      * tests/Makefile.am, tests/core/.gitignore, tests/core/kripke.test,
      tests/ltsmin/kripke.test: Adjust.
      22345d0c
  16. 01 Feb, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      dot, hoa: default to "k" for kripke structure · 02b5460b
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc: If a Kripke
      structure is passed, automatically enable the "k" option.
      * tests/core/parse_print_test.cc, tests/ltsmin/modelcheck.cc,
      tests/python/ltsmin.ipynb: Remove the explicit use of "k".
      * NEWS: Mention the change.
      02b5460b
    • Alexandre Duret-Lutz's avatar
      dot: add option "k" · a9b4560f
      Alexandre Duret-Lutz authored
      Fixes #134.
      
      * spot/twaalgos/dot.cc: Implement it.
      * bin/common_aoutput.cc, spot/twaalgos/dot.hh, NEWS: Document it.
      * tests/core/readsave.test, tests/python/ltsmin.ipynb: Test it.
      a9b4560f
  17. 29 Jan, 2016 1 commit