alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/ltlvisit/forminf.cc (form_eventual_universal_visitor,

Browse source 
inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
as ...
(eventual_universal_visitor, inf_right_recurse_visitor,
inf_left_recurse_visitor): ... these.
(is_GF, is_FG): Move ...
* src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they
are only used here.
(basic_reduce_form, basic_reduce_form_visitor): Rename as ...
(basic_reduce, basic_reduce_visitor): ... these.
* src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ...
(reduce_visitor): ... this.
* src/ltltest/inf.cc: Adjust calls.
* src/sanity/style.test: Improve missing-space after coma detection.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-30 12:33:35 +00:00
parent c0b59d0795
commit 121a55c48f
7 changed files with 200 additions and 175 deletions
Download patch file Download diff file Expand all files Collapse all files

17
ChangeLog
View file

@ -1,3 +1,20 @@
2004-05-30 Alexandre Duret-Lutz <adl@gnu.org>
* src/ltlvisit/forminf.cc (form_eventual_universal_visitor,
inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
as ...
(eventual_universal_visitor, inf_right_recurse_visitor,
inf_left_recurse_visitor): ... these.
(is_GF, is_FG): Move ...
* src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they
are only used here.
(basic_reduce_form, basic_reduce_form_visitor): Rename as ...
(basic_reduce, basic_reduce_visitor): ... these.
* src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ...
(reduce_visitor): ... this.
* src/ltltest/inf.cc: Adjust calls.
* src/sanity/style.test: Improve missing-space after coma detection.
2004-05-26 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-26 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)): * src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)):

10
src/ltltest/inf.cc
View file

@ -68,7 +68,7 @@ main(int argc, char** argv)
{ {
case 0: case 0:
std::cout << "Test f1 < f2" << std::endl; std::cout << "Test f1 < f2" << std::endl;
if (spot::ltl::inf_form(f1, f2)) if (spot::ltl::syntactic_implication(f1, f2))
{ {
std::cout << f1s << " < " << f2s << std::endl; std::cout << f1s << " < " << f2s << std::endl;
exit_return = 1; exit_return = 1;
@ -77,7 +77,7 @@ main(int argc, char** argv)
case 1: case 1:
std::cout << "Test !f1 < f2" << std::endl; std::cout << "Test !f1 < f2" << std::endl;
if (spot::ltl::infneg_form(f1, f2, 0)) if (spot::ltl::syntactic_implication_neg(f1, f2, false))
{ {
std::cout << "!(" << f1s << ") < " << f2s << std::endl; std::cout << "!(" << f1s << ") < " << f2s << std::endl;
exit_return = 1; exit_return = 1;
@ -86,7 +86,7 @@ main(int argc, char** argv)
case 2: case 2:
std::cout << "Test f1 < !f2" << std::endl; std::cout << "Test f1 < !f2" << std::endl;
if (spot::ltl::infneg_form(f1, f2, 1)) if (spot::ltl::syntactic_implication_neg(f1, f2, true))
{ {
std::cout << f1s << " < !(" << f2s << ")" << std::endl; std::cout << f1s << " < !(" << f2s << ")" << std::endl;
exit_return = 1; exit_return = 1;
@ -96,8 +96,8 @@ main(int argc, char** argv)
break; break;
} }
spot::ltl::dump(std::cout, f1); std::cout << std::endl; spot::ltl::dump(std::cout, f1) << std::endl;
spot::ltl::dump(std::cout, f2); std::cout << std::endl; spot::ltl::dump(std::cout, f2) << std::endl;
spot::ltl::destroy(f1); spot::ltl::destroy(f1);
spot::ltl::destroy(f2); spot::ltl::destroy(f2);

160
src/ltlvisit/basereduc.cc
View file

@ -29,13 +29,42 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
class basic_reduce_form_visitor : public visitor
bool
is_GF(const formula* f)
{
const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::G)
{
const unop* opchild = dynamic_cast<const unop*>(op->child());
if (opchild && opchild->op() == unop::F)
return true;
}
return false;
}
bool
is_FG(const formula* f)
{
const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::F)
{
const unop* opchild = dynamic_cast<const unop*>(op->child());
if (opchild && opchild->op() == unop::G)
return true;
}
return false;
}
formula* basic_reduce(const formula* f);
class basic_reduce_visitor : public visitor
{ {
public: public:
basic_reduce_form_visitor(){} basic_reduce_visitor(){}
virtual ~basic_reduce_form_visitor(){} virtual ~basic_reduce_visitor(){}
formula* formula*
result() const result() const
@ -60,7 +89,7 @@ namespace spot
visit(unop* uo) visit(unop* uo)
{ {
formula* f = uo->child(); formula* f = uo->child();
result_ = basic_reduce_form(f); result_ = basic_reduce(f);
multop* mo = NULL; multop* mo = NULL;
unop* u = NULL; unop* u = NULL;
binop* bo = NULL; binop* bo = NULL;
@ -90,10 +119,9 @@ namespace spot
if (is_GF(mo->nth(0))) if (is_GF(mo->nth(0)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back res->push_back(unop::instance(unop::F,
(unop::instance(unop::F, basic_reduce(mo->nth(1))));
basic_reduce_form(mo->nth(1)))); res->push_back(basic_reduce(mo->nth(0)));
res->push_back(basic_reduce_form(mo->nth(0)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
destroy(mo); destroy(mo);
return; return;
@ -101,10 +129,9 @@ namespace spot
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back res->push_back(unop::instance(unop::F,
(unop::instance(unop::F, basic_reduce(mo->nth(0))));
basic_reduce_form(mo->nth(0)))); res->push_back(basic_reduce(mo->nth(1)));
res->push_back(basic_reduce_form(mo->nth(1)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
destroy(mo); destroy(mo);
return; return;
@ -127,7 +154,7 @@ namespace spot
result_ = result_ =
unop::instance(unop::X, unop::instance(unop::X,
unop::instance(unop::F, unop::instance(unop::F,
basic_reduce_form(u->child()))); basic_reduce(u->child())));
destroy(u); destroy(u);
return; return;
} }
@ -142,10 +169,9 @@ namespace spot
if (is_GF(mo->nth(0))) if (is_GF(mo->nth(0)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back res->push_back(unop::instance(unop::F,
(unop::instance(unop::F, basic_reduce(mo->nth(1))));
basic_reduce_form(mo->nth(1)))); res->push_back(basic_reduce(mo->nth(0)));
res->push_back(basic_reduce_form(mo->nth(0)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
destroy(mo); destroy(mo);
return; return;
@ -153,10 +179,9 @@ namespace spot
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back res->push_back(unop::instance(unop::F,
(unop::instance(unop::F, basic_reduce(mo->nth(0))));
basic_reduce_form(mo->nth(0)))); res->push_back(basic_reduce(mo->nth(1)));
res->push_back(basic_reduce_form(mo->nth(1)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
destroy(mo); destroy(mo);
return; return;
@ -178,7 +203,7 @@ namespace spot
if (bo && bo->op() == binop::R) if (bo && bo->op() == binop::R)
{ {
result_ = unop::instance(unop::G, result_ = unop::instance(unop::G,
basic_reduce_form(bo->second())); basic_reduce(bo->second()));
destroy(bo); destroy(bo);
return; return;
} }
@ -190,7 +215,7 @@ namespace spot
result_ = result_ =
unop::instance(unop::X, unop::instance(unop::X,
unop::instance(unop::G, unop::instance(unop::G,
basic_reduce_form(u->child()))); basic_reduce(u->child())));
destroy(u); destroy(u);
return; return;
} }
@ -205,10 +230,9 @@ namespace spot
if (is_GF(mo->nth(0))) if (is_GF(mo->nth(0)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back res->push_back(unop::instance(unop::F,
(unop::instance(unop::F, basic_reduce(mo->nth(1))));
basic_reduce_form(mo->nth(1)))); res->push_back(basic_reduce(mo->nth(0)));
res->push_back(basic_reduce_form(mo->nth(0)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
destroy(mo); destroy(mo);
return; return;
@ -216,10 +240,9 @@ namespace spot
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back res->push_back(unop::instance(unop::F,
(unop::instance(unop::F, basic_reduce(mo->nth(0))));
basic_reduce_form(mo->nth(0)))); res->push_back(basic_reduce(mo->nth(1)));
res->push_back(basic_reduce_form(mo->nth(1)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
destroy(mo); destroy(mo);
return; return;
@ -245,21 +268,21 @@ namespace spot
{ {
case binop::Xor: case binop::Xor:
result_ = binop::instance(binop::Xor, result_ = binop::instance(binop::Xor,
basic_reduce_form(f1), basic_reduce(f1),
basic_reduce_form(f2)); basic_reduce(f2));
return; return;
case binop::Equiv: case binop::Equiv:
result_ = binop::instance(binop::Equiv, result_ = binop::instance(binop::Equiv,
basic_reduce_form(f1), basic_reduce(f1),
basic_reduce_form(f2)); basic_reduce(f2));
return; return;
case binop::Implies: case binop::Implies:
result_ = binop::instance(binop::Implies, result_ = binop::instance(binop::Implies,
basic_reduce_form(f1), basic_reduce(f1),
basic_reduce_form(f2)); basic_reduce(f2));
return; return;
case binop::U: case binop::U:
f2 = basic_reduce_form(f2); f2 = basic_reduce(f2);
// a U false = false // a U false = false
// a U true = true // a U true = true
@ -269,7 +292,7 @@ namespace spot
return; return;
} }
f1 = basic_reduce_form(f1); f1 = basic_reduce(f1);
// X(a) U X(b) = X(a U b) // X(a) U X(b) = X(a U b)
fu1 = dynamic_cast<unop*>(f1); fu1 = dynamic_cast<unop*>(f1);
@ -279,9 +302,9 @@ namespace spot
(fu2->op() == unop::X)) (fu2->op() == unop::X))
{ {
ftmp = binop::instance(binop::U, ftmp = binop::instance(binop::U,
basic_reduce_form(fu1->child()), basic_reduce(fu1->child()),
basic_reduce_form(fu2->child())); basic_reduce(fu2->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); result_ = unop::instance(unop::X, basic_reduce(ftmp));
destroy(f1); destroy(f1);
destroy(f2); destroy(f2);
destroy(ftmp); destroy(ftmp);
@ -292,7 +315,7 @@ namespace spot
return; return;
case binop::R: case binop::R:
f2 = basic_reduce_form(f2); f2 = basic_reduce(f2);
// a R false = false // a R false = false
// a R true = true // a R true = true
@ -302,7 +325,7 @@ namespace spot
return; return;
} }
f1 = basic_reduce_form(f1); f1 = basic_reduce(f1);
// X(a) R X(b) = X(a R b) // X(a) R X(b) = X(a R b)
fu1 = dynamic_cast<unop*>(f1); fu1 = dynamic_cast<unop*>(f1);
@ -312,9 +335,9 @@ namespace spot
(fu2->op() == unop::X)) (fu2->op() == unop::X))
{ {
ftmp = binop::instance(bo->op(), ftmp = binop::instance(bo->op(),
basic_reduce_form(fu1->child()), basic_reduce(fu1->child()),
basic_reduce_form(fu2->child())); basic_reduce(fu2->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); result_ = unop::instance(unop::X, basic_reduce(ftmp));
destroy(f1); destroy(f1);
destroy(f2); destroy(f2);
destroy(ftmp); destroy(ftmp);
@ -349,7 +372,7 @@ namespace spot
formula* ftmp = NULL; formula* ftmp = NULL;
for (unsigned i = 0; i < mos; ++i) for (unsigned i = 0; i < mos; ++i)
res->push_back(basic_reduce_form(mo->nth(i))); res->push_back(basic_reduce(mo->nth(i)));
switch (op) switch (op)
@ -367,17 +390,17 @@ namespace spot
if (uo && uo->op() == unop::X) if (uo && uo->op() == unop::X)
{ {
// Xa & Xb = X(a & b) // Xa & Xb = X(a & b)
tmpX->push_back(basic_reduce_form(uo->child())); tmpX->push_back(basic_reduce(uo->child()));
} }
else if (is_FG(*i)) else if (is_FG(*i))
{ {
// FG(a) & FG(b) = FG(a & b) // FG(a) & FG(b) = FG(a & b)
unop* uo2 = dynamic_cast<unop*>(uo->child()); unop* uo2 = dynamic_cast<unop*>(uo->child());
tmpFG->push_back(basic_reduce_form(uo2->child())); tmpFG->push_back(basic_reduce(uo2->child()));
} }
else else
{ {
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce(*i));
} }
} }
else if (bo) else if (bo)
@ -396,7 +419,7 @@ namespace spot
&& ftmp == bo2->second()) && ftmp == bo2->second())
{ {
tmpUright tmpUright
->push_back(basic_reduce_form(bo2->first())); ->push_back(basic_reduce(bo2->first()));
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
@ -410,7 +433,7 @@ namespace spot
instance(multop:: instance(multop::
And, And,
tmpUright), tmpUright),
basic_reduce_form(ftmp))); basic_reduce(ftmp)));
} }
else if (bo->op() == binop::R) else if (bo->op() == binop::R)
{ {
@ -426,7 +449,7 @@ namespace spot
&& ftmp == bo2->first()) && ftmp == bo2->first())
{ {
tmpRright tmpRright
->push_back(basic_reduce_form(bo2->second())); ->push_back(basic_reduce(bo2->second()));
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
@ -436,19 +459,19 @@ namespace spot
} }
tmpR tmpR
->push_back(binop::instance(binop::R, ->push_back(binop::instance(binop::R,
basic_reduce_form(ftmp), basic_reduce(ftmp),
multop:: multop::
instance(multop::And, instance(multop::And,
tmpRright))); tmpRright)));
} }
else else
{ {
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce(*i));
} }
} }
else else
{ {
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce(*i));
} }
destroy(*i); destroy(*i);
} }
@ -471,17 +494,17 @@ namespace spot
if (uo && uo->op() == unop::X) if (uo && uo->op() == unop::X)
{ {
// Xa | Xb = X(a | b) // Xa | Xb = X(a | b)
tmpX->push_back(basic_reduce_form(uo->child())); tmpX->push_back(basic_reduce(uo->child()));
} }
else if (is_GF(*i)) else if (is_GF(*i))
{ {
// GF(a) | GF(b) = GF(a | b) // GF(a) | GF(b) = GF(a | b)
unop* uo2 = dynamic_cast<unop*>(uo->child()); unop* uo2 = dynamic_cast<unop*>(uo->child());
tmpGF->push_back(basic_reduce_form(uo2->child())); tmpGF->push_back(basic_reduce(uo2->child()));
} }
else else
{ {
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce(*i));
} }
} }
else if (bo) else if (bo)
@ -500,7 +523,7 @@ namespace spot
&& ftmp == bo2->first()) && ftmp == bo2->first())
{ {
tmpUright tmpUright
->push_back(basic_reduce_form(bo2->second())); ->push_back(basic_reduce(bo2->second()));
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
@ -509,7 +532,7 @@ namespace spot
} }
} }
tmpU->push_back(binop::instance(binop::U, tmpU->push_back(binop::instance(binop::U,
basic_reduce_form(ftmp), basic_reduce(ftmp),
multop:: multop::
instance(multop::Or, instance(multop::Or,
tmpUright))); tmpUright)));
@ -528,7 +551,7 @@ namespace spot
&& ftmp == bo2->second()) && ftmp == bo2->second())
{ {
tmpRright tmpRright
->push_back(basic_reduce_form(bo->first())); ->push_back(basic_reduce(bo->first()));
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
@ -541,16 +564,16 @@ namespace spot
multop:: multop::
instance(multop::Or, instance(multop::Or,
tmpRright), tmpRright),
basic_reduce_form(ftmp))); basic_reduce(ftmp)));
} }
else else
{ {
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce(*i));
} }
} }
else else
{ {
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce(*i));
} }
destroy(*i); destroy(*i);
} }
@ -610,9 +633,10 @@ namespace spot
formula* result_; formula* result_;
}; };
formula* basic_reduce_form(const formula* f) formula*
basic_reduce(const formula* f)
{ {
basic_reduce_form_visitor v; basic_reduce_visitor v;
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
return v.result(); return v.result();
} }

123
src/ltlvisit/forminf.cc
View file

@ -32,43 +32,17 @@ namespace spot
namespace ltl namespace ltl
{ {
bool class eventual_universal_visitor : public const_visitor
is_GF(const formula* f)
{
const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::G)
{
const unop* opchild = dynamic_cast<const unop*>(op->child());
if (opchild && opchild->op() == unop::F)
return true;
}
return false;
}
bool
is_FG(const formula* f)
{
const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::F)
{
const unop* opchild = dynamic_cast<const unop*>(op->child());
if (opchild && opchild->op() == unop::G)
return true;
}
return false;
}
class form_eventual_universal_visitor : public const_visitor
{ {
public: public:
form_eventual_universal_visitor() eventual_universal_visitor()
: eventual(false), universal(false) : eventual(false), universal(false)
{ {
} }
virtual virtual
~form_eventual_universal_visitor() ~eventual_universal_visitor()
{ {
} }
@ -163,7 +137,7 @@ namespace spot
bool bool
recurse_ev(const formula* f) recurse_ev(const formula* f)
{ {
form_eventual_universal_visitor v; eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
return v.is_eventual(); return v.is_eventual();
} }
@ -171,7 +145,7 @@ namespace spot
bool bool
recurse_un(const formula* f) recurse_un(const formula* f)
{ {
form_eventual_universal_visitor v; eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
return v.is_universal(); return v.is_universal();
} }
@ -182,33 +156,36 @@ namespace spot
}; };
bool is_eventual(const formula* f) bool
is_eventual(const formula* f)
{ {
form_eventual_universal_visitor v; eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
return v.is_eventual(); return v.is_eventual();
} }
bool is_universal(const formula* f) bool
is_universal(const formula* f)
{ {
form_eventual_universal_visitor v; eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
return v.is_universal(); return v.is_universal();
} }
///////////////////////////////////////////////////////////////////////// /////////////////////////////////////////////////////////////////////////
class inf_form_right_recurse_visitor : public const_visitor
class inf_right_recurse_visitor : public const_visitor
{ {
public: public:
inf_form_right_recurse_visitor(const formula *f) inf_right_recurse_visitor(const formula *f)
: result_(false), f(f) : result_(false), f(f)
{ {
} }
virtual virtual
~inf_form_right_recurse_visitor() ~inf_right_recurse_visitor()
{ {
} }
@ -254,17 +231,17 @@ namespace spot
{ {
const unop* op = dynamic_cast<const unop*>(f); const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::X) if (op && op->op() == unop::X)
result_ = inf_form(op->child(), f1); result_ = syntactic_implication(op->child(), f1);
} }
return; return;
case unop::F: case unop::F:
/* F(a) = true U a */ /* F(a) = true U a */
result_ = inf_form(f, f1); result_ = syntactic_implication(f, f1);
return; return;
case unop::G: case unop::G:
/* G(a) = false R a */ /* G(a) = false R a */
tmp = constant::false_instance(); tmp = constant::false_instance();
if (inf_form(f, tmp)) if (syntactic_implication(f, tmp))
result_ = true; result_ = true;
destroy(tmp); destroy(tmp);
return; return;
@ -285,11 +262,12 @@ namespace spot
case binop::Implies: case binop::Implies:
return; return;
case binop::U: case binop::U:
if (inf_form(f, f2)) if (syntactic_implication(f, f2))
result_ = true; result_ = true;
return; return;
case binop::R: case binop::R:
if (inf_form(f, f1) && inf_form(f, f2)) if (syntactic_implication(f, f1)
&& syntactic_implication(f, f2))
result_ = true; result_ = true;
return; return;
} }
@ -306,13 +284,13 @@ namespace spot
{ {
case multop::And: case multop::And:
for (unsigned i = 0; i < mos; ++i) for (unsigned i = 0; i < mos; ++i)
if (!inf_form(f, mo->nth(i))) if (!syntactic_implication(f, mo->nth(i)))
return; return;
result_ = true; result_ = true;
break; break;
case multop::Or: case multop::Or:
for (unsigned i = 0; i < mos && !result_; ++i) for (unsigned i = 0; i < mos && !result_; ++i)
if (inf_form(f, mo->nth(i))) if (syntactic_implication(f, mo->nth(i)))
result_ = true; result_ = true;
break; break;
} }
@ -323,7 +301,7 @@ namespace spot
{ {
if (f1 == f2) if (f1 == f2)
return true; return true;
inf_form_right_recurse_visitor v(f2); inf_right_recurse_visitor v(f2);
const_cast<formula*>(f1)->accept(v); const_cast<formula*>(f1)->accept(v);
return v.result(); return v.result();
} }
@ -335,17 +313,17 @@ namespace spot
///////////////////////////////////////////////////////////////////////// /////////////////////////////////////////////////////////////////////////
class inf_form_left_recurse_visitor : public const_visitor class inf_left_recurse_visitor : public const_visitor
{ {
public: public:
inf_form_left_recurse_visitor(const formula *f) inf_left_recurse_visitor(const formula *f)
: result_(false), f(f) : result_(false), f(f)
{ {
} }
virtual virtual
~inf_form_left_recurse_visitor() ~inf_left_recurse_visitor()
{ {
} }
@ -355,8 +333,8 @@ namespace spot
const binop* fb = dynamic_cast<const binop*>(f); const binop* fb = dynamic_cast<const binop*>(f);
const binop* f2b = dynamic_cast<const binop*>(f2); const binop* f2b = dynamic_cast<const binop*>(f2);
if (fb && f2b && fb->op() == f2b->op() if (fb && f2b && fb->op() == f2b->op()
&& inf_form(f2b->first(), fb->first()) && syntactic_implication(f2b->first(), fb->first())
&& inf_form(f2b->second(), fb->second())) && syntactic_implication(f2b->second(), fb->second()))
return true; return true;
return false; return false;
} }
@ -370,7 +348,7 @@ namespace spot
void void
visit(const atomic_prop* ap) visit(const atomic_prop* ap)
{ {
inf_form_right_recurse_visitor v(ap); inf_right_recurse_visitor v(ap);
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
result_ = v.result(); result_ = v.result();
} }
@ -378,7 +356,7 @@ namespace spot
void void
visit(const constant* c) visit(const constant* c)
{ {
inf_form_right_recurse_visitor v(c); inf_right_recurse_visitor v(c);
switch (c->val()) switch (c->val())
{ {
case constant::True: case constant::True:
@ -397,7 +375,7 @@ namespace spot
visit(const unop* uo) visit(const unop* uo)
{ {
const formula* f1 = uo->child(); const formula* f1 = uo->child();
inf_form_right_recurse_visitor v(uo); inf_right_recurse_visitor v(uo);
switch (uo->op()) switch (uo->op())
{ {
case unop::Not: case unop::Not:
@ -408,7 +386,7 @@ namespace spot
{ {
const unop* op = dynamic_cast<const unop*>(f); const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::X) if (op && op->op() == unop::X)
result_ = inf_form(f1, op->child()); result_ = syntactic_implication(f1, op->child());
} }
return; return;
case unop::F: case unop::F:
@ -423,7 +401,7 @@ namespace spot
destroy(tmp); destroy(tmp);
return; return;
} }
if (inf_form(tmp, f)) if (syntactic_implication(tmp, f))
result_ = true; result_ = true;
destroy(tmp); destroy(tmp);
return; return;
@ -440,7 +418,7 @@ namespace spot
destroy(tmp); destroy(tmp);
return; return;
} }
if (inf_form(f1, f)) if (syntactic_implication(f1, f))
result_ = true; result_ = true;
destroy(tmp); destroy(tmp);
return; return;
@ -468,11 +446,12 @@ namespace spot
case binop::Implies: case binop::Implies:
return; return;
case binop::U: case binop::U:
if (inf_form(f1, f) && inf_form(f2, f)) if (syntactic_implication(f1, f)
&& syntactic_implication(f2, f))
result_ = true; result_ = true;
return; return;
case binop::R: case binop::R:
if (inf_form(f2, f)) if (syntactic_implication(f2, f))
result_ = true; result_ = true;
return; return;
} }
@ -489,12 +468,12 @@ namespace spot
{ {
case multop::And: case multop::And:
for (unsigned i = 0; (i < mos) && !result_; ++i) for (unsigned i = 0; (i < mos) && !result_; ++i)
if (inf_form(mo->nth(i), f)) if (syntactic_implication(mo->nth(i), f))
result_ = true; result_ = true;
break; break;
case multop::Or: case multop::Or:
for (unsigned i = 0; i < mos; ++i) for (unsigned i = 0; i < mos; ++i)
if (!inf_form(mo->nth(i), f)) if (!syntactic_implication(mo->nth(i), f))
return; return;
result_ = true; result_ = true;
break; break;
@ -506,15 +485,15 @@ namespace spot
const formula* f; const formula* f;
}; };
// This is called by syntactic_implication() after the
// formulae have been normalized.
bool bool
inf_form(const formula* f1, const formula* f2) syntactic_implication(const formula* f1, const formula* f2)
{ {
/* f1 and f2 are unabbreviated */
if (f1 == f2) if (f1 == f2)
return true; return true;
inf_form_left_recurse_visitor v1(f2); inf_left_recurse_visitor v1(f2);
inf_form_right_recurse_visitor v2(f1); inf_right_recurse_visitor v2(f1);
if (f2 == constant::true_instance() if (f2 == constant::true_instance()
|| f1 == constant::false_instance()) || f1 == constant::false_instance())
@ -532,13 +511,13 @@ namespace spot
} }
bool bool
infneg_form(const formula* f1, const formula* f2, int n) syntactic_implication_neg(const formula* f1, const formula* f2, bool right)
{ {
const formula* ftmp1; const formula* ftmp1;
const formula* ftmp2; const formula* ftmp2;
const formula* ftmp3 = unop::instance(unop::Not, const formula* ftmp3 = unop::instance(unop::Not,
(!n) ? clone(f1) : clone(f2)); right ? clone(f2) : clone(f1));
const formula* ftmp4 = negative_normal_form((!n) ? f2 : f1); const formula* ftmp4 = negative_normal_form(right ? f1 : f2);
const formula* ftmp5; const formula* ftmp5;
const formula* ftmp6; const formula* ftmp6;
bool result; bool result;
@ -549,10 +528,10 @@ namespace spot
ftmp5 = unabbreviate_logic(ftmp4); ftmp5 = unabbreviate_logic(ftmp4);
ftmp6 = negative_normal_form(ftmp5); ftmp6 = negative_normal_form(ftmp5);
if (n == 0) if (right)
result = inf_form(ftmp1, ftmp6); result = syntactic_implication(ftmp6, ftmp1);
else else
result = inf_form(ftmp6, ftmp1); result = syntactic_implication(ftmp1, ftmp6);
destroy(ftmp1); destroy(ftmp1);
destroy(ftmp2); destroy(ftmp2);

43
src/ltlvisit/reducform.cc
View file

@ -32,16 +32,16 @@ namespace spot
namespace ltl namespace ltl
{ {
class reduce_form_visitor : public visitor class reduce_visitor : public visitor
{ {
public: public:
reduce_form_visitor(int opt) reduce_visitor(int opt)
: opt_(opt) : opt_(opt)
{ {
} }
virtual ~reduce_form_visitor() virtual ~reduce_visitor()
{ {
} }
@ -116,10 +116,11 @@ namespace spot
if (opt_ & Reduce_Syntactic_Implications) if (opt_ & Reduce_Syntactic_Implications)
{ {
bool inf = inf_form(f1, f2); // FIXME: These should be done only when needed.
bool infinv = inf_form(f2, f1); bool inf = syntactic_implication(f1, f2);
bool infnegleft = infneg_form(f2, f1, 0); bool infinv = syntactic_implication(f2, f1);
bool infnegright = infneg_form(f2, f1, 1); bool infnegleft = syntactic_implication_neg(f2, f1, false);
bool infnegright = syntactic_implication_neg(f2, f1, true);
switch (bo->op()) switch (bo->op())
{ {
@ -146,7 +147,8 @@ namespace spot
/* a < b => a U (b U c) = (b U c) */ /* a < b => a U (b U c) = (b U c) */
{ {
binop* bo = dynamic_cast<binop*>(f2); binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::U && inf_form(f1, bo->first())) if (bo && bo->op() == binop::U
&& syntactic_implication(f1, bo->first()))
{ {
result_ = f2; result_ = f2;
destroy(f1); destroy(f1);
@ -173,7 +175,8 @@ namespace spot
/* b < a => a R (b R c) = b R c */ /* b < a => a R (b R c) = b R c */
{ {
binop* bo = dynamic_cast<binop*>(f2); binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::R && inf_form(bo->first(), f1)) if (bo && bo->op() == binop::R
&& syntactic_implication(bo->first(), f1))
{ {
result_ = f2; result_ = f2;
destroy(f1); destroy(f1);
@ -215,7 +218,7 @@ namespace spot
{ {
f2 = *index; f2 = *index;
/* a < b => a + b = b */ /* a < b => a + b = b */
if (inf_form(f1, f2)) // f1 < f2 if (syntactic_implication(f1, f2)) // f1 < f2
{ {
f1 = f2; f1 = f2;
destroy(*indextmp); destroy(*indextmp);
@ -223,7 +226,7 @@ namespace spot
indextmp = index; indextmp = index;
index--; index--;
} }
else if (inf_form(f2, f1)) // f2 < f1 else if (syntactic_implication(f2, f1)) // f2 < f1
{ {
destroy(*index); destroy(*index);
res->erase(index); res->erase(index);
@ -243,13 +246,13 @@ namespace spot
{ {
f2 = *index; f2 = *index;
/* a < b => a & b = a */ /* a < b => a & b = a */
if (inf_form(f1, f2)) // f1 < f2 if (syntactic_implication(f1, f2)) // f1 < f2
{ {
destroy(*index); destroy(*index);
res->erase(index); res->erase(index);
index--; index--;
} }
else if (inf_form(f2, f1)) // f2 < f1 else if (syntactic_implication(f2, f1)) // f2 < f1
{ {
f1 = f2; f1 = f2;
destroy(*indextmp); destroy(*indextmp);
@ -266,8 +269,8 @@ namespace spot
for (index = res->begin(); index != res->end(); index++) for (index = res->begin(); index != res->end(); index++)
for (indextmp = res->begin(); indextmp != res->end(); indextmp++) for (indextmp = res->begin(); indextmp != res->end(); indextmp++)
if (index != indextmp if (index != indextmp
&& infneg_form(*index,*indextmp, && syntactic_implication_neg(*index, *indextmp,
(mo->op() == multop::Or) ? 0 : 1)) mo->op() != multop::Or))
{ {
for (multop::vec::iterator j = res->begin(); for (multop::vec::iterator j = res->begin();
j != res->end(); j++) j != res->end(); j++)
@ -310,27 +313,27 @@ namespace spot
if (opt & Reduce_Basics) if (opt & Reduce_Basics)
{ {
f1 = basic_reduce_form(f2); f1 = basic_reduce(f2);
destroy(f2); destroy(f2);
f2 = f1; f2 = f1;
} }
if (opt & (Reduce_Syntactic_Implications if (opt & (Reduce_Syntactic_Implications
| Reduce_Eventuality_And_Universality)) | Reduce_Eventuality_And_Universality))
{ {
reduce_form_visitor v(opt); reduce_visitor v(opt);
f2->accept(v); f2->accept(v);
f1 = v.result(); f1 = v.result();
destroy(f2); destroy(f2);
f2 = f1; f2 = f1;
// Run basic_reduce_form again. // Run basic_reduce again.
// //
// Consider `F b & g' were g is an eventual formula rewritten // Consider `F b & g' were g is an eventual formula rewritten
// as `g = F c' Then basic_reduce_form with rewrite it // as `g = F c' Then basic_reduce with rewrite it
// as F(b & c). // as F(b & c).
if (opt & Reduce_Basics) if (opt & Reduce_Basics)
{ {
f1 = basic_reduce_form(f2); f1 = basic_reduce(f2);
destroy(f2); destroy(f2);
f2 = f1; f2 = f1;
} }

20
src/ltlvisit/reducform.hh
View file

@ -53,16 +53,18 @@ namespace spot
/// \return the reduced formula /// \return the reduced formula
formula* reduce(const formula* f, int opt = Reduce_All); formula* reduce(const formula* f, int opt = Reduce_All);
/// Implement basic rewriting. /// Basic rewritings.
formula* basic_reduce_form(const formula* f); formula* basic_reduce(const formula* f);
/// Detect easy case of implies. /// \brief Syntactic implication.
/// True if f1 < f2, false otherwise. bool syntactic_implication(const formula* f1, const formula* f2);
bool inf_form(const formula* f1, const formula* f2);
/// Detect easy case of implies. /// \brief Syntactic implication.
/// If n = 0, true if !f1 < f2, false otherwise. ///
/// If n = 1, true if f1 < !f2, false otherwise. /// If right==false, true if !f1 < f2, false otherwise.
bool infneg_form(const formula* f1, const formula* f2, int n); /// If right==true, true if f1 < !f2, false otherwise.
bool syntactic_implication_neg(const formula* f1, const formula* f2,
bool right);
/// \brief Check whether a formula is eventual. /// \brief Check whether a formula is eventual.
/// ///

2
src/sanity/style.test
View file

@ -80,7 +80,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep '! ' $tmp && grep '! ' $tmp &&
diag 'No space after unary operators (!).' diag 'No space after unary operators (!).'
grep ',[(a-zA-Z+=_!]' $tmp && grep ',[^ "%]' $tmp &&
diag 'Space after coma.' diag 'Space after coma.'
grep '[^ ]&&[^ ]' $tmp && grep '[^ ]&&[^ ]' $tmp &&