1. 28 Apr, 2012 40 commits
    • Alexandre Duret-Lutz's avatar
    • 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
      Equal and Goto should only apply to Boolean expressions. · 8cafa200
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.cc (bunop::bunop): Ensure it using an assert.
      8cafa200
    • Alexandre Duret-Lutz's avatar
      Prepare the introduction of random_sere() and random_psl(). · 7c7704f9
      Alexandre Duret-Lutz authored
      * src/ltlvisit/randomltl.hh (random_ltl): Split this class into...
      (random_formula, random_ltl): ... these.
      * src/ltlvisit/randomltl.cc: New
      7c7704f9
    • Alexandre Duret-Lutz's avatar
      Speedup syntactic_implication() by using a cache. · 4ef7805e
      Alexandre Duret-Lutz authored
      * src/ltlvisit/syntimpl.hh (syntactic_implication,
      syntactic_implication_neg): Move as member of ...
      (syntactic_implication_cache): ... this new class, that holds
      a cache of results to speedup these functions.
      * src/ltlvisit/syntimpl.cc: Adjust to use (lookup, populate,
      and cleanup) the cache.
      * src/ltltest/syntimpl.cc: Likewise.
      * src/ltlvisit/reduce.hh (reduce): Take an optional
      syntactic_implication_cache parameter.
      * src/ltlvisit/reduce.cc: Adjust to use a
      syntactic_implication_cache.
      * src/ltltest/equals.cc: Call dump_instances() to help debugging.
      4ef7805e
    • Alexandre Duret-Lutz's avatar
      Speedup some rewriting by detecting cases where they do nothing. · 20c088a4
      Alexandre Duret-Lutz authored
      * src/ltlvisit/nenoform.cc, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/simpfg.cc, src/ltlvisit/tunabbrev.cc: Do not recurse
      if the formula properties indicate that it is already in the right
      form.
      20c088a4
    • 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
      Get rid of all dynamic_cast<>s while working on LTL formulae. · 957ba664
      Alexandre Duret-Lutz authored
      They are too slow.
      
      * src/ltlast/formula.hh (opkind, kind, kind_): Use an enum
      to indicate the actual kind of the formula.  This way we can
      check the kind of a formula without relying on dynamic_cast.
      * 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/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc: Adjust constructors.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/mark.cc,
      src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc: Replace all dynamic_cast by a
      call to kind() followed by a static_cast.
      957ba664
    • 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
      Maintain basic LTL properties using a bitfield inside formula objects. · 546260e7
      Alexandre Duret-Lutz authored
      This bitfield is easily updated as the formulae are constructed.
      Doing so avoids many AST recursions to compute these properties
      individually.  This patch removes the eventual_universal_visitor,
      as well as the kind_of() function.
      
      * src/ltlast/formula.hh (is_boolean, is_sugar_free_boolean,
      is_in_nenoform, is_X_free, is_sugar_free_ltl,
      is_ltl_formula, is_eltl_formula, is_psl_formula, is_eventual,
      is_universal, is_marked): New methods to query formula
      properties in constant time.
      (get_props, ltl_prop): A method and structure for
      implementation as a field bit in an unsigned, for fast
      computation.
      (print_formula_props): New function.
      * src/ltlast/formula.cc (print_formula_props): Implement it.
      * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
      src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/multop.cc,
      src/ltlast/unop.cc, src/ltlast/automatop.cc: Compute the
      properties as instances are constructed.
      * src/ltlparse/ltlparse.yy: Update to use is_boolean() instead
      of kind_of().
      * src/ltltest/kind.cc: Update to use print_formula_props().
      * src/ltltest/kind.test: Adjust to test eventual and universal
      properties.
      * src/ltlvisit/kind.cc, src/ltlvisit/kind.hh: Delete these files.
      * src/ltlvisit/Makefile.am: Remove kind.hh and kind.cc.
      * src/ltlvisit/reduce.cc (recurse_eu, eventual_universal_visitor):
      Remove, no longer needed.
      (reduce_visitor, is_eventual, is_universal): Adjust to
      use formula::is_eventual(), and formula::is_universal().
      * src/ltlvisit/reduce.hh (is_eventual, is_universal): Declare as
      deprecated.
      546260e7
    • Alexandre Duret-Lutz's avatar
      Simplify fUf, fRf, fWf, and fRF as f. · 1671aa5d
      Alexandre Duret-Lutz authored
      * src/ltlast/binop.cc (binop::instance): Simplify fUf, fRf, fWf,
      and fRF.
      * src/ltlast/binop.hh: Document it.
      * src/ltltest/equals.test: Add new tests for 'Exp U Exp'
      and 'Exp R Exp', and all missing tests for W and M.
      1671aa5d
    • Alexandre Duret-Lutz's avatar
      Do not simplify F([*0]) and G([*0]). Make sure it does not happen. · 5bb171c8
      Alexandre Duret-Lutz authored
      * src/ltlast/unop.hh, src/ltlast/unop.cc: Replace the
      simplification by an assert.
      5bb171c8
    • Alexandre Duret-Lutz's avatar
      Fix trivial identity (0 => Exp) == 1, and add rewritings for =>. · 473cf771
      Alexandre Duret-Lutz authored
      The new rewriting are (Exp => Exp) = 1, (Exp <=> Exp) == 1,
      and (Exp ^ Exp) == 0.
      
      * src/ltlast/binop.hh: Fix documentation.
      * src/ltlast/binop.cc: Fix implementation.
      * src/ltltest/equals.test: More tests.
      * src/tgbatest/emptchk.test: Remove a useless test.
      473cf771
    • Alexandre Duret-Lutz's avatar
      Read p=0Wq=1 and p=0Mq=1 correctly. · f2732dd8
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlscan.ll: Handle p=0Wq=1 and p=0Mq=1 in
      the same way as we did for
      * src/ltltest/parse.test: More tests.
      f2732dd8
    • Alexandre Duret-Lutz's avatar
      Accept more syntaxes as range specifications for [*], [=], and [->]. · 754ff36b
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlscan.ll (OP_SQBKT_SEP): Accept ":" and "to"
      in addition to ".." and ",".
      (OP_UNBOUNDED): Recognize "$" for the rule below.
      * src/ltlparse/ltlparse.yy: Accept [OP1:$] as a synonym
      for [OP1:], for people used to SVA's syntax.
      * src/ltltest/equals.test: Test these syntaxes.
      754ff36b
    • 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
      Speed up computation of constant term on [->] and [=] operators. · c6a751b9
      Alexandre Duret-Lutz authored
      * src/ltlvisit/consterm.cc: Stop the recursion on [->] and [=].
      c6a751b9
    • Alexandre Duret-Lutz's avatar
    • 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
      Rewrite Exp[=0..] as [*]. · 2c31e541
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.cc: Implement this rewriting.
      * src/ltlast/bunop.hh: Document it.
      * src/ltltest/equals.test: Test it.
      2c31e541
    • 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
      Simplify ![*0] as [+]. · d7781bc4
      Alexandre Duret-Lutz authored
      * src/ltlast/unop.cc: Simplify ![*0] as 1[+].
      * src/ltlast/unop.hh: Document it.
      d7781bc4
    • Alexandre Duret-Lutz's avatar
      Add functions to compute the kind of a formula (LTL, PSL, Boolean...) · 437128b5
      Alexandre Duret-Lutz authored
      * src/ltlvisit/kind.hh, src/ltlvisit/kind.cc: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/ltltest/kind.test, src/ltltest/kind.cc: New files.
      * src/ltltest/Makefile.am: Add them.
      437128b5
    • Alexandre Duret-Lutz's avatar
      Add support for [+]. · 567b4607
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.cc (bunop::format): Output [*1..] as [+].
      * src/ltlvisit/tostring.cc: Output "a*" as "a[*]" for consistency.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Recognize [+].
      * src/ltltest/tostring.test, src/ltltest/equals.test,
      src/tgbatest/ltl2tgba.test: More tests.
      567b4607
    • 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
      Print '{!a}*' rather than '!a*'. · 47b2bea8
      Alexandre Duret-Lutz authored
      * src/ltlvisit/tostring.cc: Use braces for unary operators in
      Star.
      * src/ltltest/tostring.test: Add some PSL formulae, it cannot
      hurt.
      47b2bea8
    • 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
      Recognize and use "*" (or "[*]") as an abbreviation for 1*. · 93c042d0
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlparse.yy: Recognize "*" as "1*".
      * src/ltlvisit/tostring.cc: Abbreviate "1*" as "*".
      * src/tgbatest/ltl2tgba.test: Use the new syntax.
      93c042d0
    • Alexandre Duret-Lutz's avatar
      Support non-overlapping concatenations operators []=> and <>=>. · 4bde130d
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlscan.ll: Recognize "[]=>" (a.k.a "|=>") and "<>=>".
      * src/ltlparse/ltlparse.yy: Support them by rewriting them using
      "[]->" and "<>->".
      * src/tgbatest/ltl2tgba.test: More tests.
      4bde130d
    • 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
      Accept "{E}|->ltl" and "{E}(ltl)" as synonym for "{E}[]->ltl". · 1ecc6984
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlparse.yy (parenthesedsubformula): Extract these
      rules from...
      (subformula): ... here, and use it to recognize "{SERE}(formula)".
      * src/ltlparse/ltlscan.ll: Recognize "|->" as "[]->".
      * src/ltltest/equals.test: Test these two new syntaxes.
      1ecc6984
    • Alexandre Duret-Lutz's avatar
      Use [*0] instead of #e, and support [*] in addition to *. · 8b8633de
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlscan.ll: Recognize [*] as *, and use
      [*0] instead of #e for the empty word.
      * src/ltlast/binop.cc, src/ltlast/constant.cc,
      src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc,
      src/ltlast/unop.hh, src/ltltest/consterm.test,
      src/ltltest/equals.test: Adjust all occurrences of #e to [*0].
      * src/tgbatest/ltl2tgba.test: Also use [*].
      8b8633de
    • Alexandre Duret-Lutz's avatar
      Support braces in addition to parentheses in rational expressions. · 4e7233d9
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlparse.yy (rationalexp): Allow bracedrationalexp.
      * src/ltltest/consterm.test, src/tgbatest/ltl2tgba.test: Add more
      tests.
      4e7233d9
    • 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
      Adjust Python tests to the new simplification rules. · 916c1542
      Alexandre Duret-Lutz authored
      * wrap/python/tests/ltlsimple.py: Adjust.
      916c1542
    • 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
      Do not assume that concatenation cannot accept the empty word. · ad519b85
      Alexandre Duret-Lutz authored
      For instance "(a+#e);(b+#e);(c*)" does.
      
      * src/ltlvisit/consterm.cc: Fix handling of Concat operator.
      * src/ltltest/consterm.test: Add more tests.
      ad519b85