1. 24 Aug, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      python: add an SVG printer for automata · baf644a9
      Alexandre Duret-Lutz authored
      * wrap/python/spot.i (tgba._repr_svg_): Call dot to
      output SVG using the same logic as in Vaucanson 2.
    • Alexandre Duret-Lutz's avatar
      Better formula I/O for ipython. · ae35cc29
      Alexandre Duret-Lutz authored
      * src/ltlparse/public.hh, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll (parse_error): New class.
      (parse_formula): New function that raises a parse_error
      exception on error.
      * src/ltlvisit/tostring.hh, src/ltlvisit/tostring.cc:
      (to_sclatex_string): New method.
      * wrap/python/spot.i: Catch the parser_error exception,
      and use the to_sclatex_string for MathJax rendering.
      * wrap/python/tests/run.in: Start ipython on demand.
  2. 23 Aug, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      Use shared_ptr for the emptiness check interfaces. · 6d7c258f
      Alexandre Duret-Lutz authored
      At the same time, this adds a is_empty() method to the tgba class,
      simplifying many places that ran emptiness checks.
      * iface/dve2/dve2check.cc, src/bin/ltlcross.cc,
      src/dstarparse/dra2ba.cc, src/ltlvisit/contain.cc, src/tgba/tgba.cc,
      src/tgba/tgba.hh, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
      src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/gtec.cc,
      src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/gv04.hh, src/tgbaalgos/magic.cc,
      src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh,
      src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh,
      src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/word.cc, src/tgbaalgos/word.hh,
      src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc,
      src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc, wrap/python/ajax/spot.in,
      wrap/python/spot.i: Use shared_ptr.
    • Alexandre Duret-Lutz's avatar
      apcollect: Fix prototype. · 803e17bb
      Alexandre Duret-Lutz authored
      * src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: Take automaton
      by reference.
    • Alexandre Duret-Lutz's avatar
      Remove useless forward declarations of class tgba. · c3c02bfb
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/compsusp.hh, src/tgbaalgos/dotty.hh,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/hoaf.hh,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/randomgraph.hh,
      src/tgbaalgos/simulation.hh: Here.
  3. 22 Aug, 2014 3 commits
  4. 21 Aug, 2014 10 commits
  5. 20 Aug, 2014 9 commits
  6. 19 Aug, 2014 6 commits
  7. 18 Aug, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      tgbatest: rewrite emptchk.test in C++ · bc2e68f8
      Alexandre Duret-Lutz authored
      So that its run time goes from 10min+ to ~5s.
      * src/tgbatest/emptchk.cc: New file.
      * src/tgbatest/Makefile.am: Add it.
      * src/tgbatest/emptchk.test: Use it.
    • Alexandre Duret-Lutz's avatar
      tgbatest: speed ltl2ta.test up! · b360b022
      Alexandre Duret-Lutz authored
      Again instead of calling ltl2tgba dozen of times with different options
      for various formulas, this implements a single executable that reads
      formulas from a file, translate them using the different setups, and
      dump statistics for comparison.  Valgrind now only has to be started
      * src/tgbatest/checkta.cc: New file.
      * src/tgbatest/Makefile.am: Use it.
      * src/tgbatest/ltl2ta.test: Rewrite using checkta.
      * src/tgbatest/ltl2tgba.cc: Remove a unused variable.
  8. 17 Aug, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      tgbatest: implement a large part of ltl2tgba.test in c++ · 9502266f
      Alexandre Duret-Lutz authored
      So that running valgrind is a lot more efficient.  Running
      ltl2tgba.test using to take more than 15min.  We are now down to
      * src/tgbatest/checkpsl.cc: New file.
      * src/tgbatest/Makefile.am: Add it.
      * src/tgbatest/ltl2tgba.test: Adjust.
    • Alexandre Duret-Lutz's avatar
      ltltest: speedup more tests · 6a741189
      Alexandre Duret-Lutz authored
      This generalizes the previous patch.
      * src/ltltest/equalsf.cc: Allow escaped '\,' and
      negated result.
      * src/ltltest/Makefile.am: Use equalsf.cc for
      almost all tests that used equals.cc.
      (nequals): New.
      * src/ltltest/equals.test, src/ltltest/eventuniv.test,
      src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
      src/ltltest/parseerr.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test: Adjust.
    • Alexandre Duret-Lutz's avatar
      Speedup reduccmp.test · 7b9f6952
      Alexandre Duret-Lutz authored
      This test used to take more than 10min because an instance of valgrind
      was launched for each separate equivalence check.  The list of
      equivalences to checks are not given in a file, and only two valgrind
      instances are run.  The test takes less than 15sec.
      * src/ltltest/equalsf.cc: New file.
      * src/ltltest/Makefile.am (reduccmp, reductaustr): Build using
      * src/ltltest/reduccmp.test: Rewrite.
      * src/ltltest/uwrm.test: Also rewrite, and use valgrind.
  9. 15 Aug, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      tgba: move boolean properties from tgba_digraph to tgba · b43f75e9
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.hh: Remove the set_bprop/get_bprop interface.
      * src/tgba/tgba.cc, src/tgba/tgba.hh: Add a new interface for
      setting/querying/copying the following properties: single_acc_set,
      state_based_acc, inherently_weak, deterministic.
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/neverparse/neverclaimparse.yy, src/saba/sabacomplementtgba.cc,
      src/tgba/tgbagraph.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/isdet.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/postproc.cc, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/simulation.cc, src/tgbatest/degenlskip.test,
      src/tgbatest/ltl2tgba.cc: Adjust to the new interface, or use
      it to bypass some useless work.
    • Alexandre Duret-Lutz's avatar
      degen: return input if it is already degeneralized · e3b5119f
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/degen.cc (degeneralize, degeneralize_tba): Shortcut
      degeneralization if the automaton is already degeneralized.