1. 28 Apr, 2012 37 commits
    • Alexandre Duret-Lutz's avatar
      Introduce AndRat and OrRat operator. · 691119c1
      Alexandre Duret-Lutz authored
      It was a mistake to try to overload And/Or LTL operator for these when
      trivial simplification are performed.  The reason is so simple it is
      embarassing: And(f,1)=f is a trivial identity that should not be
      applied with AndRat.  E.g. AndRat(a;b, 1) is equal to 0, not a;b.
      
      * src/ltlast/multop.hh, src/ltlast/multop.cc: Add the AndRat and OrRat
      operators.
      * src/ltlparse/ltlparse.yy: Build them.
      * src/ltlvisit/mark.cc, src/ltlvisit/simplify.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:
      Adjust all switches.
      691119c1
    • Alexandre Duret-Lutz's avatar
      Fix translation of AndNLM and Fusion operators. · f7c64060
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc: Here.
      The check is done by next patch.
      f7c64060
    • Alexandre Duret-Lutz's avatar
      Get rid of bunop::Equal and bunop::Goto. · abaf1027
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.hh, src/ltlast/bunop.cc, src/ltlvisit/randomltl.cc,
      src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
      src/tgbaalgos/ltl2tgba_fm.cc: Remove all traces of these two
      operators since they are not handled like sugar.
      * doc/tl/tl.tex: Adjust documentation to reflect the fact that these
      two operators are sugar.
      abaf1027
    • Alexandre Duret-Lutz's avatar
      Remove a dynamic_cast. · 77543842
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_ratexp): Replace
      a dynamic cast by a call to kind().
      77543842
    • Alexandre Duret-Lutz's avatar
      Speedup mark_concat_ops() and simplify_mark() with a cache. · 0f11e5fe
      Alexandre Duret-Lutz authored
      * src/ltlvisit/mark.hh, src/ltlvisit/mark.cc (mark_concat_ops,
      simplify_mark): Rewrite these two functions as methods of
      (mark_tools): this new class.
      * src/ltlast/binop.cc, src/ltlast/unop.cc: Adjust computation
      of not_marked to ignore marked operators that are not at
      the top-level.  I.e., something like X(!{a}) is not marked.
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::mt): New
      instance of mark_tools.
      (formula_canonizer::translate) Adjust calls to
      mark_concat_ops() and simplify_mark().
      0f11e5fe
    • Alexandre Duret-Lutz's avatar
      Ignore sub-"SERE" that have been proved useless already. · 098e121a
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not
      translate a subformula if we have already proved it useless in
      a previous rational expression.
      * src/tgbatest/ltl2tgba.test: Add an example, although that
      test does not ensure the subformula is ignored early in the
      translation.  I.e., it would still work without the patch.
      098e121a
    • Alexandre Duret-Lutz's avatar
      Speedup construction of transitions in ltl_to_tgba_fm. · 4ba60dad
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate,
      ltl_to_tgba_fm): Do not convert labels as Boolean formulas before
      creating transitions.  Use the bdd directly, and register the used
      transitions later.
      4ba60dad
    • Alexandre Duret-Lutz's avatar
      Reuse Boolean->BDD translations performed during simplification. · b67852a5
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd):
      Use boolean_to_bdd()
      b67852a5
    • Alexandre Duret-Lutz's avatar
      Cache the LTL->BDD translation for every subformulae. · f590ca4e
      Alexandre Duret-Lutz authored
      We used to cache it only for formulas used as states.
      
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd): New method.
      (ltl_trad_visitor::recurse): Use ltl_to_bdd().
      (formula_canonizer): Likewise.
      (ltl_to_tgba_fm): Adjust.
      f590ca4e
    • 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
      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
      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
      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
      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
      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
      Fix infinite recursion when translating E* and E accepts [*0]. · a29c87b2
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit):
      Use a different translating rule for E* if E accepts [*0].
      * src/tgbatest/ltl2tgba.test: Add test case.
      a29c87b2
    • Alexandre Duret-Lutz's avatar
      Relax usage of ->, <->, and xor in SERE. · eab91aab
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlparse.yy (rationalexp): Allow ->, <->, and xor,
      in rational expressions as long as they apply only to Boolean
      formulae.
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Adjust
      assert in handling of unop::Not.
      eab91aab
    • Alexandre Duret-Lutz's avatar
      Remove the has_mark() function in favor of the is_marked() method. · 6380968f
      Alexandre Duret-Lutz authored
      * src/ltlast/unop.cc (NegClosure): Reset is.not_marked.
      * src/ltlvisit/mark.hh,
      src/ltlvisit/mark.cc (has_mark_visitor, has_mark): Remove.
      * src/tgbaalgos/ltl2tgba_fm.cc: Use f->is_marked() instead
      of has_mark(f).
      6380968f
    • Alexandre Duret-Lutz's avatar
      Replace the constant_term visitor by a flag in the formulae. · 48cde88b
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh (formula::accepts_eword): New method.
      (formula::is.accepting_eword): New flag.
      * src/ltlast/formula.cc (print_formula_props): Display the new
      property.
      * src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
      src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc,
      src/ltlast/multop.cc, src/ltlast/unop.cc: Update
      is.accepting_eword as appropriate.
      * src/ltltest/consterm.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust to
      use accepts_eword().
      * src/ltlvisit/consterm.cc, src/ltlvisit/consterm.hh: Delete.
      * src/ltlvisit/Makefile.am: Remove these files.
      48cde88b
    • Alexandre Duret-Lutz's avatar
      Fix rewriting of Negated constants and atomic propositions · 4fd4f83e
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Take a
      "negated" parameter and use it.
      4fd4f83e
    • Alexandre Duret-Lutz's avatar
      Introduce [->min..max] operator. · da74b4f1
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.hh: Declare bunop::Goto
      * src/ltlast/bunop.cc: Handle it.
      * src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll: Add rules for [->min..max].
      * src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Goto in
      the translation.
      * src/ltltest/equals.test: Test trivial identities.
      * src/tgbatest/ltl2tgba.test: Test two more formulae using [->].
      da74b4f1
    • Alexandre Duret-Lutz's avatar
      Introduce [=min..max] operator. · 8d4a413a
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.hh: Declare bunop::Equal
      * src/ltlast/bunop.cc: Handle it.
      * src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll: Add rules for [=min..max].
      * src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Equal in
      the translation.
      * src/ltltest/equals.test: Test trivial identities
      for [=min..max].
      * src/tgbatest/ltl2tgba.test: Add new formulae to test.
      8d4a413a
    • Alexandre Duret-Lutz's avatar
      Add support the bounded star operator [*i..j]. · 126b724a
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.hh, src/ltlast/bunop.cc: New files for
      bounded unary operators.
      * src/ltlast/Makefile.am, src/ltlast/allnodes.hh: Add them.
      * src/ltlast/predecl.hh (bunop): Declare.
      * src/ltlast/unop.hh, src/ltlast/unop.cc (Star): Remove
      declaration of Star and associated code.
      * src/ltlast/visitor.hh: Add visit(bunop* node) methods.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Add parse
      rules for LTL.  This required passing the parse_error list
      to the lexer, so it can report scanning errors when it reads
      a number that does not fit in an unsigned int.
      * src/ltlparse/parsedecl.hh (YY_DECL): Take error_list
      as third argument.
      * src/ltltest/consterm.test, src/ltltest/tostring.test,
      src/ltltest/equals.test, src/tgbatest/ltl2tgba.test: More tests.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/consterm.cc,
      src/ltlvisit/dotty.cc, src/ltlvisit/mark.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/postfix.cc,
      src/ltlvisit/postfix.hh, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
      src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
      src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc: Adjust syntax to use
      "bunop::Star" instead of "unop::Star".
      * src/tgbaalgos/ltl2tgba_fm.cc: Likewise, but also adjust
      the code to handle the bounds of the operator.
      126b724a
    • Alexandre Duret-Lutz's avatar
      Fix deterministic translation of []->. · aef6c1a0
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit): Fix
      the "deterministic case" of []->, and merge it with the
      non-deterministic case.
      aef6c1a0
    • Alexandre Duret-Lutz's avatar
      Allow boolean atoms to be negated in rational expressions. · 4aa82ec7
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlparse.yy (rationalexp): Recognize "OP_NOT
      booleanatom".
      * src/ltlvisit/consterm.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust.
      * src/tgbatest/ltl2tgba.test: Add one test.
      4aa82ec7
    • Alexandre Duret-Lutz's avatar
      Add support for PSL's non-length-matching And. · bbb645e1
      Alexandre Duret-Lutz authored
      * src/ltlast/multop.cc, src/ltlast/multop.hh: Declare AndNML
      operator.
      * src/ltlparse/ltlscan.ll: Distinguish "&" and "&&".
      * src/ltlparse/ltlparse.yy: Handle them both as "And" for LTL
      formula, use AndNML or And for rational expressions.
      * src/ltlvisit/tostring.cc: Adjust to distinguish "&" and "&&" in
      rational expressions. Also use {braces} to group rational
      expressions.
      * src/tgbaalgos/ltl2tgba_fm.cc
      (ratexp_trad_visitor::ratexp_trad_visitor): Remove the possibility
      to select the empty_word should act like true, and fix the rules
      for Closure and NegClosure to rely on constant_term instead.
      (ratexp_trad_visitor::visit) Adjust the And translation to also
      support AndNML.
      (ratexp_trad_visitor::recurse_and_concat): Introduce this new
      method to simplify some calls to recurse(f, to_concat_).
      * src/tgbatest/ltl2tgba.test: Add more test cases.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
      src/ltlvisit/contain.cc, src/ltlvisit/mark.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/syntimpl.cc,
      src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Add
      missing cases in switches.
      bbb645e1
    • Alexandre Duret-Lutz's avatar
      Add support for {SERE} and !{SERE} closure operators. · 2f8c4ac8
      Alexandre Duret-Lutz authored
      * src/ltlast/unop.hh, src/ltlast/unop.cc: Introduce Closure and
      NegClosure operators.
      * src/ltlparse/ltlparse.yy: Recognize {foo} as a Closure.
      * src/ltlvisit/mark.cc: Consider NegClosure as a marked operator.
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Add option to
      select whether the empty_word should act like true (for {SERE}
      and {!SERE}) or false (for {SERE}<>->Exp or {SERE}[]->Exp).
      (ltl_trad_visitor): Translate Closure and NegClosure.
      * src/tgbatest/ltl2tgba.test: Add more tests.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
      src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
      src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc: Straightforward update to support or
      assert on these new operators.
      2f8c4ac8
    • Alexandre Duret-Lutz's avatar
      Build deterministic automata for []-> operators. · f618e6bc
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit): Honor
      exprop_ while handling the binop::UConcat case.
      f618e6bc
    • Alexandre Duret-Lutz's avatar
      Build deterministic automata for <>-> operators. · dbdd3701
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Take
      an exprop argument, and use it while translation <>-> operators.
      * src/tgbatest/ltl2tgba.test (check_psl): Use -x too.
      dbdd3701
    • Alexandre Duret-Lutz's avatar
      Parse the fusion operator (":") and translate it in ltl2tgba_fm(). · c2b3dac7
      Alexandre Duret-Lutz authored
      * src/ltlast/multop.hh (multop::type::Fusion): New operator.
      * src/ltlast/multop.cc: Handle it.
      * src/ltlparse/ltlparse.yy: Declare OP_FUSION and add grammar
      rules.
      * src/ltlparse/ltlscan.ll: Recognize ":" as OP_FUSION.
      * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit):
      Add translation rule for multop::Fusion.
      * src/tgbatest/ltl2tgba.test: Add more tests.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
      src/ltlvisit/contain.cc, src/ltlvisit/mark.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
      src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc: Handle multop::Fusion in switches.
      c2b3dac7
    • Alexandre Duret-Lutz's avatar
      Update the FM translation to handle <>->, []->, *, ;, #e. · bd9136a9
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc: Implement translation for
      recently introduced operators.
      * src/tgbatest/ltl2tgba.test: Add some PSL tests.
      bd9136a9
    • Alexandre Duret-Lutz's avatar
      Introduce EConcatMarked "<>+>" as operator. · 171ca678
      Alexandre Duret-Lutz authored
      * src/ltlast/binop.cc, src/ltlast/binop.hh: Introduce
      EConcatMarked ("<>+>").
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
      src/ltlvisit/reduce.cc, src/ltlvisit/simpfg.cc,
      src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc, src/tgba/formula2bdd.cc,
      src/tgba/formula2bdd.cc: Deal with it if possible or ignore
      it.
      171ca678
    • Alexandre Duret-Lutz's avatar
      Add []-> and <>->. · c6dd811b
      Alexandre Duret-Lutz authored
      * src/ltlast/binop.hh, src/ltlast/binop.cc (EConcat, UConcat):
      Add these new operators.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse
      these new operators.
      * src/ltlvisit/simpfg.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc, src/ltlvisit/basicreduce.cc,
      src/ltlvisit/consterm.cc, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.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 these new operators into the
      switches.
      c6dd811b
    • Alexandre Duret-Lutz's avatar
      Introduce rational operators and trivial simplification rules. · 546559b8
      Alexandre Duret-Lutz authored
      Trivial simplifications rules (such as "FFa=Fa" or "x&1=x")
      are performed any time a formule is instanciated.
      
      * src/ltlast/constant.hh, src/ltlast/constant.cc
      (true_instance, true_instance_): Declare the true_instance_ as a
      static member, and move true_instance() into the .hh so it gets
      inlined.  Have true_instance_ as a class variable will ensure that
      it is the first formula instantiated.  Binop simplifications rely
      on this to order arguments.
      (false_instance, false_instance_): Likewise.
      (empty_word_instance, empty_word_instance_): New method and static
      member.
      * src/ltlast/formula.hh (formula::formula): If max_count_ ever
      loops, skip the first three values so that constants always have
      smaller hash codes.
      * src/ltlast/binop.hh, src/ltlast/binop.cc (instance): Add
      simplifications and document them.
      * src/ltlast/multop.hh (multop::Concat): New operator.
      * src/ltlast/multop.cc (op_name): Handle Concat.
      (instance): Inline Concat arguments without reordering.  Handle
      absorbent and neutral elements for all operators.
      * src/ltlast/unop.hh (unop::Star): New operator.
      * src/ltlast/unop.cc (op_name): Handle Star.
      (instance): Handle Star, and add trivial simplifications for
      other unary operators.
      * src/ltlparse/ltlparse.yy (OP_CONCAT, OP_STAR, CONST_EMPTYWORD):
      Declare these new operators and add rules for them.
      * src/ltlparse/ltlscan.ll (OP_CONCAT, OP_STAR, CONST_EMPTYWORD):
      Output these new operators.
      * src/ltltest/equals.test: New tests.
      * src/ltltest/parse.test: Remove redundant test.
      * src/ltltest/tunabbrev.test, src/tgbatest/emptchk.test: Adjust tests.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
      src/ltlvisit/tunabbrev.cc: Complete visitors to handle new
      operators.
      * src/ltltest/nenoform.test: More tests.
      * src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::visit):
      Clone formulae before instance() function actually have a chance
      to destroy them.
      * src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc: Adjust switches to assert on new
      operators.
      546559b8
  2. 27 Apr, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
      Remove the old broken game-theory-based simulation reductions. · 7e587584
      Alexandre Duret-Lutz authored
      This implementation of direct simulation was only working on
      degeneralized automata, and produce automata that are inferiors to
      those output by the new direct simulation implementation (in
      tgba/simulation.hh) which can also work on TGBA.  The delayed
      simulation has never been reliable.  It's time for some spring
      cleaning.
      
      * src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Delete.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh:
      Remove all code, and keep only a deprecated replacement
      from reduc_tgba_sim().
      * src/tgbaalgos/reductgba_sim_del.cc: Delete.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
      src/tgbatest/reductgba.test: Delete.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc: Undocument options -R1s, -R1t,
      -R2s, -R2t, and implement them using the new direct simulation.
      Remove options -Rd and -RD.
      * src/tgbatest/spotlbtt.test: Remove entry using these old options.
      * wrap/python/spot.i: Do not process tgbaalgos/reductgba_sim.cc.
      7e587584
    • Alexandre Duret-Lutz's avatar
      slights documentation changes around direct simulation · 7ba4ab79
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/simulation.hh: Mention the fact that this is
      a "direct" simulation.
      * wrap/python/ajax/ltl2tgba.html: Likewise, and change the key
      to "ds".
      * wrap/python/ajax/protocol.txt, wrap/python/ajax/spot.in: Adjust.
      7ba4ab79
  3. 18 Apr, 2012 1 commit
    • Thomas Badie's avatar
      Create the direct simulation. · 876f8c90
      Thomas Badie authored
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: New files.
      * src/tgbaalgos/Makefile.am: Add the new files to the compilation.
      * src/tgbatest/spotlbtt.test: Add the simulation.
      * src/tgbatest/ltl2tgba.cc: Add direct simulation (-RSD).
      876f8c90