1. 08 Apr, 2010 2 commits
  2. 10 Mar, 2010 1 commit
  3. 07 Mar, 2010 1 commit
  4. 06 Mar, 2010 5 commits
    • Alexandre Duret-Lutz's avatar
      629dc4c0
    • Alexandre Duret-Lutz's avatar
      Reverse the order of expected acceptance conditions in · 58b233db
      Alexandre Duret-Lutz authored
      degeneralization.
      
      * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_tba_proxy): Build the
      list of acceptance condition in the reverse order.  The order is
      still arbitrary, but the bdd_satone() call seems to output the
      acceptance conditions that are more used first, and this helps the
      degeneralization process.
      58b233db
    • Alexandre Duret-Lutz's avatar
      Tweak precedence of "->" and <->. · 351a8076
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlparse.yy: Change the precedence of "->" and
      "<->" so that "a & b -> c" is interpreted as "(a & b) -> c"
      instead of "a & (b -> c)".  The new interpretation is more
      intuitive, and matches that of LBTT.
      351a8076
    • Alexandre Duret-Lutz's avatar
      Fix memory leak introduced in yesterday's change. · 975045a4
      Alexandre Duret-Lutz authored
      * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Do not
      forget to free the initial state after usage.
      975045a4
    • Alexandre Duret-Lutz's avatar
      Keep acceptance conditions on transitions going to accepting SCCs · 27b419ce
      Alexandre Duret-Lutz authored
      by default in scc_filter().
      
      Doing so helps the degeneralization algorithm, because it will
      have more opportunity to be in an accepting level when it reaches
      the accepting SCCs.
      
      * src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a
      remove_all_useless argument.
      (filter_iter::process_link): Use the flag to decide whether to
      filter acceptance conditions going to accepting SCCs.
      (scc_filter): Take a remove_all_useless argument and pass it to
      filter_iter.
      * src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument
      and document the function.
      * src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3
      for remove_all_useless=false and add -R3f for
      remove_all_useless=true.
      * src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
      the degeneralization worse than -R3.
      27b419ce
  5. 05 Mar, 2010 3 commits
    • Alexandre Duret-Lutz's avatar
      Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). · 21402560
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace
      the FG(a)|FG(b) == FG(a|b) rule by the above more generic one.
      Add the dual rule for G(a)&G(b), as we had none (this one won't
      improve anything in the translation, but it is more symmetric
      this way).  Also simplify some pointer checks.
      21402560
    • Alexandre Duret-Lutz's avatar
      Better selection of the acceptance of the initial state in SBA. · 34af3287
      Alexandre Duret-Lutz authored
      * src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set
      cycle_start_ to start in the accepting layer of the degeneralized
      automaton if the initial state has an accepting self-loop.
      Otherwise, starts at the level of the first acceptance condition
      as previously.
      (tgba_sba_proxy::get_init_state): Use cycle_start_.
      * src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so
      that we can use it in tgba_sba_proxy::tgba_sba_proxy.
      (tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state):
      Declare.
      * src/tgbatest/ltl2tgba.test: More tests.
      34af3287
    • Alexandre Duret-Lutz's avatar
      Generalize the previous patch to accepting states in SBA. · 52faa81a
      Alexandre Duret-Lutz authored
      * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::sync_): Move
      the optimization step added by the previous patch outside the
      before the bddtrue check, so that it also applies to accepting
      states in SBA.
      52faa81a
  6. 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
  7. 24 Feb, 2010 1 commit
  8. 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
  9. 31 Jan, 2010 2 commits
    • 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
      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
  10. 30 Jan, 2010 13 commits
    • Alexandre Duret-Lutz's avatar
      Replace spot::ltl_file by a rewritten spot::ltl::ltl_file. · 4ff875f4
      Alexandre Duret-Lutz authored
      * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: Delete these
      files.
      * src/tgba/Makefile.am: Remove them.
      * src/ltl/ltlparse/ltlfile.hh, src/ltl/ltlparse/ltlfile.cc: New
      files.
      * src/ltl/ltlparse/Makefile.am: Add them.
      * bench/scc-stats/stats.cc, bench/split-product/cutscc.cc: Rewrite
      using the new class.
      4ff875f4
    • 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
      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
      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
  11. 29 Jan, 2010 3 commits
  12. 24 Jan, 2010 4 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
    • 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
  13. 22 Jan, 2010 1 commit