1. 25 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      cleanacc: better cleanup · 7353e47f
      Alexandre Duret-Lutz authored
      Sometimes, simplifying the acceptance condition (because it refers to
      sets that do not appear in the automaton) cause more sets to be removed
      from the acceptance condition, and therefore warrant another pass to
      remove those sets from the automaton.
      
      * src/tgbaalgos/cleanacc.cc: Here.
      * src/tgbatest/hoaparse.test: Add a test case.
      7353e47f
  2. 24 Mar, 2015 5 commits
  3. 23 Mar, 2015 5 commits
    • Alexandre Duret-Lutz's avatar
      dot: better support of state-based acceptance · ead2ca01
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.cc: Here.
      * src/tgbaalgos/sbacc.cc: Make the produced automata as state-based.
      * src/tgbatest/readsave.test: Add a test.
      ead2ca01
    • 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
    • Alexandre Duret-Lutz's avatar
      ltlfilt: add a --exclusive-ap option · 544c533e
      Alexandre Duret-Lutz authored
      * src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/bin/ltlfilt.cc: Implement the --exclusive-ap option.
      * NEWS: Mention it.
      * src/ltltest/exclusive.test: New file.
      * src/ltltest/Makefile.am: Add it.
      544c533e
    • Etienne Renault's avatar
      Replace guards by pragma once. · 57cd9f2d
      Etienne Renault authored
      * iface/ltsmin/ltsmin.hh, src/bin/common_aoutput.hh,
      src/bin/common_conv.hh, src/bin/common_cout.hh,
      src/bin/common_file.hh, src/bin/common_finput.hh,
      src/bin/common_output.hh, src/bin/common_post.hh,
      src/bin/common_r.hh, src/bin/common_range.hh,
      src/bin/common_setup.hh, src/bin/common_sys.hh,
      src/bin/common_trans.hh, src/dstarparse/parsedecl.hh,
      src/dstarparse/public.hh, src/graph/graph.hh,
      src/graph/ngraph.hh, src/hoaparse/parsedecl.hh,
      src/hoaparse/public.hh, src/kripke/fairkripke.hh,
      src/kripke/fwd.hh, src/kripke/kripke.hh,
      src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.hh,
      src/kripkeparse/parsedecl.hh, src/kripkeparse/public.hh,
      src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh,
      src/ltlast/binop.hh, src/ltlast/bunop.hh,
      src/ltlast/constant.hh, src/ltlast/formula.hh,
      src/ltlast/multop.hh, src/ltlast/predecl.hh,
      src/ltlast/unop.hh, src/ltlast/visitor.hh,
      src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/ltlvisit/apcollect.hh,
      src/ltlvisit/clone.hh, src/ltlvisit/contain.hh,
      src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh,
      src/ltlvisit/lbt.hh, src/ltlvisit/length.hh,
      src/ltlvisit/lunabbrev.hh, src/ltlvisit/mark.hh,
      src/ltlvisit/mutation.hh, src/ltlvisit/nenoform.hh,
      src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.hh,
      src/ltlvisit/relabel.hh, src/ltlvisit/remove_x.hh,
      src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.hh,
      src/ltlvisit/snf.hh, src/ltlvisit/tostring.hh,
      src/ltlvisit/tunabbrev.hh, src/ltlvisit/wmunabbrev.hh,
      src/misc/bareword.hh, src/misc/bddlt.hh, src/misc/bitvect.hh,
      src/misc/casts.hh, src/misc/common.hh, src/misc/escape.hh,
      src/misc/fixpool.hh, src/misc/formater.hh, src/misc/hash.hh,
      src/misc/hashfunc.hh, src/misc/intvcmp2.hh,
      src/misc/intvcomp.hh, src/misc/location.hh, src/misc/ltstr.hh,
      src/misc/memusage.hh, src/misc/minato.hh, src/misc/mspool.hh,
      src/misc/optionmap.hh, src/misc/position.hh, src/misc/random.hh,
      src/misc/satsolver.hh, src/misc/timer.hh, src/misc/tmpfile.hh,
      src/misc/version.hh, src/priv/accmap.hh, src/priv/bddalloc.hh,
      src/priv/freelist.hh, src/ta/ta.hh, src/ta/taexplicit.hh,
      src/ta/taproduct.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.hh,
      src/ta/tgtaproduct.hh, src/taalgos/dotty.hh,
      src/taalgos/emptinessta.hh, src/taalgos/minimize.hh,
      src/taalgos/reachiter.hh, src/taalgos/statessetbuilder.hh,
      src/taalgos/stats.hh, src/taalgos/tgba2ta.hh,
      src/tgba/acc.hh, src/tgba/bdddict.hh,
      src/tgba/bddprint.hh, src/tgba/formula2bdd.hh, src/tgba/fwd.hh,
      src/tgba/taatgba.hh, src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
      src/tgba/tgbamask.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.hh,
      src/tgba/tgbasafracomplement.hh, src/tgbaalgos/are_isomorphic.hh,
      src/tgbaalgos/bfssteps.hh, src/tgbaalgos/canonicalize.hh,
      src/tgbaalgos/cleanacc.hh, src/tgbaalgos/complete.hh,
      src/tgbaalgos/compsusp.hh, src/tgbaalgos/cycles.hh,
      src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh,
      src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.hh,
      src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness_stats.hh,
      src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/gtec.hh,
      src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.hh,
      src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.hh, src/tgbaalgos/isdet.hh,
      src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/magic.hh, src/tgbaalgos/mask.hh,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/product.hh, src/tgbaalgos/projrun.hh,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.hh,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.hh,
      src/tgbaalgos/relabel.hh, src/tgbaalgos/remfin.hh,
      src/tgbaalgos/replayrun.hh, src/tgbaalgos/safety.hh,
      src/tgbaalgos/sbacc.hh, src/tgbaalgos/scc.hh,
      src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.hh,
      src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.hh,
      src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.hh,
      src/tgbaalgos/stutter.hh, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.hh, src/tgbaalgos/translate.hh,
      src/tgbaalgos/weight.hh, src/tgbaalgos/word.hh,
      src/sanity/includes.test, src/tgbaalgos/ndfs_result.hxx: here.
      57cd9f2d
    • Etienne Renault's avatar
      Fix mac OSX support for echo -n. · b8bc619d
      Etienne Renault authored
      * configure.ac: here.
      b8bc619d
  4. 22 Mar, 2015 1 commit
  5. 21 Mar, 2015 2 commits
  6. 20 Mar, 2015 2 commits
  7. 18 Mar, 2015 8 commits
  8. 17 Mar, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      sat: add missing prop_state_based_acc() call · 72eed9b2
      Alexandre Duret-Lutz authored
      Fixes #62.
      
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Add call to
      prop_state_based_acc() when building an automaton with state-based
      acceptance.
      * src/tgbatest/satmin2.test: New test.
      * doc/org/satmin.org: Update.
      72eed9b2
    • Alexandre Duret-Lutz's avatar
      man: fix section number of spot-x.7 · 6712fa3c
      Alexandre Duret-Lutz authored
      * src/bin/man/Makefile.am: Make sure the header of spot-x.7 refers to
      section 7, not 1.  This error was caught by lintian on the Debian
      packages.
      6712fa3c
    • Alexandre Duret-Lutz's avatar
      dotty: colored acceptance sets · 838bfb2a
      Alexandre Duret-Lutz authored
      This implement several new options for --dot in order to
      allow emptiness sets to be output as colored ⓿ or ❶...
      Also add a SPOT_DOTDEFAULT environment variable.
      
      * NEWS, src/bin/man/spot-x.x, src/bin/common_aoutput.cc,
      src/bin/dstar2tgba.cc: Document the new options.
      * doc/org/.dir-locals.el, doc/org/init.el.in: Setup
      SPOT_DOTEXTRA and SPOT_DOTDEFAULT for all documents.
      * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org,
      doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org,
      doc/org/satmin.org: Adjust to this new setup.
      * src/misc/escape.cc, src/misc/escape.hh (escape_html): New function.
      * src/tgba/acc.cc, src/tgba/acc.hh (to_text, to_html): New method.
      * src/tgbaalgos/dotty.cc: Implement the new options.
      * src/tgbatest/readsave.test, wrap/python/tests/automata.ipynb: More
      tests.
      * wrap/python/spot.py: Make sure the default argument for
      dotty_reachable is None, so that SPOT_DOTDEFAULT is honored.
      838bfb2a
  9. 16 Mar, 2015 3 commits
  10. 15 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: some bindings for translating formulas and diplaying automata · 3c38780d
      Alexandre Duret-Lutz authored
      * wrap/python/spot.py: Introduce spot.translate (and
      spot.formula.translate) as well, as a wrapper around the
      spot.translator class.  Also implement spot.tgba.show()
      to allow passing argument to dotty_reachable() before
      the result is converted to SVG.
      * wrap/python/tests/automata.ipynb: New test file.
      * wrap/python/tests/Makefile.am: Add it.
      3c38780d
  11. 13 Mar, 2015 1 commit
  12. 11 Mar, 2015 5 commits
  13. 10 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] fix undefined behavior · 787e3f93
      Alexandre Duret-Lutz authored
      The bug was found while running Spot's src/tgbatest/randpsl.test
      on Debian i386 with gcc-4.9.2.  The following call would crash:
      
      ./ltl2tgba -R3 -t '(!(F(({{{(p0) |
      {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) &
      (G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))'
      
      On amd64 the call does not crash, but valgrind nonetheless
      report that uninitialized memory is being read by bdd_gbc()
      during the second garbage collect.
      
      * src/kernel.h (PUSHREF): Define as a function rather than a macro
      to avoid undefined behavior.  See comments for details.
      787e3f93
  14. 09 Mar, 2015 1 commit
  15. 08 Mar, 2015 1 commit