1. 07 Oct, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Hide the safra_tree_automaton type from the public interface. · 1fa1621a
      Alexandre Duret-Lutz authored
      We do that because the declaration of this type, which is local to
      src/tgba/tgbasafracomplement.cc has a member in an anonymous
      namespace, and some versions of g++-4.2 issue a very annoying
      warning about this legitimate code.  See Bug 29365 on GCC's
      Bugzilla.  Report by Silien Hong <silien.hong@lip6.fr>.
      * src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not
      forward declare.
      (tgba_safra_complement): Use void* instead of
      * src/tgba/tgbasafracomplement.cc: static_cast void* to
      safra_tree_automaton* anywhere needed.
  2. 21 Jun, 2010 1 commit
  3. 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
      * 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.
  4. 20 May, 2010 1 commit
  5. 16 Apr, 2010 3 commits
  6. 15 Apr, 2010 7 commits
  7. 14 Apr, 2010 2 commits
  8. 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.
    • 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.
    • 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.
    • 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.
    • 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.
    • Alexandre Duret-Lutz's avatar
      Adjust ltl2tgba.py to call scc_filter() with the "full" option as · 60dbeb11
      Alexandre Duret-Lutz authored
      * 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.
  9. 08 Apr, 2010 3 commits
  10. 10 Mar, 2010 1 commit
  11. 07 Mar, 2010 1 commit
  12. 06 Mar, 2010 6 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Reverse the order of expected acceptance conditions in · 58b233db
      Alexandre Duret-Lutz authored
      * 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.
    • 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.
    • 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.
    • 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.
    • 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
      * 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
      * src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
      the degeneralization worse than -R3.
  13. 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.
    • 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):
      * src/tgbatest/ltl2tgba.test: More tests.
    • 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.
  14. 03 Mar, 2010 3 commits
    • Alexandre Duret-Lutz's avatar
    • 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)'.
    • 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.