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

Parse the fusion operator (":") and translate it in ltl2tgba_fm().

* 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.
parent ad519b85
// 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), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie.
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
......@@ -113,6 +113,8 @@ namespace spot
return "Or";
case Concat:
return "Concat";
case Fusion:
return "Fusion";
}
// Unreachable code.
assert(0);
......@@ -149,48 +151,60 @@ namespace spot
}
else
{
// All operator except "Concat" not commutative, so
// we just keep a list of the inlined arguments that
// should later be added to the vector.
// All operator except "Concat" and "Fusion" are
// commutative, so we just keep a list of the inlined
// arguments that should later be added to the vector.
// For concat we have to keep track of the order of
// all the arguments.
if (op == Concat)
if (op == Concat || op == Fusion)
inlined.push_back(*i);
++i;
}
}
if (op == Concat)
if (op == Concat || op == Fusion)
*v = inlined;
else
v->insert(v->end(), inlined.begin(), inlined.end());
}
if (op != Concat)
if (op != Concat && op != Fusion)
std::sort(v->begin(), v->end(), formula_ptr_less_than());
formula* neutral;
formula* abs;
formula* abs2;
formula* weak_abs;
switch (op)
{
case And:
neutral = constant::true_instance();
abs = constant::false_instance();
abs2 = 0;
weak_abs = constant::empty_word_instance();
break;
case Or:
neutral = constant::false_instance();
abs = constant::true_instance();
abs2 = 0;
weak_abs = 0;
break;
case Concat:
neutral = constant::empty_word_instance();
abs = constant::false_instance();
abs2 = 0;
weak_abs = 0;
break;
case Fusion:
neutral = constant::true_instance();
abs = constant::false_instance();
abs2 = constant::empty_word_instance();
weak_abs = 0;
break;
default:
neutral = 0;
abs = 0;
abs2 = 0;
weak_abs = 0;
break;
}
......@@ -209,7 +223,7 @@ namespace spot
(*i)->destroy();
i = v->erase(i);
}
else if (*i == abs)
else if (*i == abs || *i == abs2)
{
for (i = v->begin(); i != v->end(); ++i)
(*i)->destroy();
......
......@@ -41,7 +41,7 @@ namespace spot
class multop : public ref_formula
{
public:
enum type { Or, And, Concat };
enum type { Or, And, Concat, Fusion };
/// List of formulae.
typedef std::vector<formula*> vec;
......
......@@ -83,11 +83,11 @@ using namespace spot::ltl;
%token OP_U "until operator" OP_R "release operator"
%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"
%token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator"
%token OP_UCONCAT "universal concat operator"
%token OP_ECONCAT "existential concat operator"
%token <str> ATOMIC_PROP "atomic proposition"
%token OP_STAR "star operator" OP_CONCAT "concat operator"
%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 OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
......@@ -97,7 +97,7 @@ using namespace spot::ltl;
/* Low priority regex operator. */
%left OP_UCONCAT OP_ECONCAT
%left OP_CONCAT
%left OP_CONCAT OP_FUSION
/* Logical operators. */
%left OP_IMPLIES OP_EQUIV
......@@ -264,6 +264,10 @@ rationalexp: booleanatom
{ $$ = multop::instance(multop::Concat, $1, $3); }
| rationalexp OP_CONCAT error
{ missing_right_binop($$, $1, @2, "concat operator"); }
| rationalexp OP_FUSION rationalexp
{ $$ = 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); }
......
......@@ -97,6 +97,7 @@ flex_set_buffer(const char* buf, int start_tok)
"<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV;
"*" BEGIN(0); return token::OP_STAR;
";" BEGIN(0); return token::OP_CONCAT;
":" BEGIN(0); return token::OP_FUSION;
"[]->" BEGIN(0); return token::OP_UCONCAT;
"<>->" BEGIN(0); return token::OP_ECONCAT;
......
......@@ -787,6 +787,7 @@ namespace spot
break;
case multop::Concat:
case multop::Fusion:
std::copy(res->begin(), res->end(), tmpOther->end());
break;
}
......
......@@ -97,6 +97,13 @@ namespace spot
void
visit(const multop* mo)
{
// The fusion operator cannot be used to recognize the empty word.
if (mo->op() == multop::Fusion)
{
result_ = false;
return;
}
unsigned max = mo->size();
// This sets the initial value of result_.
mo->nth(0)->accept(*this);
......@@ -118,6 +125,10 @@ namespace spot
if (!result_)
return;
break;
case multop::Fusion:
/* Unreachable code */
assert(0);
break;
}
}
}
......
......@@ -356,6 +356,7 @@ namespace spot
}
break;
case multop::Concat:
case multop::Fusion:
break;
}
if (changed)
......
......@@ -166,6 +166,7 @@ namespace spot
{
case multop::Or:
case multop::Concat:
case multop::Fusion:
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
break;
......
......@@ -226,23 +226,30 @@ namespace spot
op = multop::And;
break;
case multop::Concat:
case multop::Fusion:
break;
}
multop::vec* res = new multop::vec;
unsigned mos = mo->size();
if (op != multop::Concat)
switch (op)
{
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
result_ = multop::instance(op, res);
}
else
{
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse_(mo->nth(i), false));
result_ = multop::instance(op, res);
if (negated_)
result_ = unop::instance(unop::Not, result_);
case multop::And:
case multop::Or:
{
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
result_ = multop::instance(op, res);
break;
}
case multop::Concat:
case multop::Fusion:
{
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse_(mo->nth(i), false));
result_ = multop::instance(op, res);
if (negated_)
result_ = unop::instance(unop::Not, result_);
}
}
}
......
......@@ -203,6 +203,7 @@ namespace spot
result_ = true;
break;
case multop::Concat:
case multop::Fusion:
break;
}
}
......@@ -458,6 +459,7 @@ namespace spot
result_ = true;
break;
case multop::Concat:
case multop::Fusion:
break;
}
}
......
......@@ -259,6 +259,9 @@ namespace spot
case multop::Concat:
ch = ";";
break;
case multop::Fusion:
ch = ":";
break;
}
for (unsigned n = 1; n < max; ++n)
......@@ -460,6 +463,9 @@ namespace spot
case multop::Concat:
ch = ";";
break;
case multop::Fusion:
ch = ":";
break;
}
for (unsigned n = 1; n < max; ++n)
......
......@@ -142,6 +142,7 @@ namespace spot
res_ = bddfalse;
break;
case multop::Concat:
case multop::Fusion:
assert(!"unsupported operator");
}
assert(op != -1);
......
......@@ -159,6 +159,7 @@ namespace spot
res_ = bddfalse;
break;
case multop::Concat:
case multop::Fusion:
assert(!"unsupported operator");
}
assert(op != -1);
......
......@@ -323,6 +323,7 @@ namespace spot
}
return;
case multop::Concat:
case multop::Fusion:
assert(!"unsupported operator");
return;
}
......
......@@ -486,6 +486,70 @@ namespace spot
multop::instance(multop::Concat, v));
break;
}
case multop::Fusion:
{
assert(node->size() >= 2);
// the head
bdd res = recurse(node->nth(0));
// the tail
multop::vec* v = new multop::vec;
unsigned s = node->size();
v->reserve(s - 1);
for (unsigned n = 1; n < s; ++n)
v->push_back(node->nth(n)->clone());
formula* tail = multop::instance(multop::Fusion, v);
bdd tail_bdd;
bool tail_computed = false;
//trace_ltl_bdd(dict_, res);
minato_isop isop(res);
bdd cube;
res_ = bddfalse;
while ((cube = isop.next()) != bddfalse)
{
bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_formula(dest_bdd);
if (constant_term_as_bool(dest))
{
// The destination is a final state. Make sure we
// can also exit if tail is satisfied.
if (!tail_computed)
{
tail_bdd = recurse(tail,
to_concat_ ?
to_concat_->clone() : 0);
tail_computed = true;
}
res_ |= label & tail_bdd;
}
if (dynamic_cast<constant*>(dest) == 0)
{
// If the destination is not a constant, it
// means it can have successors. Fusion the
// tail and append anything to concatenate.
formula* dest2 = multop::instance(multop::Fusion, dest,
tail->clone());
if (to_concat_)
dest2 = multop::instance(multop::Concat, dest2,
to_concat_->clone());
if (dest2 != constant::false_instance())
{
int x = dict_.register_next_variable(dest2);
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
}
}
tail->destroy();
break;
}
}
}
......@@ -822,6 +886,7 @@ namespace spot
break;
}
case multop::Concat:
case multop::Fusion:
assert(!"Not an LTL operator");
break;
}
......
......@@ -257,6 +257,7 @@ namespace spot
res_ = bddfalse;
break;
case multop::Concat:
case multop::Fusion:
assert(!"unsupported operator");
}
assert(op != -1);
......
......@@ -64,6 +64,10 @@ check_psl '{((a*;b;c)*)&((b*;a;c)*)}<>->x'
check_psl '{(g;y;r)*}<>->x'
check_psl 'G({(g;y;r)*}<>->x)'
check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)'
check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)'
check_psl '{(#e + a):c*:(#e + b)}<>->d'
check_psl '{a;e;f:(g*);h}<>->d'
check_psl '{(a:b)* & (c*:d)}<>->e'
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment