1. 23 Aug, 2014 2 commits
  2. 22 Aug, 2014 3 commits
  3. 21 Aug, 2014 10 commits
  4. 20 Aug, 2014 9 commits
  5. 19 Aug, 2014 6 commits
  6. 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.
      bc2e68f8
    • 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
      once.
      
      * 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.
      b360b022
  7. 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
      25sec.
      
      * src/tgbatest/checkpsl.cc: New file.
      * src/tgbatest/Makefile.am: Add it.
      * src/tgbatest/ltl2tgba.test: Adjust.
      9502266f
    • 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.
      6a741189
    • 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
      equalsf.cc.
      * src/ltltest/reduccmp.test: Rewrite.
      * src/ltltest/uwrm.test: Also rewrite, and use valgrind.
      7b9f6952
  8. 15 Aug, 2014 4 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.
      b43f75e9
    • 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.
      e3b5119f
    • Alexandre Duret-Lutz's avatar
      Fix some bdd_dict_ptr not being passed by const reference. · bf6c9067
      Alexandre Duret-Lutz authored
      * iface/dve2/dve2.cc, iface/dve2/dve2.hh,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
      src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
      src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/formula2bdd.cc,
      src/tgba/formula2bdd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh,
      src/tgba/tgbagraph.hh, src/tgbaalgos/compsusp.cc,
      src/tgbaalgos/compsusp.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/translate.cc,
      src/tgbaalgos/translate.hh, src/tgbaalgos/word.cc,
      src/tgbaalgos/word.hh: Pass shared_ptr to functions by const ref.
      bf6c9067
    • Alexandre Duret-Lutz's avatar
      Handle all automata through shared_ptr. (monstro patch) · 51151ab2
      Alexandre Duret-Lutz authored
      A type such as 'const tgba_digraph*' and 'tgba_digraph*' are replaced
      by 'const_tgba_digraph_ptr' and 'tgba_digraph_ptr'.  Additionally 'new
      tgba_digraph(...)' is replaced by 'make_tgba_digraph(...)'.
      
      This convention is followed by all automata types. Those smart
      pointers should normally be passed by const reference as input of
      function to avoid the atomic increments/decrements, but I probably
      missed a few, as this huge patch took me nearly 12h.
      
      * src/kripke/fwd.hh, src/tgba/fwd.hh: New files.
      * src/kripke/Makefile.am, src/tgba/Makefile.am: Adjust.
      * iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
      src/bin/common_output.hh, src/bin/dstar2tgba.cc,
      src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
      src/bin/ltlfilt.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/dstar2tgba.cc, src/dstarparse/dstarparse.yy,
      src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
      src/dstarparse/public.hh, src/graphtest/tgbagraph.cc,
      src/kripke/fairkripke.hh, src/kripke/kripke.hh,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh,
      src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
      src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/contain.hh, src/neverparse/neverclaimparse.yy,
      src/neverparse/public.hh, src/priv/accmap.hh,
      src/priv/countstates.cc, src/priv/countstates.hh, src/saba/saba.hh,
      src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
      src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
      src/sabatest/sabacomplementtgba.cc, src/ta/ta.hh,
      src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
      src/ta/taproduct.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
      src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc,
      src/ta/tgtaproduct.hh, src/taalgos/dotty.cc, src/taalgos/dotty.hh,
      src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
      src/taalgos/minimize.cc, src/taalgos/minimize.hh,
      src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
      src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
      src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
      src/taalgos/tgba2ta.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/formula2bdd.hh, src/tgba/futurecondcol.cc,
      src/tgba/futurecondcol.hh, src/tgba/taatgba.hh, src/tgba/tgba.cc,
      src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
      src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc,
      src/tgba/tgbaproxy.hh, src/tgba/tgbasafracomplement.cc,
      src/tgba/tgbasafracomplement.hh, src/tgba/tgbascc.cc,
      src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh,
      src/tgba/wdbacomp.cc, src/tgba/wdbacomp.hh,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
      src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.cc,
      src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dottydec.cc,
      src/tgbaalgos/dottydec.hh, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.cc,
      src/tgbaalgos/dtgbacomp.hh, src/tgbaalgos/dtgbasat.cc,
      src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/gtec.cc,
      src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/status.cc,
      src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.cc,
      src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.cc,
      src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.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/safety.cc,
      src/tgbaalgos/safety.hh, src/tgbaalgos/save.cc,
      src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh,
      src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh,
      src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
      src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/explprod.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/maskacc.cc, src/tgbatest/powerset.cc,
      src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
      wrap/python/ajax/spot.in, wrap/python/spot.i,
      wrap/python/tests/interdep.py: Use shared pointers for automata.
      51151ab2
  9. 14 Aug, 2014 1 commit