Commit 126b724a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 47b2bea8
## Copyright (C) 2009, 2011 Laboratoire de Recherche et Dveloppement
## de l'Epita (LRDE).
## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et
## Dveloppement de l'Epita (LRDE).
## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
## dpartement Systmes Rpartis Coopratifs (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 \
......
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (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
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
// 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 <cassert>
#include <iostream>
#include <sstream>
#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<bunop*>(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<bunop*>(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;
}
}
}
// 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 <map>
#include <iosfwd>
#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<unsigned, unsigned> pairu;
typedef std::pair<type, formula*> pairo;
typedef std::pair<pairo, pairu> pair;
typedef std::map<pair, bunop*> 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
// Copyright (C) 2010 Laboratoire de Recherche et Developpement
// de l'Epita.
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
// (LIP6), dpartement Systmes Rpartis Coopratifs (SRC), Universit
// Pierre et Marie Curie.
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (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;
}
}
......
......@@ -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<unop*>(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()
......
......@@ -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
......
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (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;
};
......
......@@ -28,12 +28,15 @@
%debug
%error-verbose
%expect 0
%lex-param { spot::ltl::parse_error_list& error_list }
%code requires
{
#include <string>
#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 <num> 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 <str> 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 <ltl> subformula booleanatom rationalexp
%type <ltl> bracedrationalexp parenthesedsubformula
%type <minmax> starargs
%destructor { delete $$; } <str>
%destructor { $$->destroy(); } <ltl>
......@@ -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; }
......
......@@ -27,6 +27,7 @@
%{
#include <string>
#include <boost/lexical_cast.hpp>
#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)