1. 15 Apr, 2010 1 commit
  2. 14 Apr, 2010 2 commits
  3. 12 Apr, 2010 7 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      More LTL reductions for W and M. · e6809b8c
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc: Perform the following reductions:
      (a U b) & (c W b) = (a & c) U b
      (a W b) & (c W b) = (a & c) W b
      (a R b) | (c M b) = (a | c) R b
      (a M b) | (c M b) = (a | c) M b
      * src/ltltest/reduccmp.test: Test them.
      e6809b8c
    • Alexandre Duret-Lutz's avatar
      Add LTL reductions for strong release. · f003c3d1
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc: Perform the following reductions.
      a R (b & F(a)) = a M b
      a M (b & F(a)) = a M b
      a R Fa = Fa
      a M Fa = Fa
      a R b & Fa = a M b
      a R b & a M c = a M (b & c)
      a M b & a M c = a M (b & c)
      * src/ltltest/reduccmp.test: More tests.
      f003c3d1
    • Alexandre Duret-Lutz's avatar
      Add LTL reductions for weak until. · 80ceca59
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc: Perform the following reductions.
      a U (b | Ga) = a W b
      a W (b | Ga) = a W b
      a U b | Ga = a W b
      a U b | a W c = a W (b | c)
      a W b | a W c = a W (b | c)
      a U Ga = Ga
      a W Ga = Ga
      * src/ltltest/reduccmp.test: More tests.
      80ceca59
    • Alexandre Duret-Lutz's avatar
      Add support for W (weak until) and M (strong release) operators. · 0fc0ea31
      Alexandre Duret-Lutz authored
      * src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for
      these new operators.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them.
      * src/ltltest/reduccmp.test: Add new tests for W and M.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
      src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc,
      src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
      src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
      Add support for W and M.
      * src/tgbatest/ltl2neverclaim.test: Test never claim output
      using LBTT, this is more thorough.  Also we cannot use -N
      any more in the spotlbtt.test.
      * src/tgbatests/ltl2tgba.cc: Define M and W for ELTL.
      * src/tgbatest/ltl2neverclaim.test: Test W and M, and use
      -DS instead of -N, because lbtt-translate does not want
      to translate these operators for tools that masquerade as Spin.
      0fc0ea31
    • Alexandre Duret-Lutz's avatar
      [lbtt] Accept W and M in lbtt-translate --spot. · 35a57c6d
      Alexandre Duret-Lutz authored
      * src/SpotWrapper.cc: Translate W and M operators.
      35a57c6d
    • Alexandre Duret-Lutz's avatar
      Adjust ltl2tgba.py to call scc_filter() with the "full" option as · 60dbeb11
      Alexandre Duret-Lutz authored
      appropriate.
      
      * wrap/python/spot.i (spot::scc_filter): Make it available.
      * wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
      Use the "full" option unless the show_degen_png or
      show_never_claim are set.  Also reduce_scc the default.
      60dbeb11
  4. 08 Apr, 2010 3 commits
  5. 10 Mar, 2010 1 commit
  6. 07 Mar, 2010 1 commit
  7. 06 Mar, 2010 6 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
      * bench/ltl2tgba/formulae.ltl: Fix three formulae to match the · cc66aff6
      Alexandre Duret-Lutz authored
      original paper by Somenzi and Bloem.  Reported by Ruediger Ehlers.
      cc66aff6
    • 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
  8. 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
  9. 03 Mar, 2010 3 commits
    • Alexandre Duret-Lutz's avatar
      84058383
    • 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
  10. 24 Feb, 2010 1 commit
  11. 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
  12. 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
  13. 02 Feb, 2010 3 commits
  14. 01 Feb, 2010 2 commits
  15. 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