From 3426ece95c4a639188615ade3b8fca5e8d6f8c4f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 25 May 2004 09:14:51 +0000 Subject: [PATCH] * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes. --- ChangeLog | 3 ++ src/ltlvisit/basereduc.cc | 36 +++++++++++------------ src/ltlvisit/forminf.cc | 32 ++++++++++---------- src/ltlvisit/reducform.cc | 62 +++++++++++++++++++-------------------- 4 files changed, 68 insertions(+), 65 deletions(-) diff --git a/ChangeLog b/ChangeLog index 9686b4b99..955a7c801 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2004-05-25 Alexandre Duret-Lutz + * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, + src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes. + * wrap/python/cgi/ltl2tgba.in: Typos. 2004-05-24 Alexandre Duret-Lutz diff --git a/src/ltlvisit/basereduc.cc b/src/ltlvisit/basereduc.cc index 642d5db4d..738a6cb3e 100644 --- a/src/ltlvisit/basereduc.cc +++ b/src/ltlvisit/basereduc.cc @@ -101,7 +101,7 @@ namespace spot basic_reduce_form(mo->nth(1)))); res->push_back(basic_reduce_form(mo->nth(0))); result_ = multop::instance(mo->op(), res); - spot::ltl::destroy(mo); + destroy(mo); return; } if (is_GF(mo->nth(1))) @@ -111,7 +111,7 @@ namespace spot basic_reduce_form(mo->nth(0)))); res->push_back(basic_reduce_form(mo->nth(1))); result_ = multop::instance(mo->op(), res); - spot::ltl::destroy(mo); + destroy(mo); return; } } @@ -135,7 +135,7 @@ namespace spot unop::instance(unop::X, unop::instance(unop::F, basic_reduce_form(u->child()))); - spot::ltl::destroy(u); + destroy(u); return; } @@ -152,7 +152,7 @@ namespace spot basic_reduce_form(mo->nth(1)))); res->push_back(basic_reduce_form(mo->nth(0))); result_ = multop::instance(mo->op(), res); - spot::ltl::destroy(mo); + destroy(mo); return; } if (is_GF(mo->nth(1))) @@ -162,7 +162,7 @@ namespace spot basic_reduce_form(mo->nth(0)))); res->push_back(basic_reduce_form(mo->nth(1))); result_ = multop::instance(mo->op(), res); - spot::ltl::destroy(mo); + destroy(mo); return; } } @@ -185,7 +185,7 @@ namespace spot { result_ = unop::instance(unop::G, basic_reduce_form(bo->second())); - spot::ltl::destroy(bo); + destroy(bo); return; } @@ -197,7 +197,7 @@ namespace spot unop::instance(unop::X, unop::instance(unop::G, basic_reduce_form(u->child()))); - spot::ltl::destroy(u); + destroy(u); return; } @@ -214,7 +214,7 @@ namespace spot basic_reduce_form(mo->nth(1)))); res->push_back(basic_reduce_form(mo->nth(0))); result_ = multop::instance(mo->op(), res); - spot::ltl::destroy(mo); + destroy(mo); return; } if (is_GF(mo->nth(1))) @@ -224,7 +224,7 @@ namespace spot basic_reduce_form(mo->nth(0)))); res->push_back(basic_reduce_form(mo->nth(1))); result_ = multop::instance(mo->op(), res); - spot::ltl::destroy(mo); + destroy(mo); return; } } @@ -289,9 +289,9 @@ namespace spot basic_reduce_form(fu1->child()), basic_reduce_form(fu2->child())); result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); - spot::ltl::destroy(f1); - spot::ltl::destroy(f2); - spot::ltl::destroy(ftmp); + destroy(f1); + destroy(f2); + destroy(ftmp); return; } @@ -322,9 +322,9 @@ namespace spot basic_reduce_form(fu1->child()), basic_reduce_form(fu2->child())); result_ = unop::instance(unop::X, basic_reduce_form(ftmp)); - spot::ltl::destroy(f1); - spot::ltl::destroy(f2); - spot::ltl::destroy(ftmp); + destroy(f1); + destroy(f2); + destroy(ftmp); return; } @@ -448,7 +448,7 @@ namespace spot ->push_back(basic_reduce_form(bo->second())); if (j != i) { - spot::ltl::destroy(*j); + destroy(*j); *j = NULL; } } @@ -467,7 +467,7 @@ namespace spot tmpOther->push_back(basic_reduce_form(*i)); break; } - spot::ltl::destroy(*i); + destroy(*i); } delete(tmpGF); @@ -576,7 +576,7 @@ namespace spot tmpOther->push_back(basic_reduce_form(*i)); break; } - spot::ltl::destroy(*i); + destroy(*i); } delete(tmpFG); diff --git a/src/ltlvisit/forminf.cc b/src/ltlvisit/forminf.cc index 77e511495..81633999b 100644 --- a/src/ltlvisit/forminf.cc +++ b/src/ltlvisit/forminf.cc @@ -313,7 +313,7 @@ namespace spot tmp = constant::false_instance(); if (inf_form(f, tmp)) result_ = true; - spot::ltl::destroy(tmp); + destroy(tmp); return; } /* Unreachable code. */ @@ -467,12 +467,12 @@ namespace spot if (special_case(tmp)) { result_ = true; - spot::ltl::destroy(tmp); + destroy(tmp); return; } if (inf_form(tmp, f)) result_ = true; - spot::ltl::destroy(tmp); + destroy(tmp); return; } case unop::G: @@ -484,12 +484,12 @@ namespace spot if (special_case(tmp)) { result_ = true; - spot::ltl::destroy(tmp); + destroy(tmp); return; } if (inf_form(f1, f)) result_ = true; - spot::ltl::destroy(tmp); + destroy(tmp); return; } } @@ -584,28 +584,28 @@ namespace spot const formula* ftmp2; const formula* ftmp3 = unop::instance(unop::Not, (!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* ftmp6; bool result; - ftmp2 = spot::ltl::unabbreviate_logic(ftmp3); - ftmp1 = spot::ltl::negative_normal_form(ftmp2); + ftmp2 = unabbreviate_logic(ftmp3); + ftmp1 = negative_normal_form(ftmp2); - ftmp5 = spot::ltl::unabbreviate_logic(ftmp4); - ftmp6 = spot::ltl::negative_normal_form(ftmp5); + ftmp5 = unabbreviate_logic(ftmp4); + ftmp6 = negative_normal_form(ftmp5); if (n == 0) result = inf_form(ftmp1, ftmp6); else result = inf_form(ftmp6, ftmp1); - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(ftmp2); - spot::ltl::destroy(ftmp3); - spot::ltl::destroy(ftmp4); - spot::ltl::destroy(ftmp5); - spot::ltl::destroy(ftmp6); + destroy(ftmp1); + destroy(ftmp2); + destroy(ftmp3); + destroy(ftmp4); + destroy(ftmp5); + destroy(ftmp6); return result; } diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index 95b17e698..455fdfc91 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.cc @@ -141,14 +141,14 @@ namespace spot if (inf) { result_ = f2; - spot::ltl::destroy(f1); + destroy(f1); return; } /* !b < a => a U b = Fb */ if (infnegleft) { result_ = unop::instance(unop::F, f2); - spot::ltl::destroy(f1); + destroy(f1); return; } /* a < b => a U (b U c) = (b U c) */ @@ -157,7 +157,7 @@ namespace spot && inf_form(f1, dynamic_cast(f2)->first())) { result_ = f2; - spot::ltl::destroy(f1); + destroy(f1); return; } break; @@ -167,14 +167,14 @@ namespace spot if (infinv) { result_ = f2; - spot::ltl::destroy(f1); + destroy(f1); return; } /* b < !a => a R b = Gb */ if (infnegright) { result_ = unop::instance(unop::G, f2); - spot::ltl::destroy(f1); + destroy(f1); return; } /* b < a => a R (b R c) = b R c */ @@ -183,7 +183,7 @@ namespace spot && inf_form(dynamic_cast(f2)->first(), f1)) { result_ = f2; - spot::ltl::destroy(f1); + destroy(f1); return; } break; @@ -225,14 +225,14 @@ namespace spot if (inf_form(f1, f2)) // f1 < f2 { f1 = f2; - spot::ltl::destroy(*indextmp); + destroy(*indextmp); res->erase(indextmp); indextmp = index; index--; } else if (inf_form(f2, f1)) // f2 < f1 { - spot::ltl::destroy(*index); + destroy(*index); res->erase(index); index--; } @@ -252,14 +252,14 @@ namespace spot /* a < b => a & b = a */ if (inf_form(f1, f2)) // f1 < f2 { - spot::ltl::destroy(*index); + destroy(*index); res->erase(index); index--; } else if (inf_form(f2, f1)) // f2 < f1 { f1 = f2; - spot::ltl::destroy(*indextmp); + destroy(*indextmp); res->erase(indextmp); indextmp = index; index--; @@ -278,7 +278,7 @@ namespace spot { for (multop::vec::iterator j = res->begin(); j != res->end(); j++) - spot::ltl::destroy(*j); + destroy(*j); if (mo->op() == multop::Or) result_ = constant::true_instance(); else @@ -308,18 +308,18 @@ namespace spot formula* reduce_form(const formula* f, option o) { - spot::ltl::formula* ftmp1 = NULL; - spot::ltl::formula* ftmp2 = NULL; + formula* ftmp1 = NULL; + formula* ftmp2 = NULL; reduce_form_visitor v(o); if (o == BRI || o == InfBase || o == EventualUniversalBase) { - ftmp1 = spot::ltl::basic_reduce_form(f); + ftmp1 = basic_reduce_form(f); const_cast(ftmp1)->accept(v); - ftmp2 = spot::ltl::basic_reduce_form(v.result()); - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(v.result()); + ftmp2 = basic_reduce_form(v.result()); + destroy(ftmp1); + destroy(v.result()); return ftmp2; } @@ -336,41 +336,41 @@ namespace spot formula* reduce(const formula* f, option o) { - spot::ltl::formula* ftmp1; - spot::ltl::formula* ftmp2; - spot::ltl::formula* ftmp3; + formula* ftmp1; + formula* ftmp2; + formula* ftmp3; - ftmp1 = spot::ltl::unabbreviate_logic(f); - ftmp2 = spot::ltl::negative_normal_form(ftmp1); + ftmp1 = unabbreviate_logic(f); + ftmp2 = negative_normal_form(ftmp1); switch (o) { case Base: - ftmp3 = spot::ltl::basic_reduce_form(ftmp2); + ftmp3 = basic_reduce_form(ftmp2); break; case Inf: - ftmp3 = spot::ltl::reduce_form(ftmp2, o); + ftmp3 = reduce_form(ftmp2, o); break; case InfBase: - ftmp3 = spot::ltl::reduce_form(ftmp2, o); + ftmp3 = reduce_form(ftmp2, o); break; case EventualUniversal: - ftmp3 = spot::ltl::reduce_form(ftmp2, o); + ftmp3 = reduce_form(ftmp2, o); break; case EventualUniversalBase: - ftmp3 = spot::ltl::reduce_form(ftmp2, o); + ftmp3 = reduce_form(ftmp2, o); break; case InfEventualUniversal: - ftmp3 = spot::ltl::reduce_form(ftmp2, o); + ftmp3 = reduce_form(ftmp2, o); break; case BRI: - ftmp3 = spot::ltl::reduce_form(ftmp2, o); + ftmp3 = reduce_form(ftmp2, o); break; default: assert(0); } - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(ftmp2); + destroy(ftmp1); + destroy(ftmp2); return ftmp3; }