1. 30 Sep, 2012 1 commit
  2. 24 Sep, 2012 3 commits
  3. 16 Sep, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Add a visitor to relabel the atomic proposition in formulas. · d9dc1f48
      Alexandre Duret-Lutz authored
      * src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/ltlvisit/clone.cc (recurse): Don't call clone(), nobody
      needs that.  Instead, really recurse.
      * src/bin/ltlfilt.cc: Add a --relabel option.
      * src/bin/genltl.cc: Relabel formulas if --lbt is used.
      * src/sanity/style.test: Tweak detection of i++.
      d9dc1f48
  4. 14 Sep, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Add an LTL printer in LBT's syntax. · 1a84c17e
      Alexandre Duret-Lutz authored
      * src/ltlvisit/lbt.cc, src/ltlvisit/lbt.hh: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/bin/common_output.cc, src/bin/common_output.hh: Add
      support for LBT output, and reporting formulae that cannot
      be output in this syntax.
      * src/bin/ltlfilt.cc: Pass filename and linenum to
      output_formula() for better error reporting.
      1a84c17e
  5. 07 Sep, 2012 3 commits
  6. 04 Sep, 2012 1 commit
  7. 21 Aug, 2012 2 commits
  8. 19 Jun, 2012 2 commits
  9. 21 May, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Clear the contaiment cache after -r7. · 72f36c50
      Alexandre Duret-Lutz authored
      Doing so will release all BDD variables used by automata created for
      syntactic implication.  This way the main translation will create
      acceptance variables again in a more natural order, which will help
      the degeneralization (until we get a better degeneralization).
      
      * src/ltlvisit/contain.cc, src/ltlvisit/contain.hh
      (language_containment_checker::clear): New method to clear the
      containment cache.
      * src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
      (clear_as_bdd_cache): Also call language_containment_checker::clear.
      72f36c50
  10. 20 May, 2012 3 commits
  11. 12 May, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix translation of !{r}. · e2f70e72
      Alexandre Duret-Lutz authored
      We need a marked version of !{r} to perform breakpoint unroling.
      
      * src/ltlast/unop.cc, src/ltlast/unop.hh: Declare a NegClosureMarked
      operator.
      * src/ltlvisit/mark.hh, src/ltlvisit/mark.cc,
      src/tgbaalgos/ltl2tgba_fm.cc: Adjust to deal with NegClosureMarked
      and NegClosure as apropriate.
      * src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
      src/ltlvisit/tunabbrev.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgba/formula2bdd.cc: Deal with NegClosureMarked in the same way as
      we deal with NegClosure.
      * src/tgbatest/ltl2tgba.test: More tests.
      * src/ltltest/kind.test: Adjust.
      * doc/tl/tl.tex: Mention the marked negated closure.
      e2f70e72
  12. 10 May, 2012 1 commit
  13. 07 May, 2012 1 commit
  14. 05 May, 2012 1 commit
  15. 03 May, 2012 1 commit
  16. 02 May, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Use 'const formula*' instead of 'formula*' everywhere. · bf62d439
      Alexandre Duret-Lutz authored
      The distinction makes no sense since Spot 0.5, where we switched from
      mutable furmulae to immutable formulae.  The difference between
      const_visitor and visitor made no sense either.  They have been merged
      into one: visitor.
      
      * iface/dve2/dve2check.cc, iface/gspn/ltlgspn.cc,
      src/eltlparse/eltlparse.yy, src/eltlparse/public.hh,
      src/evtgbatest/ltl2evtgba.cc, src/kripkeparse/kripkeparse.yy,
      src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
      src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
      src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
      src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
      src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/visitor.hh, src/ltlenv/declenv.cc, src/ltlenv/declenv.hh,
      src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/ltlfile.cc,
      src/ltlparse/ltlfile.hh, src/ltlparse/ltlparse.yy,
      src/ltlparse/public.hh, src/ltltest/consterm.cc,
      src/ltltest/equals.cc, src/ltltest/genltl.cc, src/ltltest/kind.cc,
      src/ltltest/length.cc, src/ltltest/randltl.cc, src/ltltest/readltl.cc,
      src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
      src/ltltest/tostring.cc, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/contain.hh, src/ltlvisit/dotty.cc,
      src/ltlvisit/length.cc, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/lunabbrev.hh, src/ltlvisit/mark.cc, src/ltlvisit/mark.hh,
      src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
      src/ltlvisit/reduce.cc, src/ltlvisit/reduce.hh,
      src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh,
      src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
      src/ltlvisit/snf.cc, src/ltlvisit/snf.hh, src/ltlvisit/tostring.cc,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh,
      src/neverparse/neverclaimparse.yy, src/sabatest/sabacomplementtgba.cc,
      src/tgba/bdddict.cc, src/tgba/formula2bdd.cc, src/tgba/taatgba.cc,
      src/tgba/taatgba.hh, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
      src/tgbatest/randtgba.cc: Massive adjustment!
      * src/tgbatest/reductgba.cc: Delete.
      bf62d439
  17. 30 Apr, 2012 5 commits
  18. 28 Apr, 2012 10 commits
    • Alexandre Duret-Lutz's avatar
      Implement basic rewriting rules for {r} and !{r}. · aec556f7
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc: Here.
      * src/ltltest/reduccmp.test: Test them.
      * doc/tl/tl.tex: Document them.
      aec556f7
    • Alexandre Duret-Lutz's avatar
      Implement dual rewritings rules for <>->. · d6587cf5
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc (reduce_sere_ltl): New function,
      to factor the code of the []-> and <>-> rewrittings.
      * src/ltltest/reduccmp.test: Add more tests.
      * doc/tl/tl.tex: Document these rewritings.
      d6587cf5
    • Alexandre Duret-Lutz's avatar
      Implement 11 rewritings for []->. · 6f46345c
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc: Here.
      * doc/tl/tl.tex: Document then.
      * src/ltlast/bunop.hh (as_KleenStar): New helper function.
      * src/ltltest/reduccmp.test: Add more tests.
      * src/ltltest/reduc.cc: Also display the resulting formula
      without reduce_size_stricly.
      6f46345c
    • Alexandre Duret-Lutz's avatar
      Implement star-normal-form rewriting. · 6eb830c8
      Alexandre Duret-Lutz authored
      * src/ltlvisit/snf.cc, src/ltlvisit/snf.hh: New files.
      * src/ltlvisit/Makefile.am: Distribute them.
      * src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Call snf(f) for
      all f[*].
      * src/ltltest/reduccmp.test: Test it.
      * doc/tl/tl.tex, doc/tl/tl.bib: Document it.
      6eb830c8
    • 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
      Add more simplification rules for AndNLM. · 35b41331
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc: Here.
      * src/ltltest/reduccmp.test: More tests.
      * doc/tl/tl.tex: Document them.
      35b41331
    • 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
      to_string: abbreviate [->i..j] and [=i..j] expressed using [*i..j] · 39417037
      Alexandre Duret-Lutz authored
      * src/ltlast/bunop.hh (is_bunop, is_Star): New functions.
      * src/ltlast/multop.hh (is_And, is_Or): Fix constness.
      (is_Concat, is_Fusion): New functions.
      * src/ltlast/unop.hh (is_unop, is_X, is_F, is_G, is_GF, is_FG):
      Fix constness.
      (is_Not): New function.
      * src/ltlvisit/tostring.cc (strip_star_not, match_goto,
      emit_bunop_child, resugar_concat): New methods.
      (visit(bunop)): Rewrite without calling format().  Detect the
      [->i..j] pattern.
      (visit(multop)): Call resugar_concat to detect [=i..j] patterns.
      39417037
    • Alexandre Duret-Lutz's avatar
      Factor the code of ltl::to_string and ltl::to_spin_string. · e109f21c
      Alexandre Duret-Lutz authored
      * src/ltlvisit/tostring.cc (to_string_visitor): Take a list of
      keywords as fourth argument.
      (to_spin_string_visitor): Remove.
      (to_string, to_spin_string): Adjust usage of to_string_visitor.
      e109f21c
    • Alexandre Duret-Lutz's avatar
      Prefer "xor" over "^" when outputing formulae. · 62bf41cd
      Alexandre Duret-Lutz authored
      * src/ltlvisit/tostring.cc (to_string_visitor): Here.
      62bf41cd