1. 30 Jan, 2010 14 commits
    • Alexandre Duret-Lutz's avatar
      Check for missing Copyright blurbs, and add them. · dd3ac6b4
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Check for missing Copyrights blurbs.
      * src/sanity/Makefile.am: Run style.test before includes.test.
      * iface/gspn/dcswave.test, iface/gspn/dcswaveeltl.test,
      iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test,
      iface/gspn/simple.test, iface/gspn/udcsefm.test,
      iface/gspn/udcseltl.test, iface/gspn/udcsfm.test,
      iface/gspn/udcsltl.test, iface/nips/nipstest/dotty.test,
      iface/nips/nipstest/emptiness.test, src/eltltest/acc.test,
      src/eltltest/nfa.test, src/saba/sabacomplementtgba.cc,
      src/sabatest/sabacomplementtgba.cc, src/tgbatest/eltl2tgba.test,
      src/tgbatest/taatgba.test: Add missing Copyright blurb.
      dd3ac6b4
    • Alexandre Duret-Lutz's avatar
      * NEWS: More text. · 91fee65a
      Alexandre Duret-Lutz authored
      91fee65a
    • Alexandre Duret-Lutz's avatar
      Touch up some doxygen comments and copyrights. · dac05027
      Alexandre Duret-Lutz authored
      * eltlparse/public.hh, saba/saba.hh, tgba/tgbakvcomplement.hh,
      tgba/tgbasafracomplement.hh, tgbaalgos/eltl2tgba_lacim.cc,
      tgbaalgos/eltl2tgba_lacim.hh, tgbaalgos/ltl2taa.hh: Comment
      changes.
      dac05027
    • Alexandre Duret-Lutz's avatar
      Add SCC pruning options to the CGI script. · a4766f2f
      Alexandre Duret-Lutz authored
      * wrap/python/cgi-bin/ltl2tgba.in: Add options to symbolically
      prune unaccepting SCCs in LaCIM, and explicitely pruns unaccepting
      SCCs in all algorithms.
      * src/tgbaalgos/reductgba_sim.hh: Conceal most of the file to
      SWIG.
      * wrap/python/spot.i: Include reductgba_sim.hh.
      a4766f2f
    • Alexandre Duret-Lutz's avatar
      322e1a01
    • Alexandre Duret-Lutz's avatar
      Make it possible to use the cgi script without installing a web · 4efde0d3
      Alexandre Duret-Lutz authored
      server.
      
      * wrap/python/cgi-bin/ltl2tgba.in: Starts a web server if the
      script is not called as a CGI.  Arrange to load libraries from
      the build directory.  Create the spotimg/ if needed when run as
      a web server.
      * wrap/python/cgi-bin/Makefile.am: Adjust build rule and clean
      the spotimg directory.
      * wrap/python/cgi-bin/README, NEWS: Update.
      4efde0d3
    • Alexandre Duret-Lutz's avatar
      More * -> & replacements. · 24cde3c2
      Alexandre Duret-Lutz authored
      * src/ltltest/parse.test, src/ltltest/syntimpl.test: Replace * by &.
      24cde3c2
    • Alexandre Duret-Lutz's avatar
      Remove the theoretically bogus "containment" option of ltl2tgba_fm. · dd71e37d
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
      Remove the containment option.
      * src/tgbafromfile.cc, src/tgbafromfile.hh: Remove the
      containment_ member.
      * src/tgbatest/ltl2tgba.cc (syntax): Remove -c option for
      FM algorithm, use it exclusively for TAA.
      dd71e37d
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbasafracomplement.hh: Add missing copyright and · 7cc2776d
      Alexandre Duret-Lutz authored
      fix some comments.
      7cc2776d
    • Alexandre Duret-Lutz's avatar
      Rename tgba_complement as tgba_kv_complement. · 7647ba0f
      Alexandre Duret-Lutz authored
      * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: Rename
      as...
      * src/tgba/tgbakvcomplement.hh, src/tgba/tgbakvcomplement.cc:
      ... these. It makes more sense since we also have
      tgba_safra_complement.
      * src/tgba/Makefile.am, src/tgbatest/complement.cc, NEWS: Adjust.
      7647ba0f
    • Alexandre Duret-Lutz's avatar
      Do not recognize "*" as "and". This leaves room for an · 85532dc8
      Alexandre Duret-Lutz authored
      implementation of rational operators in a future version.
      
      * src/ltlparse/ltlscan.ll: Do not recognize "*".
      * wrap/python/cgi-bin/ltl2tgba.in: Undocument it.
      * NEWS: Mention this.
      * src/tgbatest/kv.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/reductgba.test: Replace "*" by "&".
      85532dc8
    • Alexandre Duret-Lutz's avatar
      Make Couvreur/FM the default translation. · 55b693e1
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (syntax, main): Do it.
      * NEWS: Mention it.
      55b693e1
    • Alexandre Duret-Lutz's avatar
      Overhaul LaCIM's ELTL options. · 369e4c41
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (syntax, main): Introduce -le to select
      this algorithm and -lo to add the default LTL operators.  This
      replace the undocumented hack to add LTL operators when the
      formula with read for command-line, or the automaton was output
      for LBTT.
      * src/tgbatest/eltl2tgba.test, src/tgbatest/spotlbtt.test: Update
      call syntax.
      * NEWS: Mention -le, -lo, and -taa.
      369e4c41
    • Alexandre Duret-Lutz's avatar
      Touch up -R3b handling. · 9a43a06b
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (syntax): Move -R3b with the other
      LaCIM options.
      (main): Speak of "symbolic SCC pruning" instead of "deleting
      unaccepting SCC", and do that right after the translation, before
      degeneralization.  Also error out when -R3b is used on non
      symbolic automata.
      9a43a06b
  2. 29 Jan, 2010 5 commits
  3. 25 Jan, 2010 2 commits
  4. 24 Jan, 2010 7 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
    • Alexandre Duret-Lutz's avatar
      * README: Typo. · 9f41e397
      Alexandre Duret-Lutz authored
      9f41e397
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      2919b645
    • Guillaume Sadegh's avatar
      * src/sanity/readme.test: A script to check whether all the · cbdb0feb
      Guillaume Sadegh authored
      directories referenced in README exist.
      * src/sanity/Makefile.am: Adjust to call `readme.test' when make
      check is invoked.
      cbdb0feb
    • Guillaume Sadegh's avatar
      Update the README. · 3633fced
      Guillaume Sadegh authored
      * README: Reference src/saba/, src/sabaalgos/, src/sabatest/,
      iface/nips/, iface/nips/nipstest/ and iface/nips/nips_vm/.
      3633fced
  5. 22 Jan, 2010 6 commits
  6. 21 Jan, 2010 6 commits