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

* src/ltlvisit/forminf.cc: Fix style to please sanity checks.

Browse source 
Also avoid node_type_form_visitor where a dynamic_cast is done.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-17 10:28:55 +00:00
parent 1e2669d640
commit d22c647322
2 changed files with 135 additions and 141 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2004-05-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/forminf.cc: Fix style to please sanity checks.
Also avoid node_type_form_visitor where a dynamic_cast is done.
2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
* wrap/python/buddy.i: Preliminary bindings for FDD and BVEC. * wrap/python/buddy.i: Preliminary bindings for FDD and BVEC.

271
src/ltlvisit/forminf.cc
View file

@ -35,22 +35,26 @@ namespace spot
bool bool
is_GF(const formula* f) is_GF(const formula* f)
{ {
if (node_type(f) == node_type_form_visitor::Unop) const unop* op = dynamic_cast<const unop*>(f);
if (dynamic_cast<const unop*>(f)->op() == unop::G) if (op && op->op() == unop::G)
if (node_type(((const unop*)f)->child()) == node_type_form_visitor::Unop) {
if (dynamic_cast<const unop*>(dynamic_cast<const unop*>(f)->child())->op() == unop::F) const unop* opchild = dynamic_cast<const unop*>(op->child());
return true; if (opchild && opchild->op() == unop::F)
return true;
}
return false; return false;
} }
bool bool
is_FG(const formula* f) is_FG(const formula* f)
{ {
if (node_type(f) == node_type_form_visitor::Unop) const unop* op = dynamic_cast<const unop*>(f);
if (dynamic_cast<const unop*>(f)->op() == unop::F) if (op && op->op() == unop::F)
if (node_type(((const unop*)f)->child()) == node_type_form_visitor::Unop) {
if (dynamic_cast<const unop*>(dynamic_cast<const unop*>(f)->child())->op() == unop::G) const unop* opchild = dynamic_cast<const unop*>(op->child());
return true; if (opchild && opchild->op() == unop::G)
return true;
}
return false; return false;
} }
@ -60,36 +64,37 @@ namespace spot
node_type_form_visitor::result() const { return result_;} node_type_form_visitor::result() const { return result_;}
void void
node_type_form_visitor::visit(const atomic_prop* ap){ node_type_form_visitor::visit(const atomic_prop*)
if (ap == NULL); {
result_ = node_type_form_visitor::Atom; result_ = node_type_form_visitor::Atom;
} }
void void
node_type_form_visitor::visit(const constant* c){ node_type_form_visitor::visit(const constant*)
if (c == NULL); {
result_ = node_type_form_visitor::Const; result_ = node_type_form_visitor::Const;
} }
void void
node_type_form_visitor::visit(const unop* uo){ node_type_form_visitor::visit(const unop*)
if (uo == NULL); {
result_ = node_type_form_visitor::Unop; result_ = node_type_form_visitor::Unop;
} }
void void
node_type_form_visitor::visit(const binop* bo){ node_type_form_visitor::visit(const binop*)
if (bo == NULL); {
result_ = node_type_form_visitor::Binop; result_ = node_type_form_visitor::Binop;
} }
void void
node_type_form_visitor::visit(const multop* mo){ node_type_form_visitor::visit(const multop*)
if (mo == NULL); {
result_ = node_type_form_visitor::Multop; result_ = node_type_form_visitor::Multop;
} }
node_type_form_visitor::type node_type(const formula* f) node_type_form_visitor::type
node_type(const formula* f)
{ {
node_type_form_visitor v; node_type_form_visitor v;
assert(f != NULL); assert(f != NULL);
@ -102,12 +107,12 @@ namespace spot
public: public:
form_eventual_universal_visitor() form_eventual_universal_visitor()
: eventual(false), universal(false)
{ {
eventual = false;
universal = false;
} }
virtual ~form_eventual_universal_visitor() virtual
~form_eventual_universal_visitor()
{ {
} }
@ -124,15 +129,13 @@ namespace spot
} }
void void
visit(const atomic_prop* ap) visit(const atomic_prop*)
{ {
if (ap);
} }
void void
visit(const constant* c) visit(const constant*)
{ {
if (c->val());
} }
void void
@ -168,14 +171,12 @@ namespace spot
case binop::Implies: case binop::Implies:
return; return;
case binop::U: case binop::U:
if (node_type(f1) == node_type_form_visitor::Const) if (f1 == constant::true_instance())
if (dynamic_cast<const constant*>(f1)->val() == constant::True) eventual = true;
eventual = true;
return; return;
case binop::R: case binop::R:
if (node_type(f1) == node_type_form_visitor::Const) if (f1 == constant::false_instance())
if (dynamic_cast<const constant*>(f1)->val() == constant::False) universal = true;
universal = true;
return; return;
} }
/* Unreachable code. */ /* Unreachable code. */
@ -185,23 +186,22 @@ namespace spot
void void
visit(const multop* mo) visit(const multop* mo)
{ {
if (mo == NULL);
unsigned mos = mo->size(); unsigned mos = mo->size();
eventual = true; eventual = true;
universal = true; universal = true;
for (unsigned i = 0; i < mos; ++i){ for (unsigned i = 0; i < mos; ++i)
if (!(recurse_ev(mo->nth(i)))){ if (!recurse_ev(mo->nth(i)))
eventual = false; {
break; eventual = false;
} break;
} }
for (unsigned i = 0; i < mos; ++i){ for (unsigned i = 0; i < mos; ++i)
if (!(recurse_un(mo->nth(i)))){ if (!recurse_un(mo->nth(i)))
universal = false; {
break; universal = false;
} break;
} }
} }
bool bool
@ -220,7 +220,7 @@ namespace spot
return v.is_universal(); return v.is_universal();
} }
protected: protected:
bool eventual; bool eventual;
bool universal; bool universal;
}; };
@ -247,12 +247,12 @@ namespace spot
public: public:
inf_form_right_recurse_visitor(const formula *f) inf_form_right_recurse_visitor(const formula *f)
: result_(false), f(f)
{ {
this->f = f;
result_ = false;
} }
virtual ~inf_form_right_recurse_visitor() virtual
~inf_form_right_recurse_visitor()
{ {
} }
@ -295,19 +295,20 @@ namespace spot
result_ = true; result_ = true;
return; return;
case unop::X: case unop::X:
if (node_type(f) == node_type_form_visitor::Unop) {
if (dynamic_cast<const unop*>(f)->op() == unop::X) { const unop* op = dynamic_cast<const unop*>(f);
result_ = inf_form(dynamic_cast<const unop*>(f)->child(),f1); if (op && op->op() == unop::X)
} result_ = inf_form(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_ = inf_form(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 (inf_form(f, tmp))
result_ = true; result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
@ -328,11 +329,11 @@ namespace spot
case binop::Implies: case binop::Implies:
return; return;
case binop::U: case binop::U:
if ((inf_form(f,f2))) if (inf_form(f, f2))
result_ = true; result_ = true;
return; return;
case binop::R: case binop::R:
if ((inf_form(f,f1)) && (inf_form(f,f2))) if (inf_form(f, f1) && inf_form(f, f2))
result_ = true; result_ = true;
return; return;
} }
@ -343,20 +344,19 @@ namespace spot
void void
visit(const multop* mo) visit(const multop* mo)
{ {
if (mo == NULL);
multop::type op = mo->op(); multop::type op = mo->op();
unsigned mos = mo->size(); unsigned mos = mo->size();
switch (op) switch (op)
{ {
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 (!inf_form(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 (inf_form(f, mo->nth(i)))
result_ = true; result_ = true;
break; break;
} }
@ -365,7 +365,8 @@ namespace spot
bool bool
recurse(const formula* f1, const formula* f2) recurse(const formula* f1, const formula* f2)
{ {
if (f1 == f2) return true; if (f1 == f2)
return true;
inf_form_right_recurse_visitor v(f2); inf_form_right_recurse_visitor v(f2);
const_cast<formula*>(f1)->accept(v); const_cast<formula*>(f1)->accept(v);
return v.result(); return v.result();
@ -383,33 +384,24 @@ namespace spot
public: public:
inf_form_left_recurse_visitor(const formula *f) inf_form_left_recurse_visitor(const formula *f)
{ : result_(false), f(f)
this->f = f;
result_ = false;
}
virtual ~inf_form_left_recurse_visitor()
{ {
} }
bool special_case(const formula* f2) virtual
~inf_form_left_recurse_visitor()
{ {
if ((node_type(f) == node_type_form_visitor::Binop)
&& (node_type(f2) == node_type_form_visitor::Binop))
if (dynamic_cast<const binop*>(f)->op() == dynamic_cast<const binop*>(f2)->op())
if (inf_form(dynamic_cast<const binop*>(f2)->first(),dynamic_cast<const binop*>(f)->first())
&& inf_form(dynamic_cast<const binop*>(f2)->second(),dynamic_cast<const binop*>(f)->second()))
return true;
return false;
} }
bool nodeX() bool
special_case(const formula* f2)
{ {
/* const binop* fb = dynamic_cast<const binop*>(f);
if (node_type(f) == node_type_form_visitor::Unop) const binop* f2b = dynamic_cast<const binop*>(f2);
if (dynamic_cast<const unop*>(f)->op() == unop::X) if (fb && f2b && fb->op() == f2b->op()
&& inf_form(f2b->first(), fb->first())
&& inf_form(f2b->second(), fb->second()))
return true; return true;
*/
return false; return false;
} }
@ -422,7 +414,6 @@ namespace spot
void void
visit(const atomic_prop* ap) visit(const atomic_prop* ap)
{ {
if (this->nodeX()) return;
inf_form_right_recurse_visitor v(ap); inf_form_right_recurse_visitor v(ap);
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
result_ = v.result(); result_ = v.result();
@ -431,7 +422,6 @@ namespace spot
void void
visit(const constant* c) visit(const constant* c)
{ {
if (this->nodeX()) return;
inf_form_right_recurse_visitor v(c); inf_form_right_recurse_visitor v(c);
switch (c->val()) switch (c->val())
{ {
@ -451,7 +441,6 @@ namespace spot
visit(const unop* uo) visit(const unop* uo)
{ {
const formula* f1 = uo->child(); const formula* f1 = uo->child();
const formula* tmp = NULL;
inf_form_right_recurse_visitor v(uo); inf_form_right_recurse_visitor v(uo);
switch (uo->op()) switch (uo->op())
{ {
@ -460,38 +449,46 @@ namespace spot
result_ = true; result_ = true;
return; return;
case unop::X: case unop::X:
if (node_type(f) == node_type_form_visitor::Unop) {
if (dynamic_cast<const unop*>(f)->op() == unop::X) { const unop* op = dynamic_cast<const unop*>(f);
result_ = inf_form(f1,dynamic_cast<const unop*>(f)->child()); if (op && op->op() == unop::X)
} result_ = inf_form(f1, op->child());
}
return; return;
case unop::F: case unop::F:
if (this->nodeX()) return; {
/* F(a) = true U a */ /* F(a) = true U a */
tmp = binop::instance(binop::U,constant::true_instance(),clone(f1)); const formula* tmp = binop::instance(binop::U,
if (this->special_case(tmp)){ constant::true_instance(),
result_ = true; clone(f1));
if (special_case(tmp))
{
result_ = true;
spot::ltl::destroy(tmp);
return;
}
if (inf_form(tmp, f))
result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
} }
if (inf_form(tmp,f))
result_ = true;
spot::ltl::destroy(tmp);
return;
case unop::G: case unop::G:
if (this->nodeX()) return; {
/* F(a) = false R a */ /* F(a) = false R a */
tmp = binop::instance(binop::R, const formula* tmp = binop::instance(binop::R,
constant::false_instance(),clone(f1)); constant::false_instance(),
if (this->special_case(tmp)){ clone(f1));
result_ = true; if (special_case(tmp))
{
result_ = true;
spot::ltl::destroy(tmp);
return;
}
if (inf_form(f1, f))
result_ = true;
spot::ltl::destroy(tmp); spot::ltl::destroy(tmp);
return; return;
} }
if (inf_form(f1,f))
result_ = true;
spot::ltl::destroy(tmp);
return;
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);
@ -500,9 +497,7 @@ namespace spot
void void
visit(const binop* bo) visit(const binop* bo)
{ {
if (this->nodeX()) return; if (special_case(bo))
if (this->special_case(bo))
{ {
result_ = true; result_ = true;
return; return;
@ -517,11 +512,11 @@ 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 (inf_form(f1, f) && inf_form(f2, f))
result_ = true; result_ = true;
return; return;
case binop::R: case binop::R:
if ((inf_form(f2,f))) if (inf_form(f2, f))
result_ = true; result_ = true;
return; return;
} }
@ -532,20 +527,18 @@ namespace spot
void void
visit(const multop* mo) visit(const multop* mo)
{ {
if (this->nodeX()) return;
multop::type op = mo->op(); multop::type op = mo->op();
unsigned mos = mo->size(); unsigned mos = mo->size();
switch (op) switch (op)
{ {
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 (inf_form(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 (!inf_form(mo->nth(i), f))
return; return;
result_ = true; result_ = true;
break; break;
@ -557,30 +550,27 @@ namespace spot
const formula* f; const formula* f;
}; };
bool inf_form(const formula* f1, const formula* f2) bool
inf_form(const formula* f1, const formula* f2)
{ {
/* f1 and f2 are unabbreviate */ /* f1 and f2 are unabbreviated */
if (f1 == f2) return true; if (f1 == f2)
return true;
inf_form_left_recurse_visitor v1(f2); inf_form_left_recurse_visitor v1(f2);
inf_form_right_recurse_visitor v2(f1); inf_form_right_recurse_visitor v2(f1);
if ((node_type(f1) == node_type_form_visitor::Const) &&
(node_type(f2) == node_type_form_visitor::Const)) if (f2 == constant::true_instance()
if ((dynamic_cast<const constant*>(f2)->val() == constant::True) || || f1 == constant::false_instance())
(dynamic_cast<const constant*>(f1)->val() == constant::False)) return true;
{
return true;
}
const_cast<formula*>(f1)->accept(v1); const_cast<formula*>(f1)->accept(v1);
if (v1.result()) { if (v1.result())
return true; return true;
}
const_cast<formula*>(f2)->accept(v2); const_cast<formula*>(f2)->accept(v2);
if (v2.result()) { if (v2.result())
return true; return true;
}
return false; return false;
} }
@ -590,11 +580,11 @@ namespace spot
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 == 0)? clone(f1) : clone(f2)); (!n) ? clone(f1) : clone(f2));
const formula* ftmp4 = spot::ltl::negative_normal_form((n == 0)? f2 : f1); const formula* ftmp4 = spot::ltl::negative_normal_form((!n) ? f2 : f1);
const formula* ftmp5; const formula* ftmp5;
const formula* ftmp6; const formula* ftmp6;
bool retour; bool result;
ftmp2 = spot::ltl::unabbreviate_logic(ftmp3); ftmp2 = spot::ltl::unabbreviate_logic(ftmp3);
ftmp1 = spot::ltl::negative_normal_form(ftmp2); ftmp1 = spot::ltl::negative_normal_form(ftmp2);
@ -603,9 +593,9 @@ namespace spot
ftmp6 = spot::ltl::negative_normal_form(ftmp5); ftmp6 = spot::ltl::negative_normal_form(ftmp5);
if (n == 0) if (n == 0)
retour = inf_form(ftmp1, ftmp6); result = inf_form(ftmp1, ftmp6);
else else
retour = inf_form(ftmp6, ftmp1); result = inf_form(ftmp6, ftmp1);
spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp1);
spot::ltl::destroy(ftmp2); spot::ltl::destroy(ftmp2);
@ -614,8 +604,7 @@ namespace spot
spot::ltl::destroy(ftmp5); spot::ltl::destroy(ftmp5);
spot::ltl::destroy(ftmp6); spot::ltl::destroy(ftmp6);
return retour; return result;
} }
} }
} }