1. 28 Nov, 2011 1 commit
  2. 28 Aug, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Improve SCC simplification by removing implied acceptance conditions. · d9fc75e9
      Alexandre Duret-Lutz authored
      Spot 0.7.1 used to need 190 acceptance conditions to translate the
      188 literature formulae.  With this patch we are down to 185.
      That's not an impressive, but there are only ~20 formulae that
      require more than 1 acceptance conditions; hence little room for
      improvement.
      
      * src/misc/bddlt.hh (bdd_hash): New function.
      * src/misc/accconv.hh, src/misc/accconv.cc: New files.
      * src/misc/Makefile.am: Add them.
      * src/tgbaalgos/scc.cc (scc_map::build_map): Adjust
      to record all combination of acceptance conditions occurring in a SCC.
      * src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description.
      * src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance
      conditions that are always implied by another acceptance
      conditions.  Previously, we only removed acceptance conditions
      that where always present in accepting SCCs.
      * src/tgbatest/sccsimpl.test: New file.
      * src/tgbatest/Makefile.am (TESTS): Add it.
      d9fc75e9
  3. 08 Jun, 2011 1 commit
  4. 06 Jun, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Install a misc/_config.h to hide all the defines that clutter the · 67ff9f20
      Alexandre Duret-Lutz authored
      built output.
      
      This is also a step towards better checks for things like
      __attribute__ or std::tr1.
      
      * m4/ax_prefix_config_h.m4: New file.
      * configure.ac: Call AC_CONFIG_HEADERS and AX_PREFIX_CONFIG_H.
      * src/misc/Makefile.am: Install misc/_config.h.
      * src/misc/random.cc, src/misc/version.cc: Include misc/_config.h.
      67ff9f20
  5. 18 May, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Some intvcomp2 speedups. · 290b825a
      Alexandre Duret-Lutz authored
      * src/misc/intvcmp2.cc (stream_compression_base::run):
      Implement a shift-less encoding for the 1-bit and 3-bit cases.
      Also declare offsets as size_t, to help 64-bit compilers.
      290b825a
  6. 16 May, 2011 1 commit
  7. 05 May, 2011 2 commits
  8. 02 May, 2011 1 commit
  9. 15 Apr, 2011 1 commit
  10. 13 Apr, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix compression of large repetitions · 445a785e
      Alexandre Duret-Lutz authored
      * src/misc/intvcomp.cc (stream_compression_base::run): Limit
      repeatitions to 40, not 42.
      (stream_decompression_base::refill): Refill the end of the stream
      with 0.
      (stream_decompression_base::look_n_bits): Add assertion.
      * src/tgbatest/intvcomp.cc: Add a new test case.
      445a785e
  11. 12 Apr, 2011 1 commit
  12. 10 Apr, 2011 1 commit
  13. 09 Apr, 2011 5 commits
  14. 03 Apr, 2011 1 commit
  15. 31 Mar, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Introduct a down_cast macro. · 9f63bb66
      Alexandre Duret-Lutz authored
      * src/misc/casts.hh: New file.
      * src/misc/Makefile.am: Add it.
      * iface/dve2/dve2.cc, iface/gspn/gspn.cc, iface/gspn/ssp.cc,
      src/evtgba/explicit.cc, src/evtgba/product.cc, src/misc/casts.hh,
      src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/taatgba.cc,
      src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbaproduct.cc,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
      src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reductgba_sim.cc,
      src/tgbaalgos/reductgba_sim_del.cc: Use down_cast when
      appropriate.
      9f63bb66
  16. 07 Mar, 2011 2 commits
    • Alexandre Duret-Lutz's avatar
      Clear the timer map to help valgrind. · 0584d278
      Alexandre Duret-Lutz authored
      * src/misc/timer.hh (reset_all): New method.
      * iface/dve2/dve2check.cc: Use it to help valgrind.
      0584d278
    • Alexandre Duret-Lutz's avatar
      Allow atomic propositions and identifiers like `X.Y'. · 4a622249
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlscan.ll: Do not recognize `.' as an AND.  Allow
      it in atomic propositions.
      * src/evtgbaparse/evtgbascan.ll, src/tgbaparse/tgbascan.ll: Accept
      `.' in identifiers.
      * src/misc/bareword.cc (is_bareword): Accept `.' inside
      barewords, so that there is no need to quote `X.Y'.
      * src/ltltest/parse.test: Do not use `.' as and operator..
      4a622249
  17. 21 Feb, 2011 1 commit
  18. 12 Jan, 2011 1 commit
  19. 24 Jan, 2010 1 commit
    • 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
  20. 11 Dec, 2009 1 commit
  21. 24 Nov, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      Detect running timers, and stop a timer in ltl2tgba. · b796bb3d
      Alexandre Duret-Lutz authored
      * src/misc/timer.hh (time_info::running): New attribute.
      (time_info::start, time_info::stop): Update and check
      time_info::running.
      * src/misc/timer.cc (timer_map::print): Mark running timers with
      a "+" in the output.
      * src/tgbatest/ltl2tgba.cc (main): Rename the name of the timers
      for SCC and simulation reduction, and actually stop the SCC timer.
      b796bb3d
  22. 23 Nov, 2009 1 commit
  23. 20 Nov, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      Strip useless acceptance conditions in scc_filter(). · dfb9c662
      Alexandre Duret-Lutz authored
      A useless acceptance conditions is one that is always implied by
      another.
      
      * src/misc/bddop.hh, src/misc/bddop.cc
      (compute_neg_acceptance_conditions): New function.
      * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
      (set_acceptance_conditions): New function.
      * src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot):
      Keep track of useful acceptance conditions.
      (useful_acc_of): New function.
      * src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New
      attributes.
      * src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter
      useless acceptance conditions.
      (scc_filter): Compute useful acceptance conditions and pass them
      to filter_iter.
      dfb9c662
  24. 16 Oct, 2009 2 commits
    • Damien Lefortier's avatar
      Minor fixes. · 84060b49
      Damien Lefortier authored
      * src/misc/bddop.hh, src/tgba/taa.hh, src/tgbaalgos/ltl2taa.hh:
      Fix sanity (incorrect include guard).
      * src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh:
      Copyright 2009.
      * src/tgbaalgos/eltl2tgba_lacim.cc: Use abbreviations.
      * src/tgbatest/taa.cc: Fix it.
      84060b49
    • Damien Lefortier's avatar
      Add a class to represent Transition-based Alternating Automata (TAA). · 20c1f01e
      Damien Lefortier authored
      * misc/Makefile.am, misc/bbop.cc, misc/bddop.hh: Factorize some
      code on BDDs to compute all_acceptance_conditions from
      neg_acceptance_condition.
      * src/tgba/Makefile.am, src/tgbatest/Makefile.am: Adjust.
      * src/tgba/taa.cc, src/tgba/taa.hh: The TAA class.
      * src/tgba/tgbaexplicit.hh: Use the factorized code in bddop.hh.
      * src/tgbatest/taa.cc, src/tgbatest/taa.test: Some test cases.
      20c1f01e
  25. 18 Dec, 2008 1 commit
  26. 25 Mar, 2008 2 commits
  27. 21 Mar, 2008 2 commits
  28. 14 Mar, 2008 2 commits
    • Alexandre Duret-Lutz's avatar
      Make sure Spot compiles with g++-4.3. · d3b702a9
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh (hash): Remove const from return type.
      This kills a g++-4.3 warning.
      * src/misc/hash.hh: Adjust to use unordered_set and unordered_map
      from TR1 when g++-4.3 is used.
      * src/evtgba/product.cc, src/ltltest/randltl.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/tostring.cc,
      src/misc/freelist.hh, src/misc/optionmap.cc,
      src/tgba/tgbareduc.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/randomgraph.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
      src/ltltest/equals.cc, src/ltltest/readltl.cc,
      src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
      src/ltltest/tostring.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/powerset.cc, src/tgbatest/explprod.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc,
      src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc,
      src/tgbatest/tripprod.cc, src/evtgbatest/product.cc,
      src/evtgbatest/readsave.cc, src/evtgbatest/ltl2evtgba.cc,
      src/evtgbatest/readsave.cc: Add missing includes.
      * src/tgbatest/explicit.test, src/tgbatest/explprod.test,
      src/tgbatest/explpro2.test, src/tgbatest/troprod.test,
      src/tgbatest/emptchk.test: Cope with different outputs.
      d3b702a9
    • Alexandre Duret-Lutz's avatar
      Add .gitignore files · 5ef7084b
      Alexandre Duret-Lutz authored
      5ef7084b
  29. 25 Feb, 2008 2 commits