1. 28 Apr, 2012 40 commits
    • Alexandre Duret-Lutz's avatar
      Speedup minimize_obligation() when f->is_syntactic_obligation(). · 98f67973
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize_obligation): Do not check
      the output of minimize_wdba if the input formula is a syntactic
      obligation.
      98f67973
    • Alexandre Duret-Lutz's avatar
      Add documentation for temporal logic operators. · c483053a
      Alexandre Duret-Lutz authored
      * doc/tl/Makefile.am, doc/tl/tl.tex, doc/tl/tl.bib: New files.
      * doc/Makefile.am (SUBDIRS): Recurse into tl/.
      * configure.ac: Output doc/tl/Makefile
      * README: Describe doc/tl/.
      c483053a
    • Alexandre Duret-Lutz's avatar
      Trim DFAs used when translating PSL's closure operators. · b3cc033e
      Alexandre Duret-Lutz authored
      This fixes a bug where {(a&!a)[=2]} was translated either into an
      universal automaton (with simplification turned off) or in an
      empty automaton (with simplification turned on).
      
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Trim
      the automaton.
      (ratexp_to_dfa::succ, ratexp_to_dfa::get_label): Deal with trimed
      states.
      (ltl_trad_visitor::visit(unop::Closure)): Likewise.
      * src/tgbatest/ltl2tgba.test, src/ltltest/reduccmp.test: New test
      cases.
      b3cc033e
    • Alexandre Duret-Lutz's avatar
      Setup machinery to build DFA when translating some PSL operators. · d1530de1
      Alexandre Duret-Lutz authored
      This is especially important when translating the Closure
      operators, because normally we should only keep the satisfiable
      formulae (i.e. co-accessible states), which seems hard to check on
      the fly.  After this patch we need to teach
      ratexp_to_dfa::translate() how to trim (and then minimize) the DFA
      to prune those useless (non co-accessible) states.
      
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa): New class.
      (translate_dict::transdfa): New member.
      (ltl_trad_visitor::visit(unop::Closure)): Use transdfa.
      d1530de1
    • Alexandre Duret-Lutz's avatar
      Generalize syntactic implication for event. and univ. formulae. · 2f036493
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (syntactic_implication_aux): Refine
      rules to deal with pure eventualities and purely universal
      properties.
      * src/ltltest/reduccmp.test: Add tests.
      2f036493
    • Alexandre Duret-Lutz's avatar
      Translate Boolean formulae as BDD using the ltl_simplifier cache. · 07e40e70
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
      (ltl_simplifier::ltl_simplifier, ltl_simplifier::get_dict): Make
      it possible to supply and retrieve the dictionary used.
      (ltl_simplifier::as_bdd): New function, exported from the cache.
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Store the
      ltl_simplifier object.
      (translate_dict::boolean_to_bdd): Call ltl_simplifier::as_bdd.
      (translate_ratexp): New wrapper around the ratexp_trad_visitor,
      calling boolean_to_bdd whenever possible.
      (ratexp_trad_visitor): Do not deal with negated formulae, there
      are necessarily Boolean and handled by translate_ratexp().
      (ltl_visitor): Adjust to call translate_ratexp.
      (ltl_to_tgba_fm): Adjust passing of the ltl_simplifier to the
      translate_dict, and make sure everybody is using the same
      dictionary.
      * src/tgbatest/ltl2tgba.cc: Pass the dictionary to the
      ltl_simplifier.
      07e40e70
    • Alexandre Duret-Lutz's avatar
      Rewrite syntactic implication using a single function. · 369ad87e
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (inf_left_recurse_visitor,
      inf_right_recurse_visitor): Remove.
      (syntactic_implication, syntactic_implication_aux): Rewrite all
      rules for syntactic implication.
      (syntactic_implication_neg): Simplify.
      369ad87e
    • Alexandre Duret-Lutz's avatar
      Decrease the maximum bound used in random BUnOps. · 7514cc15
      Alexandre Duret-Lutz authored
      * src/ltlvisit/randomltl.cc (bunop_bounded_builder,
      bunop_bool_bounded_builder): Set the maximum value
      to 3 instead of 4, to speed up the test suite.
      7514cc15
    • Alexandre Duret-Lutz's avatar
      Avoid containment checks on equal formulae. · c54627be
      Alexandre Duret-Lutz authored
      * src/ltlvisit/contain.cc
      (language_containment_checker::contained,
      language_containment_checker::neg_contained,
      language_containment_checker::contained_neg): Detect
      cases where both formulae are equal.
      c54627be
    • Alexandre Duret-Lutz's avatar
      Fix translation of '{(c&!c)[->0..1]}!'. · 58bbaa08
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit): Fix
      the translation of the Goto operator.
      (ratexp_trad_visitor::next_to_concat): More comments.
      * src/ltltest/reduccmp.test: Add a test case.
      58bbaa08
    • Alexandre Duret-Lutz's avatar
      Fix a Clang-2.9 warning. · 1507dbc6
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (trace_ltl_bdd):
      Declare as unused.
      1507dbc6
    • Alexandre Duret-Lutz's avatar
      Check that reductions are legitimates with containment. · 7f7627bf
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
      (are_equivalent): Export this function from the cache.
      * src/ltltest/reduc.cc, src/ltltest/equals.cc: Use
      are_equivalent() to check that the reductions are legitimate.
      7f7627bf
    • Alexandre Duret-Lutz's avatar
      Fix universal and eventual rules for M and W. · cd9369c1
      Alexandre Duret-Lutz authored
      * src/ltlast/binop.cc: a M b is eventual if both a and b are
      eventual, or if b == 1.  a W b is universal if both a and b
      are universal or if b == 0.
      * src/ltltest/kind.test: New test case.
      cd9369c1
    • Alexandre Duret-Lutz's avatar
      Compare Boolean LTL formulae using BDDs. · c9a659c8
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (syntactic_implication): Here.
      c9a659c8
    • Alexandre Duret-Lutz's avatar
      Merge the syntactic implication code with ltl_simplifier. · fea49630
      Alexandre Duret-Lutz authored
      So that we can latter use some combined optimizations.
      
      * src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Integrate
      the code from syntimpl.cc
      * src/ltlvisit/syntimpl.hh, src/ltlvisit/syntimpl.cc: Delete.  All
      code has been moved above.
      * src/ltlvisit/Makefile.am: Adjust.
      * src/ltltest/syntimpl.cc: Adjust code.
      fea49630
    • Alexandre Duret-Lutz's avatar
      3db13a6f
    • Alexandre Duret-Lutz's avatar
      Rewrite xor, =>, and <=> in negative_normal_form(). · 03fd46a1
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
      (ltl_simplify::negative_normal_form): Remove the third
      parameter and always rewrite XOR, =>, and <=>.  This avoid
      problems with the cache, that could have been populated with
      a different value for this third parameter.
      * src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust
      calls to negative_normal_form().
      * src/ltltest/nenoform.test: Adjust tests.
      03fd46a1
    • Alexandre Duret-Lutz's avatar
      Mark reduce_tau03() as deprecated. · b89f86ed
      Alexandre Duret-Lutz authored
      * src/ltlvisit/contain.hh (reduce_tau03): Mark as deprecated.
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/ltl2tgba.cc,
      src/ltltest/equals.cc: Do not include ltlvisit/contain.hh, since
      it's not used.
      b89f86ed
    • Alexandre Duret-Lutz's avatar
      Remove basicreduce files. ltl_simplifier does all the work. · 5c1729d6
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/basicreduce.hh: Delete.
      * src/ltlvisit/Makefile.am: Remove them.
      5c1729d6
    • Alexandre Duret-Lutz's avatar
      Deprecate reduce() in favor of ltl_simplifier. · 67f4e8b5
      Alexandre Duret-Lutz authored
      * src/ltlvisit/reduce.hh: Mark the file as obsolete.
      (reduce): Declare this function as obsolete.
      * src/ltlvisit/reduce.cc: Define SKIP_DEPRECATED_WARNING
      so we can include reduce.hh.
      * src/sanity/includes.test: Also use SKIP_DEPRECATED_WARNING
      when compiling headers.
      * iface/dve2/dve2check.cc,
      src/ltltest/equals.cc, src/ltltest/randltl.cc,
      src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/randtgba.cc,
      wrap/python/ajax/spot.in, wrap/python/spot.i: Adjust
      to use ltl_simplifier.
      * src/tgbatest/ltl2tgba.cc: Adjust to use ltl_simplifier,
      and replace -fr1...-fr7 options by a single -fr option.
      * src/tgbatest/spotlbtt.test: Adjust -fr flags accordingly.
      * src/tgbatest/reductgba.cc: Do not include reduce.hh.
      67f4e8b5
    • Alexandre Duret-Lutz's avatar
      Move the remaining reduce() logic into ltl_simplifier. · c0085a8f
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.hh
      (ltl_simplifier::negative_normal_form): Allow logical
      unabbreviations during the NNF pass.
      * src/ltlvisit/simplify.cc
      (ltl_simplifier::negative_normal_form)
      (negative_normal_form_visitor): Adjust.
      (ltl_simplifier::simplify): Request unabbreviations.
      * src/ltlvisit/reduce.cc (reduce): Remove most
      of the code, leaving only a call ltl_simplifier
      and some wrapper code to convert options.
      * src/ltltest/reduccmp.test: Add more test cases.
      c0085a8f
    • Alexandre Duret-Lutz's avatar
      Typo in the code rewriting "a M 1 = Fa". · d4d4c0e7
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (simplify_visitor): Fix it,
      and leave the trace code.
      d4d4c0e7
    • Alexandre Duret-Lutz's avatar
      Remove the negative_normal_form call from reduce(). · c2335edb
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (ltl_simplifier::simplify):
      Convert in negative normal form if needed.
      * src/ltlvisit/reduce.cc (reduce): Do not call
      negative_normal_form().
      c2335edb
    • Alexandre Duret-Lutz's avatar
      Move language containment into ltl_simplifier. · 1087c623
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc: Integrate the tau03
      containment rules.
      * src/ltlvisit/simplify.hh: Add options to select simplifications.
      * src/ltlvisit/reduce.cc (reduce): Do not call reduce_tau03().
      * src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove.
      (reduce_tau03): Implement it using ltl_simplifier.
      1087c623
    • Alexandre Duret-Lutz's avatar
      Generalize G,&,| rewritings to deal with event. and univ. terms. · 82b42494
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (ltl_simplifier): Adjust
      code.
      * src/ltltest/reduccmp.test: Add some test cases.
      82b42494
    • Alexandre Duret-Lutz's avatar
      More rewritings or multop::And and multop::Or. · ab7a1c7a
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (ltl_simplifier): Add more rewritings
      for formulae that are both universal and eventual.
      * src/ltltest/reduccmp.test: Add six more cases.
      ab7a1c7a
    • Alexandre Duret-Lutz's avatar
      Make sure 'a U XXXFb' reduces to 'XXXFb'. Spot 0.7.1 missed that. · 09d96969
      Alexandre Duret-Lutz authored
      * src/ltltest/reduccmp.test: Add the test.
      09d96969
    • Alexandre Duret-Lutz's avatar
      47fb4491
    • Alexandre Duret-Lutz's avatar
      Fix a case caught by the random formula generator. · ca686cb0
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (ltl_simplifier): Since we are processing
      the formula bottom-up, don't assume all trivial simplification have
      been done.
      * src/ltltest/reduccmp.test: More tests.
      ca686cb0
    • Alexandre Duret-Lutz's avatar
      Reimplement basic_reduce()'s rules in ltl_simplifier. · ca2fe4f3
      Alexandre Duret-Lutz authored
      So far I have only checked these rewritings with reduccmp.test.
      There are probably a few kinks to iron out.
      
      * src/ltlvisit/simplify.cc: Reimplement most of the basic
      rewriting rules, leaving some FIXME comments for dubious ones.
      * src/ltlast/multop.cc, src/ltlast/multop.hh: Ignore NULL
      pointers in the vector.
      * src/ltlvisit/reduce.cc (reduce): Do not call basic_reduce().
      * src/ltltest/reduccmp.test: Adjust tests.
      ca2fe4f3
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      event./univ. and syntactic implications rewriting in ltl_simplifier. · dd1cd89a
      Alexandre Duret-Lutz authored
      * src/ltlvisit/reduce.cc (reduce_visitor): Move ...
      * src/ltlvisit/simplify.cc (simplify_visitor): ... here, and
      adjust to use the new ltl_simplifier_options.
      * src/ltlvisit/reduce.cc (reduce): Use ltl_simplifier
      to perform the work of reduce_visitor.  Eventually we want to
      get rid of reduce.cc.
      * src/ltlvisit/reduce.hh (reduce): Remove the
      syntactic_implication_cache used as third argument.
      dd1cd89a
    • Alexandre Duret-Lutz's avatar
      Adjust kind.test Adjust after the change of 2011-05-23. · 503bdb5b
      Alexandre Duret-Lutz authored
      * src/ltltest/kind.test: More pure eventualities and purely
      universal properties are detected.
      503bdb5b
    • Alexandre Duret-Lutz's avatar
      Take trivial identities into account to simplify basicreduce. · aa5c2f60
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc: Do not test
      for things like X(true), F(false), or `a U 1`.
      These are all trivial identities.
      aa5c2f60
    • Alexandre Duret-Lutz's avatar
      bd720488
    • Alexandre Duret-Lutz's avatar
      Generalize computation of is.eventual and is.universal. · 8ecf57e8
      Alexandre Duret-Lutz authored
      * src/ltlast/binop.cc (binop::binop): Generalize detection
      of pure eventualities and purely universal formulae.  E.g.
      `f U g' is a pure eventuality if g is a pure eventuality
      (regardless of f) or if g is 1.
      * src/ltlast/unop.cc (unop::unop): Compute is.eventual
      and is.universal for Not.
      * src/ltltest/kind.test: Adjust.
      8ecf57e8
    • Alexandre Duret-Lutz's avatar
      Introduce ltl_simplifier. · 9f7ef5d0
      Alexandre Duret-Lutz authored
      It is limited to negative_normal_form_visitor for now.
      
      * src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh: Rewrite
      using ltl_simplifier.
      9f7ef5d0
    • Alexandre Duret-Lutz's avatar
      Speedup randpsl.test. · 0caa631c
      Alexandre Duret-Lutz authored
      * src/tgbatest/randpsl.test: Run without valgrind, it is too
      slow otherwise.
      0caa631c
    • Alexandre Duret-Lutz's avatar
      Track finite formulae. · fb386209
      Alexandre Duret-Lutz authored
      I.e., SERE without star, or LTL formula using only X and Boolean
      operators.
      
      * src/ltlast/formula.hh, src/ltlast/formula.cc: Add a bit for
      tracking finite formulas.
      * src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
      src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc:
      Adjust.
      * src/ltlast/unop.cc, src/ltlast/binop.cc: Adjust and use that
      bit to refine the computation of some LTL classes.
      * src/ltltest/kind.test: New tests.
      fb386209
    • Alexandre Duret-Lutz's avatar
      Track syntactic classes. · df760a45
      Alexandre Duret-Lutz authored
      These are safety, guarantee, obligation, persistence, and recurrence.
      
      * src/ltlast/formula.hh, src/ltlast/formula.cc: Declare a bit for
      each of these classes.
      * src/ltlast/atomic_prop.cc, src/ltlast/constant.cc,
      src/ltlast/automatop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc,
      src/ltlast/unop.cc: Update these bits.
      * src/ltltest/kind.test: Update tests and add more.
      df760a45