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

* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,

Browse source 
src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-25 09:14:51 +00:00
parent c68d182951
commit 3426ece95c
4 changed files with 68 additions and 65 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes.
* wrap/python/cgi/ltl2tgba.in: Typos. * wrap/python/cgi/ltl2tgba.in: Typos.
2004-05-24 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-24 Alexandre Duret-Lutz <adl@src.lip6.fr>

36
src/ltlvisit/basereduc.cc
View file

@ -101,7 +101,7 @@ namespace spot
basic_reduce_form(mo->nth(1)))); basic_reduce_form(mo->nth(1))));
res->push_back(basic_reduce_form(mo->nth(0))); res->push_back(basic_reduce_form(mo->nth(0)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
spot::ltl::destroy(mo); destroy(mo);
return; return;
} }
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
@ -111,7 +111,7 @@ namespace spot
basic_reduce_form(mo->nth(0)))); basic_reduce_form(mo->nth(0))));
res->push_back(basic_reduce_form(mo->nth(1))); res->push_back(basic_reduce_form(mo->nth(1)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
spot::ltl::destroy(mo); destroy(mo);
return; return;
} }
} }
@ -135,7 +135,7 @@ namespace spot
unop::instance(unop::X, unop::instance(unop::X,
unop::instance(unop::F, unop::instance(unop::F,
basic_reduce_form(u->child()))); basic_reduce_form(u->child())));
spot::ltl::destroy(u); destroy(u);
return; return;
} }
@ -152,7 +152,7 @@ namespace spot
basic_reduce_form(mo->nth(1)))); basic_reduce_form(mo->nth(1))));
res->push_back(basic_reduce_form(mo->nth(0))); res->push_back(basic_reduce_form(mo->nth(0)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
spot::ltl::destroy(mo); destroy(mo);
return; return;
} }
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
@ -162,7 +162,7 @@ namespace spot
basic_reduce_form(mo->nth(0)))); basic_reduce_form(mo->nth(0))));
res->push_back(basic_reduce_form(mo->nth(1))); res->push_back(basic_reduce_form(mo->nth(1)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
spot::ltl::destroy(mo); destroy(mo);
return; return;
} }
} }
@ -185,7 +185,7 @@ namespace spot
{ {
result_ = unop::instance(unop::G, result_ = unop::instance(unop::G,
basic_reduce_form(bo->second())); basic_reduce_form(bo->second()));
spot::ltl::destroy(bo); destroy(bo);
return; return;
} }
@ -197,7 +197,7 @@ namespace spot
unop::instance(unop::X, unop::instance(unop::X,
unop::instance(unop::G, unop::instance(unop::G,
basic_reduce_form(u->child()))); basic_reduce_form(u->child())));
spot::ltl::destroy(u); destroy(u);
return; return;
} }
@ -214,7 +214,7 @@ namespace spot
basic_reduce_form(mo->nth(1)))); basic_reduce_form(mo->nth(1))));
res->push_back(basic_reduce_form(mo->nth(0))); res->push_back(basic_reduce_form(mo->nth(0)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
spot::ltl::destroy(mo); destroy(mo);
return; return;
} }
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
@ -224,7 +224,7 @@ namespace spot
basic_reduce_form(mo->nth(0)))); basic_reduce_form(mo->nth(0))));
res->push_back(basic_reduce_form(mo->nth(1))); res->push_back(basic_reduce_form(mo->nth(1)));
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
spot::ltl::destroy(mo); destroy(mo);
return; return;
} }
} }
@ -289,9 +289,9 @@ namespace spot
basic_reduce_form(fu1->child()), basic_reduce_form(fu1->child()),
basic_reduce_form(fu2->child())); basic_reduce_form(fu2->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
spot::ltl::destroy(f1); destroy(f1);
spot::ltl::destroy(f2); destroy(f2);
spot::ltl::destroy(ftmp); destroy(ftmp);
return; return;
} }
@ -322,9 +322,9 @@ namespace spot
basic_reduce_form(fu1->child()), basic_reduce_form(fu1->child()),
basic_reduce_form(fu2->child())); basic_reduce_form(fu2->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
spot::ltl::destroy(f1); destroy(f1);
spot::ltl::destroy(f2); destroy(f2);
spot::ltl::destroy(ftmp); destroy(ftmp);
return; return;
} }
@ -448,7 +448,7 @@ namespace spot
->push_back(basic_reduce_form(bo->second())); ->push_back(basic_reduce_form(bo->second()));
if (j != i) if (j != i)
{ {
spot::ltl::destroy(*j); destroy(*j);
*j = NULL; *j = NULL;
} }
} }
@ -467,7 +467,7 @@ namespace spot
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce_form(*i));
break; break;
} }
spot::ltl::destroy(*i); destroy(*i);
} }
delete(tmpGF); delete(tmpGF);
@ -576,7 +576,7 @@ namespace spot
tmpOther->push_back(basic_reduce_form(*i)); tmpOther->push_back(basic_reduce_form(*i));
break; break;
} }
spot::ltl::destroy(*i); destroy(*i);
} }
delete(tmpFG); delete(tmpFG);

32
src/ltlvisit/forminf.cc
View file

@ -313,7 +313,7 @@ namespace spot
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); destroy(tmp);
return; return;
} }
/* Unreachable code. */ /* Unreachable code. */
@ -467,12 +467,12 @@ namespace spot
if (special_case(tmp)) if (special_case(tmp))
{ {
result_ = true; result_ = true;
spot::ltl::destroy(tmp); destroy(tmp);
return; return;
} }
if (inf_form(tmp, f)) if (inf_form(tmp, f))
result_ = true; result_ = true;
spot::ltl::destroy(tmp); destroy(tmp);
return; return;
} }
case unop::G: case unop::G:
@ -484,12 +484,12 @@ namespace spot
if (special_case(tmp)) if (special_case(tmp))
{ {
result_ = true; result_ = true;
spot::ltl::destroy(tmp); destroy(tmp);
return; return;
} }
if (inf_form(f1, f)) if (inf_form(f1, f))
result_ = true; result_ = true;
spot::ltl::destroy(tmp); destroy(tmp);
return; return;
} }
} }
@ -584,28 +584,28 @@ namespace spot
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)); (!n) ? clone(f1) : clone(f2));
const formula* ftmp4 = spot::ltl::negative_normal_form((!n) ? f2 : f1); const formula* ftmp4 = negative_normal_form((!n) ? f2 : f1);
const formula* ftmp5; const formula* ftmp5;
const formula* ftmp6; const formula* ftmp6;
bool result; bool result;
ftmp2 = spot::ltl::unabbreviate_logic(ftmp3); ftmp2 = unabbreviate_logic(ftmp3);
ftmp1 = spot::ltl::negative_normal_form(ftmp2); ftmp1 = negative_normal_form(ftmp2);
ftmp5 = spot::ltl::unabbreviate_logic(ftmp4); ftmp5 = unabbreviate_logic(ftmp4);
ftmp6 = spot::ltl::negative_normal_form(ftmp5); ftmp6 = negative_normal_form(ftmp5);
if (n == 0) if (n == 0)
result = inf_form(ftmp1, ftmp6); result = inf_form(ftmp1, ftmp6);
else else
result = inf_form(ftmp6, ftmp1); result = inf_form(ftmp6, ftmp1);
spot::ltl::destroy(ftmp1); destroy(ftmp1);
spot::ltl::destroy(ftmp2); destroy(ftmp2);
spot::ltl::destroy(ftmp3); destroy(ftmp3);
spot::ltl::destroy(ftmp4); destroy(ftmp4);
spot::ltl::destroy(ftmp5); destroy(ftmp5);
spot::ltl::destroy(ftmp6); destroy(ftmp6);
return result; return result;
} }

62
src/ltlvisit/reducform.cc
View file

@ -141,14 +141,14 @@ namespace spot
if (inf) if (inf)
{ {
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); destroy(f1);
return; return;
} }
/* !b < a => a U b = Fb */ /* !b < a => a U b = Fb */
if (infnegleft) if (infnegleft)
{ {
result_ = unop::instance(unop::F, f2); result_ = unop::instance(unop::F, f2);
spot::ltl::destroy(f1); destroy(f1);
return; return;
} }
/* a < b => a U (b U c) = (b U c) */ /* a < b => a U (b U c) = (b U c) */
@ -157,7 +157,7 @@ namespace spot
&& inf_form(f1, dynamic_cast<binop*>(f2)->first())) && inf_form(f1, dynamic_cast<binop*>(f2)->first()))
{ {
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); destroy(f1);
return; return;
} }
break; break;
@ -167,14 +167,14 @@ namespace spot
if (infinv) if (infinv)
{ {
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); destroy(f1);
return; return;
} }
/* b < !a => a R b = Gb */ /* b < !a => a R b = Gb */
if (infnegright) if (infnegright)
{ {
result_ = unop::instance(unop::G, f2); result_ = unop::instance(unop::G, f2);
spot::ltl::destroy(f1); destroy(f1);
return; return;
} }
/* b < a => a R (b R c) = b R c */ /* b < a => a R (b R c) = b R c */
@ -183,7 +183,7 @@ namespace spot
&& inf_form(dynamic_cast<binop*>(f2)->first(), f1)) && inf_form(dynamic_cast<binop*>(f2)->first(), f1))
{ {
result_ = f2; result_ = f2;
spot::ltl::destroy(f1); destroy(f1);
return; return;
} }
break; break;
@ -225,14 +225,14 @@ namespace spot
if (inf_form(f1, f2)) // f1 < f2 if (inf_form(f1, f2)) // f1 < f2
{ {
f1 = f2; f1 = f2;
spot::ltl::destroy(*indextmp); destroy(*indextmp);
res->erase(indextmp); res->erase(indextmp);
indextmp = index; indextmp = index;
index--; index--;
} }
else if (inf_form(f2, f1)) // f2 < f1 else if (inf_form(f2, f1)) // f2 < f1
{ {
spot::ltl::destroy(*index); destroy(*index);
res->erase(index); res->erase(index);
index--; index--;
} }
@ -252,14 +252,14 @@ namespace spot
/* a < b => a & b = a */ /* a < b => a & b = a */
if (inf_form(f1, f2)) // f1 < f2 if (inf_form(f1, f2)) // f1 < f2
{ {
spot::ltl::destroy(*index); destroy(*index);
res->erase(index); res->erase(index);
index--; index--;
} }
else if (inf_form(f2, f1)) // f2 < f1 else if (inf_form(f2, f1)) // f2 < f1
{ {
f1 = f2; f1 = f2;
spot::ltl::destroy(*indextmp); destroy(*indextmp);
res->erase(indextmp); res->erase(indextmp);
indextmp = index; indextmp = index;
index--; index--;
@ -278,7 +278,7 @@ namespace spot
{ {
for (multop::vec::iterator j = res->begin(); for (multop::vec::iterator j = res->begin();
j != res->end(); j++) j != res->end(); j++)
spot::ltl::destroy(*j); destroy(*j);
if (mo->op() == multop::Or) if (mo->op() == multop::Or)
result_ = constant::true_instance(); result_ = constant::true_instance();
else else
@ -308,18 +308,18 @@ namespace spot
formula* formula*
reduce_form(const formula* f, option o) reduce_form(const formula* f, option o)
{ {
spot::ltl::formula* ftmp1 = NULL; formula* ftmp1 = NULL;
spot::ltl::formula* ftmp2 = NULL; formula* ftmp2 = NULL;
reduce_form_visitor v(o); reduce_form_visitor v(o);
if (o == BRI || o == InfBase || if (o == BRI || o == InfBase ||
o == EventualUniversalBase) o == EventualUniversalBase)
{ {
ftmp1 = spot::ltl::basic_reduce_form(f); ftmp1 = basic_reduce_form(f);
const_cast<formula*>(ftmp1)->accept(v); const_cast<formula*>(ftmp1)->accept(v);
ftmp2 = spot::ltl::basic_reduce_form(v.result()); ftmp2 = basic_reduce_form(v.result());
spot::ltl::destroy(ftmp1); destroy(ftmp1);
spot::ltl::destroy(v.result()); destroy(v.result());
return ftmp2; return ftmp2;
} }
@ -336,41 +336,41 @@ namespace spot
formula* formula*
reduce(const formula* f, option o) reduce(const formula* f, option o)
{ {
spot::ltl::formula* ftmp1; formula* ftmp1;
spot::ltl::formula* ftmp2; formula* ftmp2;
spot::ltl::formula* ftmp3; formula* ftmp3;
ftmp1 = spot::ltl::unabbreviate_logic(f); ftmp1 = unabbreviate_logic(f);
ftmp2 = spot::ltl::negative_normal_form(ftmp1); ftmp2 = negative_normal_form(ftmp1);
switch (o) switch (o)
{ {
case Base: case Base:
ftmp3 = spot::ltl::basic_reduce_form(ftmp2); ftmp3 = basic_reduce_form(ftmp2);
break; break;
case Inf: case Inf:
ftmp3 = spot::ltl::reduce_form(ftmp2, o); ftmp3 = reduce_form(ftmp2, o);
break; break;
case InfBase: case InfBase:
ftmp3 = spot::ltl::reduce_form(ftmp2, o); ftmp3 = reduce_form(ftmp2, o);
break; break;
case EventualUniversal: case EventualUniversal:
ftmp3 = spot::ltl::reduce_form(ftmp2, o); ftmp3 = reduce_form(ftmp2, o);
break; break;
case EventualUniversalBase: case EventualUniversalBase:
ftmp3 = spot::ltl::reduce_form(ftmp2, o); ftmp3 = reduce_form(ftmp2, o);
break; break;
case InfEventualUniversal: case InfEventualUniversal:
ftmp3 = spot::ltl::reduce_form(ftmp2, o); ftmp3 = reduce_form(ftmp2, o);
break; break;
case BRI: case BRI:
ftmp3 = spot::ltl::reduce_form(ftmp2, o); ftmp3 = reduce_form(ftmp2, o);
break; break;
default: default:
assert(0); assert(0);
} }
spot::ltl::destroy(ftmp1); destroy(ftmp1);
spot::ltl::destroy(ftmp2); destroy(ftmp2);
return ftmp3; return ftmp3;
} }