1. 18 Dec, 2011 1 commit
  2. 16 Dec, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Don't rely on the g++ version to include tr1/unordered_map and co. · 96790325
      Alexandre Duret-Lutz authored
      The previous setup failed with clang++ 3.0.
      
      * m4/stl.m4: New file.
      * configure.ac: Call AC_HEADER_UNORDERED_MAP,
      AC_HEADER_TR1_UNORDERED_MAP, and AC_HEADER_EXT_HASH_MAP.
      * src/misc/hash.hh: Include _config.h, and used the
      SPOT_HAVE_UNORDERED_MAP, SPOT_HAVE_TR1_UNORDERED_MAP,
      or SPOT_HAVE_EXT_HASH_MAP defines to decide which
      file to include.
      96790325
  3. 28 Nov, 2011 3 commits
  4. 24 Nov, 2011 1 commit
    • Thomas Badie's avatar
      Add text I/O for Kripke structures. · bb5949f6
      Thomas Badie authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files.
      * src/kripke/Makefile.am: Add them.
      * src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy,
      src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh,
      src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New
      files.
      * src/kripkeparse/Makefile.am: Add them.
      * src/kripketest/bad_parsing.test, src/kripketest/defs.in,
      src/kripketest/kripke.test, src/kripketest/origin,
      src/kripketest/parse_print_test.cc: New files.
      * src/kripketest/Makefile.am: Add them.
      * src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest.
      * README: Document src/kripketest/ and src/kripkeparse/.
      * configure.ac: Generate src/kripkeparse/Makefile,
      src/kripketest/Makefile, src/kripketest/defs.
      * iface/dve2/defs.in (run2): New function.
      * iface/dve2/dve2check.cc (syntax, main): Add option -gK.
      * iface/dve2/kripke.test: New file.
      * iface/dve2/Makefile.am (TESTS): Add kripke.test.
      bb5949f6
  5. 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
  6. 10 Apr, 2011 1 commit
  7. 03 Apr, 2011 1 commit
  8. 07 Mar, 2011 2 commits
  9. 05 Mar, 2011 2 commits
  10. 07 Feb, 2011 3 commits
  11. 01 Feb, 2011 2 commits
  12. 18 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Preliminary implementation of an ajax-based ltl2tgba translator. · 34f49a86
      Alexandre Duret-Lutz authored
      * configure.ac: Output wrap/python/ajax/Makefile.
      * wrap/python/Makefile.am (SUBDIRS): Add ajax.
      * wrap/python/ajax/Makefile.am, wrap/python/ajax/README,
      wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files.
      * wrap/python/ajax/css/, wrap/python/ajax/js,
      wrap/python/ajax/logos: New directories.
      * README: Document wrap/python/ajax/.
      34f49a86
  13. 05 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Add a WDBA benchmark. · edc71b80
      Alexandre Duret-Lutz authored
      * bench/wdba/: New directory.
      * bench/Makefile.am (SUBDIRS): Add wdba.
      * NEWS: Mention it.
      * configure.ac: Output bench/wdba/defs and bench/wdba/Makefile.
      edc71b80
  14. 24 Dec, 2010 1 commit
  15. 04 Dec, 2010 1 commit
  16. 06 Nov, 2010 2 commits
    • Alexandre Duret-Lutz's avatar
      Cleanup neverclaim support. · ac08c5ab
      Alexandre Duret-Lutz authored
      * src/neverclaimparse/: Shorthen as ...
      * src/neverparse/:... this.
      * src/Makefile.am: Adjust, and add back the directories mistakenly
      removed by previous patch.
      * README: Adjust, and keep the file's width under 80 columns.
      * configure.ac: Adjust.
      * src/neverparse/Makefile.am, src/neverparse/fmterror.cc,
      src/neverparse/neverclaimparse.yy,
      src/neverparse/neverclaimscan.ll, src/neverparse/public.hh:
      Fix copyright.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread.
      * src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim.
      * src/tgbatest/readneverclaim.cc: Delete.
      * src/tgbatest/neverclaimread.test: Use ltl2tgba instead of
      neverclaimread.
      ac08c5ab
    • Felix Abecassis's avatar
      Add never claim parser. · ab6ec5cb
      Felix Abecassis authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/neverclaimparse/: New directory.
      * src/neverclaimparse/fmterror.cc: New file.  Print a formatted parse
      error on a output stream.
      * src/neverclaimparse/neverclaimparse.yy: New file.  Parser declaration
      for Bison.
      * src/neverclaimparse/neverclaimscan.ll: New file.  Scanner declaration
      for Flex.
      * src/neverclaimparse/public.hh: New file.  Public header for external
      use.
      * src/neverclaimparse/parsedecl.hh: New file.  Header file for
      Flex-Bison interaction.
      * src/neverclaimparse/Makefile.am: New Makefile.
      * src/tgbatest/neverclaimread.cc: New file.  Test program for the
      never claim parser.
      * src/tgbatest/neverclaimread.test: New file.  Test script for the
      never claim parser.
      * src/tgbatest/Makefile.am: Adjust.
      * configure.ac : Adjust.
      * README: Adjust.
      ab6ec5cb
  17. 07 Oct, 2010 1 commit
  18. 21 Jun, 2010 1 commit
  19. 25 May, 2010 1 commit
    • Felix Abecassis's avatar
      Add never claim parser. · 9aaa638b
      Felix Abecassis authored
      * src/neverclaimparse/: New directory.
      * src/neverclaimparse/fmterror.cc: New file.  Print a formatted parse
      error on a output stream.
      * src/neverclaimparse/neverclaimparse.yy: New file.  Parser declaration
      for Bison.
      * src/neverclaimparse/neverclaimscan.ll: New file.  Scanner declaration
      for Flex.
      * src/neverclaimparse/public.hh: New file.  Public header for external
      use.
      * src/neverclaimparse/parsedecl.hh: New file.  Header file for
      Flex-Bison interaction.
      * src/neverclaimparse/Makefile.am: New Makefile.
      * src/tgbatest/neverclaimread.cc: New file.  Test program for the
      never claim parser.
      * src/tgbatest/neverclaimread.test: New file.  Test script for the
      never claim parser.
      * src/tgbatest/Makefile.am: Adjust.
      * configure.ac : Adjust.
      * README: Adjust.
      9aaa638b
  20. 16 Apr, 2010 2 commits
  21. 01 Feb, 2010 2 commits
  22. 31 Jan, 2010 1 commit
    • 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
  23. 29 Jan, 2010 2 commits
  24. 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
  25. 30 Nov, 2009 1 commit
    • Guillaume Sadegh's avatar
      Add a new type of automata: State-labeled Alternating Büchi · 7cb6ff33
      Guillaume Sadegh authored
      Automata (SABA).
      
      * src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh,
      src/saba/sabasucciter.hh: New.  Interface for
      SABA (State-labeled Alternating Büchi Automata).
      * src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh: New.  Default
      implementation for a conjunction of states.
      * src/saba/Makefile.am: New.
      * src/Makefile.am, configure.ac: Adjust.
      * src/sabaalgos/sabareachiter.cc,
      src/sabaalgos/sabareachiter.hh: New.  Iterate over all reachable
      states of a spot::saba.
      * src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh: New.
      Print reachable states in dot format.
      * src/sabaalgos/Makefile.am: New.
      7cb6ff33
  26. 09 Nov, 2009 2 commits
  27. 02 Sep, 2009 2 commits
    • Alexandre Duret-Lutz's avatar
      Use Automake 1.11's parallel-tests feature. · 1098c62d
      Alexandre Duret-Lutz authored
      * configure.ac: Enable parallel-tests.
      * src/eltltest/defs.in, src/evtgbatest/defs.in,
      src/ltltest/defs.in, src/tgbatest/defs.in: Always output verbose
      tests.  Make a subdirectory for each test case.
      * src/ltltest/Makefile.am, src/eltltest/Makefile.am,
      src/tgbatest/Makefile.am, src/evtgbatest/Makefile.am: Remove
      CLEANFILES and clean the test subdirectories in a distclean-local
      rule instead.
      * src/eltltest/acc.test, src/eltltest/nfa.test,
      src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.test,
      src/evtgbatest/product.test, src/evtgbatest/readsave.test,
      src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/reduc.test,
      src/ltltest/reduccmp.test, src/ltltest/syntimpl.test,
      src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test, src/tgbatest/bddprod.test,
      src/tgbatest/complementation.test, src/tgbatest/dfs.test,
      src/tgbatest/dupexp.test, src/tgbatest/eltl2tgba.test,
      src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
      src/tgbatest/emptchkr.test, src/tgbatest/explicit.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
      src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
      src/tgbatest/readsave.test, src/tgbatest/reduccmp.test,
      src/tgbatest/reductgba.test, src/tgbatest/scc.test,
      src/tgbatest/spotlbtt.test, src/tgbatest/tgbaread.test,
      src/tgbatest/tripprod.test: Adjust to run from a subdirectory.
      1098c62d
    • Alexandre Duret-Lutz's avatar