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

Avoid containment checks on equal formulae.

Browse source 
* src/ltlvisit/contain.cc
(language_containment_checker::contained,
language_containment_checker::neg_contained,
language_containment_checker::contained_neg): Detect
cases where both formulae are equal.
This commit is contained in:
Alexandre Duret-Lutz 2011-10-30 18:37:42 +01:00
parent 58bbaa0859
commit c54627bebd
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ltlvisit/contain.cc
View file

@ -89,6 +89,8 @@ namespace spot
bool bool
language_containment_checker::contained(const formula* l, const formula* g) language_containment_checker::contained(const formula* l, const formula* g)
{ {
if (l == g)
return true;
record_* rl = register_formula_(l); record_* rl = register_formula_(l);
const formula* ng = unop::instance(unop::Not, g->clone()); const formula* ng = unop::instance(unop::Not, g->clone());
record_* rng = register_formula_(ng); record_* rng = register_formula_(ng);
@ -101,12 +103,16 @@ namespace spot
language_containment_checker::neg_contained(const formula* l, language_containment_checker::neg_contained(const formula* l,
const formula* g) const formula* g)
{ {
if (l == g)
return false;
const formula* nl = unop::instance(unop::Not, l->clone()); const formula* nl = unop::instance(unop::Not, l->clone());
record_* rnl = register_formula_(nl); record_* rnl = register_formula_(nl);
const formula* ng = unop::instance(unop::Not, g->clone()); const formula* ng = unop::instance(unop::Not, g->clone());
record_* rng = register_formula_(ng); record_* rng = register_formula_(ng);
nl->destroy(); nl->destroy();
ng->destroy(); ng->destroy();
if (nl == g)
return true;
return incompatible_(rnl, rng); return incompatible_(rnl, rng);
} }
@ -115,6 +121,8 @@ namespace spot
language_containment_checker::contained_neg(const formula* l, language_containment_checker::contained_neg(const formula* l,
const formula* g) const formula* g)
{ {
if (l == g)
return false;
record_* rl = register_formula_(l); record_* rl = register_formula_(l);
record_* rg = register_formula_(g); record_* rg = register_formula_(g);
return incompatible_(rl, rg); return incompatible_(rl, rg);