From 126b724a989a1df0358e41048dbb4d3fba9636b7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 12 May 2010 19:09:20 +0200 Subject: [PATCH] Add support the bounded star operator [*i..j]. * 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. --- src/ltlast/Makefile.am | 6 +- src/ltlast/allnodes.hh | 3 +- src/ltlast/bunop.cc | 248 +++++++++++++++++++++++++++++++ src/ltlast/bunop.hh | 113 ++++++++++++++ src/ltlast/predecl.hh | 17 ++- src/ltlast/unop.cc | 16 +- src/ltlast/unop.hh | 5 - src/ltlast/visitor.hh | 4 + src/ltlparse/ltlparse.yy | 51 ++++++- src/ltlparse/ltlscan.ll | 31 +++- src/ltlparse/parsedecl.hh | 4 +- src/ltltest/consterm.test | 8 + src/ltltest/equals.test | 12 ++ src/ltltest/tostring.test | 6 + src/ltlvisit/basicreduce.cc | 10 +- src/ltlvisit/clone.cc | 9 +- src/ltlvisit/clone.hh | 3 +- src/ltlvisit/consterm.cc | 12 +- src/ltlvisit/dotty.cc | 14 +- src/ltlvisit/mark.cc | 19 ++- src/ltlvisit/nenoform.cc | 12 +- src/ltlvisit/postfix.cc | 14 ++ src/ltlvisit/postfix.hh | 4 + src/ltlvisit/reduce.cc | 14 +- src/ltlvisit/syntimpl.cc | 12 +- src/ltlvisit/tostring.cc | 57 ++++--- src/ltlvisit/tunabbrev.cc | 1 - src/tgba/formula2bdd.cc | 8 +- src/tgbaalgos/eltl2tgba_lacim.cc | 7 +- src/tgbaalgos/ltl2taa.cc | 7 +- src/tgbaalgos/ltl2tgba_fm.cc | 57 +++++-- src/tgbaalgos/ltl2tgba_lacim.cc | 7 +- src/tgbatest/ltl2tgba.test | 2 + 33 files changed, 678 insertions(+), 115 deletions(-) create mode 100644 src/ltlast/bunop.cc create mode 100644 src/ltlast/bunop.hh diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index a957a432a..990dc4f01 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -1,5 +1,5 @@ -## Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. @@ -31,6 +31,7 @@ ltlast_HEADERS = \ atomic_prop.hh \ automatop.hh \ binop.hh \ + bunop.hh \ constant.hh \ formula.hh \ formula_tree.hh \ @@ -46,6 +47,7 @@ libltlast_la_SOURCES = \ atomic_prop.cc \ automatop.cc \ binop.cc \ + bunop.cc \ constant.cc \ formula.cc \ formula_tree.cc \ diff --git a/src/ltlast/allnodes.hh b/src/ltlast/allnodes.hh index 6797892f4..e19d79060 100644 --- a/src/ltlast/allnodes.hh +++ b/src/ltlast/allnodes.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -34,5 +34,6 @@ # include "atomic_prop.hh" # include "constant.hh" # include "automatop.hh" +# include "bunop.hh" #endif // SPOT_LTLAST_ALLNODES_HH diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc new file mode 100644 index 000000000..b2f146704 --- /dev/null +++ b/src/ltlast/bunop.cc @@ -0,0 +1,248 @@ +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "bunop.hh" +#include "visitor.hh" +#include +#include +#include +#include "constant.hh" + +namespace spot +{ + namespace ltl + { + bunop::bunop(type op, formula* child, unsigned min, unsigned max) + : op_(op), child_(child), min_(min), max_(max) + { + } + + bunop::~bunop() + { + // Get this instance out of the instance map. + pair p(pairo(op(), child()), pairu(min_, max_)); + map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + + // Dereference child. + child()->destroy(); + } + + std::string + bunop::dump() const + { + std::ostringstream out; + out << "bunop(" << op_name() << ", " + << child()->dump() << ", " << min_ << ", "; + if (max_ == unbounded) + out << "unbounded"; + else + out << max_; + out << ")"; + return out.str(); + } + + void + bunop::accept(visitor& v) + { + v.visit(this); + } + + void + bunop::accept(const_visitor& v) const + { + v.visit(this); + } + + const formula* + bunop::child() const + { + return child_; + } + + formula* + bunop::child() + { + return child_; + } + + unsigned + bunop::min() const + { + return min_; + } + + unsigned + bunop::max() const + { + return max_; + } + + bunop::type + bunop::op() const + { + return op_; + } + + const char* + bunop::op_name() const + { + switch (op_) + { + case Star: + return "Star"; + } + // Unreachable code. + assert(0); + return 0; + } + + std::string + bunop::format() const + { + std::ostringstream out; + out << "[*"; + if (min_ != 0 || max_ != unbounded) + { + out << min_; + if (min_ != max_) + { + out << ".."; + if (max_ != unbounded) + out << max_; + } + } + out << "]"; + return out.str(); + } + + bunop::map bunop::instances; + + formula* + bunop::instance(type op, formula* child, unsigned min, unsigned max) + { + assert(min <= max); + + // Some trivial simplifications. + + // - [*0][*min..max] = [*0] + if (child == constant::empty_word_instance()) + return child; + + // - 0[*0..max] = [*0] + // - 0[*min..max] = 0 if min > 0 + if (child == constant::false_instance()) + { + if (min == 0) + return constant::empty_word_instance(); + else + return child; + } + + // - Exp[*0..0] = [*0] + if (max == 0) + { + child->destroy(); + return constant::empty_word_instance(); + } + + // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] if i*(min+1)<=j(min)+1. + bunop* s = dynamic_cast(child); + if (s) + { + unsigned i = s->min(); + unsigned j = s->max(); + + // Exp has to be true between i*min and j*min + // then between i*(min+1) and j*(min+1) + // ... + // finally between i*max and j*max + // + // We can merge these intervals into [i*min..j*max] iff the + // first are adjacent or overlap, i.e. iff + // i*(min+1) <= j*min+1. + // (Because i<=j, this entails that the other intervals also + // overlap). + + formula* exp = s->child(); + if (j == unbounded) + { + min *= i; + max = unbounded; + + // Exp[*min..max] + exp->clone(); + child->destroy(); + child = exp; + } + else + { + if (i * (min + 1) <= (j * min) + 1) + { + min *= i; + if (max != unbounded) + { + if (j == unbounded) + max = unbounded; + else + max *= j; + } + exp->clone(); + child->destroy(); + child = exp; + } + } + } + + pair p(pairo(op, child), pairu(min, max)); + map::iterator i = instances.find(p); + if (i != instances.end()) + { + // This instance already exists. + child->destroy(); + return i->second->clone(); + } + bunop* ap = new bunop(op, child, min, max); + instances[p] = ap; + return static_cast(ap->clone()); + } + + unsigned + bunop::instance_count() + { + return instances.size(); + } + + std::ostream& + bunop::dump_instances(std::ostream& os) + { + for (map::iterator i = instances.begin(); i != instances.end(); ++i) + { + os << i->second << " = " + << i->second->ref_count_() << " * " + << i->second->dump() + << std::endl; + } + return os; + } + + } +} diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh new file mode 100644 index 000000000..5738c57ad --- /dev/null +++ b/src/ltlast/bunop.hh @@ -0,0 +1,113 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +/// \file ltlast/bunop.hh +/// \brief Bounded Unary operators +#ifndef SPOT_LTLAST_BUNOP_HH +# define SPOT_LTLAST_BUNOP_HH + +#include +#include +#include "refformula.hh" + +namespace spot +{ + namespace ltl + { + + /// \brief Bounded unary operator. + /// \ingroup ltl_ast + class bunop : public ref_formula + { + public: + enum type { Star }; + + static const unsigned unbounded = -1U; + + /// \brief Build a bunop with bounds \a min and \a max. + /// + /// The following trivial simplifications are performed + /// automatically (the left expression is rewritten as the right + /// expression): + /// - 0[*0..max] = [*0] + /// - 0[*min..max] = 0 if min > 0 + /// - [*0][*min..max] = [*0] + /// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1. + /// + /// These rewriting rules imply that it is not possible to build + /// an LTL formula object that is SYNTACTICALLY equal to one of + /// these left expressions. + static formula* instance(type op, + formula* child, + unsigned min = 0, + unsigned max = unbounded); + + virtual void accept(visitor& v); + virtual void accept(const_visitor& v) const; + + /// Get the sole operand of this operator. + const formula* child() const; + /// Get the sole operand of this operator. + formula* child(); + + /// Minimum number of repetition. + unsigned min() const; + /// Minimum number of repetition. + unsigned max() const; + + /// \brief A string representation of the operator. + /// + /// For instance "[*2..]". + std::string format() const; + + /// Get the type of this operator. + type op() const; + /// Get the type of this operator, as a string. + const char* op_name() const; + + /// Return a canonic representation of operation. + virtual std::string dump() const; + + /// Number of instantiated unary operators. For debugging. + static unsigned instance_count(); + + /// Dump all instances. For debugging. + static std::ostream& dump_instances(std::ostream& os); + + protected: + typedef std::pair pairu; + typedef std::pair pairo; + typedef std::pair pair; + typedef std::map map; + static map instances; + + bunop(type op, formula* child, unsigned min, unsigned max); + virtual ~bunop(); + + private: + type op_; + formula* child_; + unsigned min_; + unsigned max_; + }; + + } +} +#endif // SPOT_LTLAST_BUNOP_HH diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh index 611b6884d..fccd25361 100644 --- a/src/ltlast/predecl.hh +++ b/src/ltlast/predecl.hh @@ -1,8 +1,8 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement -// de l'Epita. -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université -// Pierre et Marie Curie. +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -39,12 +39,13 @@ namespace spot struct const_visitor; class atomic_prop; - class unop; - class constant; + class automatop; class binop; + class bunop; + class constant; class formula; class multop; - class automatop; + class unop; } } diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index bc67c2ea9..a5d78c697 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -99,8 +99,6 @@ namespace spot return "G"; case Finish: return "Finish"; - case Star: - return "Star"; case Closure: return "Closure"; case NegClosure: @@ -120,26 +118,14 @@ namespace spot // Some trivial simplifications. switch (op) { - // We have (0*) == ([*0]) - // ([*0]*) == ([*0]) - case Star: - if (child == constant::false_instance() - || child == constant::empty_word_instance()) - return constant::empty_word_instance(); - - // -- fall thru -- - case F: case G: { - // F, G, * are idempotent. + // F and G are idempotent. unop* u = dynamic_cast(child); if (u && u->op() == op) return u; - if (op == Star) - break; - // F(0) = G(0) = 0 // F(1) = G(1) = 1 if (child == constant::false_instance() diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 37c40ea6b..153eb19cc 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -45,8 +45,6 @@ namespace spot Not, X, F, G, // ELTL Finish, - // Kleene Star - Star, // Closure Closure, NegClosure, }; @@ -57,9 +55,6 @@ namespace spot /// The following trivial simplifications are performed /// automatically (the left expression is rewritten as the right /// expression): - /// - 0* = [*0] - /// - [*0]* = [*0] - /// - Exp** = Exp* /// - FF(Exp) = F(Exp) /// - GG(Exp) = G(Exp) /// - F(0) = 0 diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index b6a7c6a6d..66fcc89b3 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -48,6 +50,7 @@ namespace spot virtual void visit(unop* node) = 0; virtual void visit(multop* node) = 0; virtual void visit(automatop* node) = 0; + virtual void visit(bunop* node) = 0; }; /// \brief Formula visitor that cannot modify the formula. @@ -67,6 +70,7 @@ namespace spot virtual void visit(const unop* node) = 0; virtual void visit(const multop* node) = 0; virtual void visit(const automatop* node) = 0; + virtual void visit(const bunop* node) = 0; }; diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 24193cc1e..56cf7c374 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -28,12 +28,15 @@ %debug %error-verbose %expect 0 +%lex-param { spot::ltl::parse_error_list& error_list } %code requires { #include #include "public.hh" #include "ltlast/allnodes.hh" + + struct minmax_t { unsigned min, max; }; } %parse-param {spot::ltl::parse_error_list &error_list} @@ -43,6 +46,8 @@ { std::string* str; spot::ltl::formula* ltl; + unsigned num; + minmax_t minmax; } %code { @@ -85,6 +90,10 @@ using namespace spot::ltl; %token OP_W "weak until operator" OP_M "strong release operator" %token OP_F "sometimes operator" OP_G "always operator" %token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator" +%token OP_STAR_OPEN "opening bracket for star operator" +%token OP_STAR_CLOSE "closing bracket for star operator" +%token OP_STAR_NUM "number for star operator" +%token OP_STAR_SEP "separator for star operator" %token OP_UCONCAT "universal concat operator" %token OP_ECONCAT "existential concat operator" %token OP_UCONCAT_NONO "universal non-overlapping concat operator" @@ -92,7 +101,7 @@ using namespace spot::ltl; %token ATOMIC_PROP "atomic proposition" %token OP_CONCAT "concat operator" OP_FUSION "fusion operator" %token CONST_TRUE "constant true" CONST_FALSE "constant false" -%token END_OF_INPUT "end of formula" CONST_EMPTYWORD "empty word" +%token END_OF_INPUT "end of formula" %token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix" /* Priorities. */ @@ -114,7 +123,7 @@ using namespace spot::ltl; %nonassoc OP_X /* High priority regex operator. */ -%nonassoc OP_STAR +%nonassoc OP_STAR OP_STAR_OPEN /* Not has the most important priority after Wring's `=0' and `=1'. */ %nonassoc OP_NOT @@ -123,6 +132,7 @@ using namespace spot::ltl; %type subformula booleanatom rationalexp %type bracedrationalexp parenthesedsubformula +%type starargs %destructor { delete $$; } %destructor { $$->destroy(); } @@ -175,6 +185,32 @@ enderror: error END_OF_INPUT "ignoring trailing garbage")); } + +OP_STAR_SEP_opt: | OP_STAR_SEP +error_opt: | error + +starargs: OP_STAR + { $$.min = 0U; $$.max = bunop::unbounded; } + | OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_NUM OP_STAR_CLOSE + { $$.min = $2; $$.max = $4; } + | OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_CLOSE + { $$.min = $2; $$.max = bunop::unbounded; } + | OP_STAR_OPEN OP_STAR_SEP OP_STAR_NUM OP_STAR_CLOSE + { $$.min = 0U; $$.max = $3; } + | OP_STAR_OPEN OP_STAR_SEP_opt OP_STAR_CLOSE + { $$.min = 0U; $$.max = bunop::unbounded; } + | OP_STAR_OPEN OP_STAR_NUM OP_STAR_CLOSE + { $$.min = $2; $$.max = $2; } + | OP_STAR_OPEN error OP_STAR_CLOSE + { error_list.push_back(parse_error(@$, + "treating this star block as [*]")); + $$.min = 0U; $$.max = bunop::unbounded; } + | OP_STAR_OPEN error_opt END_OF_INPUT + { error_list.push_back(parse_error(@$, + "missing closing bracket for star")); + $$.min = $$.max = 0U; } + + /* The reason we use `constant::false_instance()' for error recovery is that it isn't reference counted. (Hence it can't leak references.) */ @@ -239,8 +275,6 @@ rationalexp: booleanatom | OP_NOT booleanatom { $$ = unop::instance(unop::Not, $2); } | bracedrationalexp - | CONST_EMPTYWORD - { $$ = constant::empty_word_instance(); } | PAR_OPEN rationalexp PAR_CLOSE { $$ = $2; } | PAR_OPEN error PAR_CLOSE @@ -281,10 +315,11 @@ rationalexp: booleanatom { $$ = multop::instance(multop::Fusion, $1, $3); } | rationalexp OP_FUSION error { missing_right_binop($$, $1, @2, "fusion operator"); } - | rationalexp OP_STAR - { $$ = unop::instance(unop::Star, $1); } - | OP_STAR - { $$ = unop::instance(unop::Star, constant::true_instance()); } + | rationalexp starargs + { $$ = bunop::instance(bunop::Star, $1, $2.min, $2.max); } + | starargs + { $$ = bunop::instance(bunop::Star, constant::true_instance(), + $1.min, $1.max); } bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE { $$ = $2; } diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 0db5ddc5f..64d734973 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -27,6 +27,7 @@ %{ #include +#include #include "ltlparse/parsedecl.hh" /* Hack Flex so we read from a string instead of reading from a file. */ @@ -58,6 +59,7 @@ flex_set_buffer(const char* buf, int start_tok) %} %s not_prop +%x star %% @@ -86,14 +88,33 @@ flex_set_buffer(const char* buf, int start_tok) "!"|"~" BEGIN(0); return token::OP_NOT; /* PSL operators */ -"[*0]" BEGIN(0); return token::CONST_EMPTYWORD; "[]->"|"|->" BEGIN(0); return token::OP_UCONCAT; "<>->" BEGIN(0); return token::OP_ECONCAT; "[]=>"|"|=>" BEGIN(0); return token::OP_UCONCAT_NONO; "<>=>" BEGIN(0); return token::OP_ECONCAT_NONO; -"*"|"[*]" BEGIN(0); return token::OP_STAR; ";" BEGIN(0); return token::OP_CONCAT; ":" BEGIN(0); return token::OP_FUSION; +"*"|"[*]" BEGIN(0); return token::OP_STAR; +"[*" BEGIN(star); return token::OP_STAR_OPEN; +"]" BEGIN(0); return token::OP_STAR_CLOSE; +[0-9]+ { + unsigned num = 0; + try { + num = boost::lexical_cast(yytext); + yylval->num = num; + return token::OP_STAR_NUM; + } + catch (boost::bad_lexical_cast &) + { + error_list.push_back( + spot::ltl::parse_error(*yylloc, + "value too large ignored")); + // Skip this number and read next token + yylloc->step(); + } + } +","|".." return token::OP_STAR_SEP; + /* & and | come from Spin. && and || from LTL2BA. /\, \/, and xor are from LBTT. @@ -122,7 +143,7 @@ flex_set_buffer(const char* buf, int start_tok) "=0" return token::OP_POST_NEG; "=1" return token::OP_POST_POS; -[ \t\n]+ /* discard whitespace */ yylloc->step (); +<*>[ \t\n]+ /* discard whitespace */ yylloc->step (); /* An Atomic proposition cannot start with the letter used by a unary operator (F,G,X), unless this @@ -142,7 +163,7 @@ flex_set_buffer(const char* buf, int start_tok) condition we will not consider `Uq' as an atomic proposition but as a `U' operator followed by a `q' atomic proposition. - We also disable atomic proposition that may look a combination + We also disable atomic proposition that may look like a combination of a binary operator followed by several unary operators. E.g. UFXp. This way, `p=0UFXp=1' will be parsed as `(p=0)U(F(X(p=1)))'. */ @@ -161,7 +182,7 @@ flex_set_buffer(const char* buf, int start_tok) return token::ATOMIC_PROP; } -. return *yytext; +<*>. return *yytext; <> return token::END_OF_INPUT; diff --git a/src/ltlparse/parsedecl.hh b/src/ltlparse/parsedecl.hh index 8c5edbfd8..b54b8bb5d 100644 --- a/src/ltlparse/parsedecl.hh +++ b/src/ltlparse/parsedecl.hh @@ -28,7 +28,9 @@ #include "location.hh" # define YY_DECL \ - int ltlyylex (ltlyy::parser::semantic_type *yylval, ltlyy::location *yylloc) + int ltlyylex (ltlyy::parser::semantic_type *yylval, \ + ltlyy::location *yylloc, \ + spot::ltl::parse_error_list& error_list) YY_DECL; void flex_set_buffer(const char *buf, int start_tok); diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test index c01f92f4e..cd4dc54c9 100755 --- a/src/ltltest/consterm.test +++ b/src/ltltest/consterm.test @@ -32,6 +32,14 @@ run 0 ../consterm '0' run 1 ../consterm '[*0]' run 1 ../consterm 'a*' run 1 ../consterm '0*' +run 1 ../consterm 'a[*0]' +run 1 ../consterm 'a[*0..]' +run 1 ../consterm 'a[*0..3]' +run 0 ../consterm 'a[*1..3]' +run 0 ../consterm 'a[*3]' +run 1 ../consterm 'a[*..4][*3]' +run 0 ../consterm 'a[*1..4][*3]' +run 1 ../consterm 'a[*1..4][*0..3]' run 0 ../consterm '((a ; b) + c)' run 1 ../consterm '((a ; b) + [*0])' run 0 ../consterm '((a ; b) + [*0]) & e' diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index ce4f68811..b91851bfc 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -122,3 +122,15 @@ run 0 ../equals '{x;x}[]->GX(1)' '1' run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0' run 0 ../equals '{x;x}[]->y' '{x;x}|->y' run 0 ../equals '{x;x}[]->y' '{x;x}(y)' + +run 0 ../equals '{a[*0]}' '{[*0]}' +run 0 ../equals '{a[*..]}' '{a[*]}' +run 0 ../equals '{a[*2..3][*4..5]}' '{a[*8..15]}' +run 0 ../equals '{a[*4..5][*2..3]}' '{a[*4..5][*2..3]}' +run 0 ../equals '{a[*2..3][*]}' '{a[*2..3][*]}' +run 0 ../equals '{a[*1..3][*]}' '{a[*]}' +run 0 ../equals '{a[*][*2..3]}' '{a[*]}' +run 0 ../equals '{a[*..3][*2]}' '{a[*..6]}' +run 0 ../equals '{a[*..3][*..2]}' '{a[*..6]}' +run 0 ../equals '{a[*..3][*2..]}' '{a[*]}' +run 0 ../equals '{a[*..3][*2..]}' '{a[*]}' diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test index bca0c66fb..9f0e9f39d 100755 --- a/src/ltltest/tostring.test +++ b/src/ltltest/tostring.test @@ -61,3 +61,9 @@ run 0 ../tostring '{a;b;{c && d*};**}|=>G{a*:b*}' run 0 ../tostring 'GF!{{a || c} && b}' run 0 ../tostring 'GF!{{a || c*} && b}<>->{{!a}*}' run 0 ../tostring 'GF{{a || c*} & b[*]}[]->{d}' +run 0 ../tostring '{a[*2..3]}' +run 0 ../tostring '{a[*0..1]}' +run 0 ../tostring '{a[*0..]}' +run 0 ../tostring '{a[*..]}' +run 0 ../tostring '{a[*1..]}' +run 0 ../tostring '{a[*2..3][*4..5]}' diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index d1762fb45..190b915b7 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -75,8 +75,13 @@ namespace spot void visit(atomic_prop* ap) { - formula* f = ap->clone(); - result_ = f; + result_ = ap->clone(); + } + + void + visit(bunop* bo) + { + result_ = bo->clone(); } void @@ -239,7 +244,6 @@ namespace spot return; case unop::Finish: - case unop::Star: case unop::Closure: case unop::NegClosure: result_ = unop::instance(uo->op(), result_); diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 806ad3bb3..94b3164af 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -54,6 +54,13 @@ namespace spot result_ = c->clone(); } + void + clone_visitor::visit(bunop* bo) + { + result_ = bunop::instance(bo->op(), recurse(bo->child()), + bo->min(), bo->max()); + } + void clone_visitor::visit(unop* uo) { diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 8965a8d89..6b4430ecb 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -52,6 +52,7 @@ namespace spot void visit(automatop* mo); void visit(multop* mo); void visit(constant* c); + void visit(bunop* c); virtual formula* recurse(formula* f); diff --git a/src/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc index 87f5afb7f..f0289179f 100644 --- a/src/ltlvisit/consterm.cc +++ b/src/ltlvisit/consterm.cc @@ -70,6 +70,15 @@ namespace spot } } + void + visit(const bunop* bo) + { + if (bo->min() == 0) + result_ = true; + else + bo->child()->accept(*this); + } + void visit(const unop* uo) { @@ -78,9 +87,6 @@ namespace spot case unop::Not: result_ = false; break; - case unop::Star: - result_ = true; - break; case unop::X: case unop::F: case unop::G: diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index fc768fa9b..ab495e1a9 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -60,6 +60,16 @@ namespace spot draw_node_(c, c->val_name(), true); } + void + visit(const bunop* so) + { + if (draw_node_(so, so->format(), true)) + { + dir = none; + so->child()->accept(*this); + } + } + void visit(const binop* bo) { diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index c4b858cf9..73d003472 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -58,6 +58,11 @@ namespace spot { } + void + visit(bunop*) + { + } + void visit(unop* uo) { @@ -67,7 +72,6 @@ namespace spot result_ = true; return; case unop::Finish: - case unop::Star: case unop::Closure: case unop::Not: case unop::X: @@ -161,6 +165,12 @@ namespace spot result_ = c->clone(); } + void + visit(bunop* bo) + { + result_ = bo->clone(); + } + void visit(unop* uo) { @@ -170,7 +180,6 @@ namespace spot has_mark_ = true; /* fall through */ case unop::Finish: - case unop::Star: case unop::Closure: case unop::Not: case unop::X: @@ -322,6 +331,12 @@ namespace spot result_ = c->clone(); } + void + visit(bunop* bo) + { + result_ = bo->clone(); + } + void visit(unop* uo) { diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index a77c73abf..294a0da1a 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -119,9 +119,7 @@ namespace spot recurse_(f, false)); return; /* !Finish(x), is not simplified */ - /* !(a*) is not simplified */ case unop::Finish: - case unop::Star: result_ = unop::instance(uo->op(), recurse_(f, false)); if (negated_) result_ = unop::instance(unop::Not, result_); @@ -131,6 +129,16 @@ namespace spot assert(0); } + void + visit(bunop* bo) + { + // !(a*) is not simplified + result_ = bunop::instance(bo->op(), recurse_(bo->child(), false), + bo->min(), bo->max()); + if (negated_) + result_ = unop::instance(unop::Not, result_); + } + void visit(binop* bo) { diff --git a/src/ltlvisit/postfix.cc b/src/ltlvisit/postfix.cc index 9b7fe1e2c..175a70952 100644 --- a/src/ltlvisit/postfix.cc +++ b/src/ltlvisit/postfix.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -73,6 +75,12 @@ namespace spot doit(mo); } + void + postfix_visitor::visit(bunop* so) + { + doit(so); + } + void postfix_visitor::visit(constant* c) { @@ -109,6 +117,12 @@ namespace spot doit_default(ao); } + void + postfix_visitor::doit(bunop* so) + { + doit_default(so); + } + void postfix_visitor::doit(constant* c) { diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh index f467ed16c..b360c1a2c 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -47,6 +49,7 @@ namespace spot void visit(multop* mo); void visit(automatop* c); void visit(constant* c); + void visit(bunop* c); virtual void doit(atomic_prop* ap); virtual void doit(unop* uo); @@ -54,6 +57,7 @@ namespace spot virtual void doit(multop* mo); virtual void doit(automatop* mo); virtual void doit(constant* c); + virtual void doit(bunop* c); virtual void doit_default(formula* f); }; } diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 330a8bc0a..66cb9fa85 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -93,6 +93,12 @@ namespace spot ret_.v = 0; } + void + visit(const bunop*) + { + ret_.v = 0; + } + void visit(const unop* uo) { @@ -228,6 +234,13 @@ namespace spot result_ = c; } + void + visit(bunop* bo) + { + result_ = bunop::instance(bo->op(), recurse(bo->child()), + bo->min(), bo->max()); + } + void visit(unop* uo) { @@ -252,7 +265,6 @@ namespace spot case unop::Not: case unop::X: case unop::Finish: - case unop::Star: case unop::Closure: case unop::NegClosure: result_ = unop::instance(uo->op(), result_); diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 248751ed7..ab5fcaefb 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -79,6 +79,11 @@ namespace spot } } + void + visit(const bunop*) + { + } + void visit(const unop* uo) { @@ -106,7 +111,6 @@ namespace spot result_ = true; return; case unop::Finish: - case unop::Star: case unop::Closure: case unop::NegClosure: return; @@ -265,6 +269,11 @@ namespace spot result_ = v.result(); } + void + visit(const bunop*) + { + } + void visit(const constant* c) { @@ -339,7 +348,6 @@ namespace spot return; } case unop::Finish: - case unop::Star: case unop::Closure: case unop::NegClosure: return; diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 5b8032342..af55339db 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -179,6 +179,31 @@ namespace spot closep(); } + void + visit(const bunop* bo) + { + // Abbreviate "1*" as "*". + if (bo->child() != constant::true_instance()) + { + // a* is OK, no need to print {a}*. + // However want braces for {!a}*, the only unary + // operator that can be nested with *. + bool need_parent = !!dynamic_cast(bo->child()); + + if (need_parent || full_parent_) + openp(); + bo->child()->accept(*this); + if (need_parent || full_parent_) + closep(); + } + + // Output "*" instead of "[*]". + if (bo->min() == 0 && bo->max() == bunop::unbounded) + os_ << "*"; + else + os_ << bo->format(); + } + void visit(const unop* uo) { @@ -225,19 +250,6 @@ namespace spot in_ratexp_ = true; top_level_ = true; break; - case unop::Star: - // Abbreviate "1*" as "*". - if (uo->child() == constant::true_instance()) - { - os_ << "*"; - return; - } - // 1* is OK, no need to print {1}*. - // However want braces for {!a}*, the only unary - // operator that can be nested with *. - need_parent = !!dynamic_cast(uo->child()); - // Do not output anything yet, star is a postfix operator. - break; } top_level_ = false; @@ -249,9 +261,6 @@ namespace spot switch (uo->op()) { - case unop::Star: - os_ << "*"; - break; case unop::Closure: case unop::NegClosure: os_ << "}"; @@ -476,19 +485,6 @@ namespace spot top_level_ = true; in_ratexp_ = true; break; - case unop::Star: - // Abbreviate "1*" as "*". - if (uo->child() == constant::true_instance()) - { - os_ << "*"; - return; - } - // 1* is OK, no need to print {1}*. - // However want braces for {!a}*, the only unary - // operator that can be nested with *. - need_parent = !!dynamic_cast(uo->child()); - // Do not output anything yet, star is a postfix operator. - break; } if (need_parent) @@ -499,9 +495,6 @@ namespace spot switch (uo->op()) { - case unop::Star: - os_ << "*"; - break; case unop::Closure: case unop::NegClosure: os_ << "}"; diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index e12dbc464..21c65d59a 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -44,7 +44,6 @@ namespace spot case unop::Finish: case unop::X: case unop::Not: - case unop::Star: case unop::Closure: case unop::NegClosure: this->super::visit(uo); diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 8c0eb945c..202b9fad8 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -70,6 +70,13 @@ namespace spot assert(0); } + virtual void + visit(const bunop*) + { + assert(!"unsupported operator"); + return; + } + virtual void visit(const unop* node) { @@ -79,7 +86,6 @@ namespace spot case unop::F: case unop::G: case unop::X: - case unop::Star: case unop::Closure: case unop::NegClosure: assert(!"unsupported operator"); diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index e00cae023..16c4ada42 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -101,7 +101,6 @@ namespace spot case unop::X: case unop::F: case unop::G: - case unop::Star: case unop::Closure: case unop::NegClosure: assert(!"unsupported operator"); @@ -110,6 +109,12 @@ namespace spot assert(0); } + void + visit(const bunop*) + { + assert(!"unsupported operator"); + } + void visit(const binop* node) { diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index bf8175bf5..b6cea7d0c 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -141,7 +141,6 @@ namespace spot succ_ = v.succ_; return; case unop::Finish: - case unop::Star: case unop::Closure: case unop::NegClosure: assert(!"unsupported operator"); @@ -151,6 +150,12 @@ namespace spot assert(0); } + void + visit(const bunop*) + { + assert(!"unsupported operator"); + } + void visit(const binop* node) { diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 9adc14510..cdfce762d 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -380,18 +380,34 @@ namespace spot res_ = !recurse(f) & next_to_concat(); return; } - case unop::Star: - { - formula* f; - if (to_concat_) - f = multop::instance(multop::Concat, node->clone(), - to_concat_->clone()); - else - f = node->clone(); + } + /* Unreachable code. */ + assert(0); + } - res_ = recurse(node->child(), f) | now_to_concat(); - return; - } + void + visit(const bunop* bo) + { + formula* f; + unsigned min = bo->min(); + unsigned max = bo->max(); + unsigned min2 = (min == 0) ? 0 : (min - 1); + unsigned max2 = + (max == bunop::unbounded) ? bunop::unbounded : (max - 1); + + bunop::type op = bo->op(); + switch (op) + { + case bunop::Star: + f = bunop::instance(op, bo->child()->clone(), min2, max2); + + if (to_concat_) + f = multop::instance(multop::Concat, f, to_concat_->clone()); + + res_ = recurse(bo->child(), f); + if (min == 0) + res_ |= now_to_concat(); + return; } /* Unreachable code. */ assert(0); @@ -452,8 +468,8 @@ namespace spot // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] formula* f = multop::instance(multop::Or, final); formula* n = multop::instance(multop::AndNLM, non_final); - formula* t = unop::instance(unop::Star, - constant::true_instance()); + formula* t = bunop::instance(bunop::Star, + constant::true_instance()); formula* ft = multop::instance(multop::Concat, f->clone(), t->clone()); formula* nt = multop::instance(multop::Concat, @@ -887,12 +903,15 @@ namespace spot case unop::Finish: assert(!"unsupported operator"); break; - case unop::Star: - assert(!"Not an LTL operator"); - break; } } + void + visit(const bunop*) + { + assert(!"Not an LTL operator"); + } + void visit(const binop* node) { @@ -1225,6 +1244,12 @@ namespace spot assert(!"unsupported operator"); } + void + visit(const bunop*) + { + assert(!"unsupported operator"); + } + void visit(const multop* node) { diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index c2cc4c06c..1bf4d4d15 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -150,7 +150,6 @@ namespace spot return; } case unop::Finish: - case unop::Star: case unop::Closure: case unop::NegClosure: assert(!"unsupported operator"); @@ -159,6 +158,12 @@ namespace spot assert(0); } + void + visit(const bunop*) + { + assert(!"unsupported operator"); + } + void visit(const binop* node) { diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 72a155fea..ffb33b80f 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -81,6 +81,8 @@ check_psl '{a*&b}' check_psl '{a*&b*}' check_psl '{((!c;b*) & d);e}' check_psl '{(a* & (c;b*) & d);e}' +check_psl '{[*2];a[*2..4]}|->b' +check_psl '{a[*2..5] && b[*..3]}|->c' # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Ruah, Zarpas (2007). check_psl '{[*];req;ack}|=>{start;busy[*];done}'