1. 03 Mar, 2010 2 commits
    • Alexandre Duret-Lutz's avatar
      Optimize tgba_tba_proxy and tgba_sba_proxy for states that share · 96cc3a3f
      Alexandre Duret-Lutz authored
      an acceptance condition on all outgoing transitions.
      
      This was motivated by experiments from Rüdiger Ehlers, showing
      that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a
      U (b U c)'".  With this change and the previous one, it is no
      longer the case.
      
      * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store
      a pointer to the source automaton and...
      (tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra
      optimization step to gather the acceptance conditions common
      to all outgoing transitions of the destination state, and pretend
      they are on the current (ingoing) transition.
      (tgba_tba_proxy::succ_iter): Pass the
      source automaton to the constructed iterator.
      * src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7.
      * src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'.
      96cc3a3f
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: apply -R3 before -D or -DS. · efb15a91
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
      degeneralization, because it might remove useless acceptance
      conditions.  I realized this while looking at experiments from
      Rüdiger Ehlers.
      efb15a91
  2. 24 Feb, 2010 1 commit
  3. 23 Feb, 2010 2 commits
    • Alexandre Duret-Lutz's avatar
      Work around a spurious style.test error. · 57d5eb3c
      Alexandre Duret-Lutz authored
      * src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi
      is the BibTex entry used as comment, because some version of sed
      will choke on non-ascii character and cause sanity/style.test to
      fail.
      57d5eb3c
    • Alexandre Duret-Lutz's avatar
      Fix random_graph() not to generate dead states. · 21832760
      Alexandre Duret-Lutz authored
      This is actually the third time I fix random_graph().  On
      2007-02-06 I changed the function not to generated dead states,
      but in a way that made it non-deterministic.  On 2010-01-20 I made
      the function deterministic again, but it started to generate dead
      states as a side effect.  This time, I'm making sure that dead
      states won't come again with a test-case that we should have had
      from the beginning.
      
      * src/tgbaalgos/randomgraph.cc (random_graph): Add an extra
      indirection array, state_randomizer[], so that we can reorder
      states indices after a random selection without actually changing
      the value of the indices used by unreachable_states and
      nodes_to_process.
      * src/tgbatest/randtgba.test: New file.
      * src/tgbatest/Makefile.am: Add randtgba.test.
      21832760
  4. 17 Feb, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      ltl2tgba cgi updates. · 72b7deec
      Alexandre Duret-Lutz authored
      * wrap/python/cgi-bin/ltl2tgba.in (dot): Use the value computed by
      configure.
      (os.system): Cleanup stale files only when the form has been
      submitted.
      (list options): Keep track of the selected value.
      (draw_acc_run|print_acc_run): set ec=0 to detect if it has been
      later set or not.  Fix error message when using generalized
      automata with degeneralized emptiness checks.
      * wrap/python/cgi-bin/Makefile.am (ltl2tgba.py): Substitute @DOT@.
      72b7deec
  5. 02 Feb, 2010 3 commits
  6. 01 Feb, 2010 2 commits
  7. 31 Jan, 2010 4 commits
    • Alexandre Duret-Lutz's avatar
      * doc/Makefile.am ($(srcdir)/stamp): Do not depend on dot · ca1bec30
      Alexandre Duret-Lutz authored
      explicitly, otherwise the documentation is always built and
      distcheck fails.
      ca1bec30
    • Alexandre Duret-Lutz's avatar
      More Doxygen fixes. · 34728dca
      Alexandre Duret-Lutz authored
      * src/sabaalgos/sabareachiter.hh (process_link): Document argument SI.
      * src/eltlparse/public.hh (format_parse_errors): Remove the
      non-existing eltl_string argument from the description.
      (parse_file): Fix name of parameters in documentation.
      34728dca
    • Alexandre Duret-Lutz's avatar
      Build doxygen pictures with libgd to reduce their size. · 5b87fa62
      Alexandre Duret-Lutz authored
      Doxygen only knows how to call dot with -Tpng, while using
      -Tpng:gd produces pictures that are 10 times smaller.  Use a
      simple wrapper around dot to simplify this.
      
      * doc/dot.in: New file, that wrap the system's dot and replace
      -Tpng by -Tpng:gd.
      * doc/Makefile.am ($(srcdir)/stamp): Depend on dot.
      * doc/Doxyfile.in: Update to 1.6.2.
      (DOT_PATH): Set to @srcdir@ to use doc/dot instead of the
      system's dot.
      * configure.ac: Find the absolute path of dot, and generate
      the doc/dot script.
      5b87fa62
    • Alexandre Duret-Lutz's avatar
      More Doxygen fixes. · c63923fa
      Alexandre Duret-Lutz authored
      * src/tgba/tgbakvcomplement.hh: Use \verbatim around the bibtex
      entry.
      * src/saba/sabacomplementtgba.hh: Use latin1.
      c63923fa
  8. 30 Jan, 2010 16 commits
  9. 29 Jan, 2010 5 commits
  10. 25 Jan, 2010 2 commits
  11. 24 Jan, 2010 2 commits
    • Guillaume Sadegh's avatar
      Fix copyrights. · 3a974d61
      Guillaume Sadegh authored
      * bench/Makefile.am, bench/gspn-ssp/Makefile.am,
      bench/gspn-ssp/defs.in, bench/scc-stats/Makefile.am,
      bench/split-product/Makefile.am, configure.ac,
      iface/Makefile.am, iface/gspn/Makefile.am, iface/gspn/ssp.hh,
      iface/nips/Makefile.am, iface/nips/common.cc,
      iface/nips/common.hh, iface/nips/dottynips.cc,
      iface/nips/nips.cc, iface/nips/nips.hh, src/Makefile.am,
      src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy,
      src/eltlparse/eltlscan.ll, src/eltlparse/fmterror.cc,
      src/eltlparse/parsedecl.hh, src/eltltest/Makefile.am,
      src/eltltest/defs.in, src/eltltest/nfa.cc, src/evtgba/evtgba.hh,
      src/evtgba/product.cc, src/evtgba/product.hh,
      src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaparse/Makefile.am,
      src/evtgbaparse/evtgbaparse.yy, src/evtgbatest/defs.in,
      src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
      src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
      src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
      src/evtgbatest/readsave.test, src/ltlast/atomic_prop.cc,
      src/ltlast/atomic_prop.hh, src/ltlast/binop.cc,
      src/ltlast/binop.hh, src/ltlast/constant.cc,
      src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
      src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
      src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh,
      src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlenv/declenv.cc,
      src/ltlenv/declenv.hh, src/ltlenv/environment.hh,
      src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
      src/ltltest/Makefile.am, src/ltltest/defs.in,
      src/ltltest/equals.cc, src/ltltest/equals.test,
      src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
      src/ltltest/parse.test, src/ltltest/parseerr.test,
      src/ltltest/randltl.cc, src/ltltest/readltl.cc,
      src/ltltest/reduccmp.test, src/ltltest/syntimpl.cc,
      src/ltltest/syntimpl.test, src/ltltest/tostring.cc,
      src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test, src/ltlvisit/basicreduce.cc,
      src/ltlvisit/clone.cc, src/ltlvisit/clone.hh,
      src/ltlvisit/contain.cc, src/ltlvisit/destroy.cc,
      src/ltlvisit/destroy.hh, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc,
      src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc, src/misc/bddalloc.cc,
      src/misc/bddop.cc, src/misc/bddop.hh, src/misc/freelist.hh,
      src/misc/hash.hh, src/misc/minato.cc, src/misc/minato.hh,
      src/misc/optionmap.cc, src/misc/timer.cc, src/misc/timer.hh,
      src/saba/Makefile.am, src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh, src/saba/saba.cc,
      src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
      src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
      src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am,
      src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
      src/sabatest/Makefile.am, src/sabatest/defs.in,
      src/sanity/Makefile.am, src/tgba/Makefile.am,
      src/tgba/bdddict.cc, src/tgba/bddprint.cc,
      src/tgba/formula2bdd.cc, src/tgba/state.hh,
      src/tgba/succiterconcrete.cc, src/tgba/taatgba.hh,
      src/tgba/tgba.hh, src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbacomplement.cc,
      src/tgba/tgbacomplement.hh, src/tgba/tgbaexplicit.cc,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
      src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc,
      src/tgba/tgbaunion.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/ltl2taa.cc,
      src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.cc,
      src/tgbaalgos/reductgba_sim.hh,
      src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/stats.cc,
      src/tgbaalgos/stats.hh, src/tgbaparse/Makefile.am,
      src/tgbaparse/tgbaparse.yy, src/tgbatest/Makefile.am,
      src/tgbatest/bddprod.test, src/tgbatest/complementation.cc,
      src/tgbatest/complementation.test, src/tgbatest/defs.in,
      src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
      src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
      src/tgbatest/explpro3.test, src/tgbatest/explpro4.test,
      src/tgbatest/explprod.cc, src/tgbatest/explprod.test,
      src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.cc,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.cc,
      src/tgbatest/mixprod.test, src/tgbatest/powerset.cc,
      src/tgbatest/readsave.cc, src/tgbatest/readsave.test,
      src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
      src/tgbatest/reductgba.test, src/tgbatest/taatgba.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test,
      src/tgbatest/tripprod.cc, src/tgbatest/tripprod.test,
      wrap/python/cgi/ltl2tgba.in, wrap/python/tests/ltl2tgba.py,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py:
      Fix copyrights.
      3a974d61
    • Alexandre Duret-Lutz's avatar
      Check that all directories are documented. · 06f0fe1d
      Alexandre Duret-Lutz authored
      * src/sanity/readme.test: For each AC_OUTPUT Makefile, check that
      the directory is documented in README.  Also skip non distributed
      directories in readme.test.
      * README: Fit on 80 columns.
      06f0fe1d