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

* src/ltlvisit/basereduc.cc, src/ltltest/inf.cc (main): Style.

Browse source
This commit is contained in:
martinez 2004-05-17 15:17:55 +00:00
parent 788ed772c2
commit 62a05ab1fb
3 changed files with 16 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
ChangeLog
View file

@ -1,5 +1,7 @@
2004-05-17 Thomas Martinez <martinez@src.lip6.fr> 2004-05-17 Thomas Martinez <martinez@src.lip6.fr>
* src/ltlvisit/basereduc.cc, src/ltltest/inf.cc (main): Style.
* src/ltlvisit/basereduc.cc (spot): 80 columns. * src/ltlvisit/basereduc.cc (spot): 80 columns.
* src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc, * src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc,
src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh, src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh,

3
src/ltltest/inf.cc
View file

@ -92,7 +92,8 @@ main(int argc, char** argv)
exit_return = 1; exit_return = 1;
} }
break; break;
default: break; default:
break;
} }
spot::ltl::dump(std::cout, f1); std::cout << std::endl; spot::ltl::dump(std::cout, f1); std::cout << std::endl;

19
src/ltlvisit/basereduc.cc
View file

@ -86,7 +86,8 @@ namespace spot
return; return;
/* XGF(f) = GF(f) */ /* XGF(f) = GF(f) */
if (is_GF(result_)) return; if (is_GF(result_))
return;
/* X(f1 & GF(f2)) = X(f1) & GF(F2) */ /* X(f1 & GF(f2)) = X(f1) & GF(F2) */
/* X(f1 | GF(f2)) = X(f1) | GF(F2) */ /* X(f1 | GF(f2)) = X(f1) | GF(F2) */
@ -338,7 +339,6 @@ namespace spot
void void
visit(multop* mo) visit(multop* mo)
{ {
if (mo == NULL);
multop::type op = mo->op(); multop::type op = mo->op();
unsigned mos = mo->size(); unsigned mos = mo->size();
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
@ -402,7 +402,8 @@ namespace spot
tmpUright = new multop::vec; tmpUright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++) for (multop::vec::iterator j = i; j != res->end(); j++)
{ {
if (*j == NULL) continue; if (*j == NULL)
continue;
if ((node_type(*j) == node_type_form_visitor::Binop) if ((node_type(*j) == node_type_form_visitor::Binop)
&& &&
(dynamic_cast<binop*>(*j)->op() == binop::U) && (dynamic_cast<binop*>(*j)->op() == binop::U) &&
@ -435,7 +436,8 @@ namespace spot
tmpRright = new multop::vec; tmpRright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++) for (multop::vec::iterator j = i; j != res->end(); j++)
{ {
if (*j == NULL) continue; if (*j == NULL)
continue;
if ((node_type(*j) == node_type_form_visitor::Binop) if ((node_type(*j) == node_type_form_visitor::Binop)
&& &&
(dynamic_cast<binop*>(*j)->op() == binop::R) && (dynamic_cast<binop*>(*j)->op() == binop::R) &&
@ -477,7 +479,8 @@ namespace spot
for (multop::vec::iterator i = res->begin(); i != res->end(); i++) for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
{ {
if (*i == NULL) continue; if (*i == NULL)
continue;
switch (node_type(*i)) switch (node_type(*i))
{ {
@ -510,7 +513,8 @@ namespace spot
tmpUright = new multop::vec; tmpUright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++) for (multop::vec::iterator j = i; j != res->end(); j++)
{ {
if (*j == NULL) continue; if (*j == NULL)
continue;
if ((node_type(*j) == node_type_form_visitor::Binop) if ((node_type(*j) == node_type_form_visitor::Binop)
&& &&
(dynamic_cast<binop*>(*j)->op() == binop::U) && (dynamic_cast<binop*>(*j)->op() == binop::U) &&
@ -541,7 +545,8 @@ namespace spot
tmpRright = new multop::vec; tmpRright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++) for (multop::vec::iterator j = i; j != res->end(); j++)
{ {
if (*j == NULL) continue; if (*j == NULL)
continue;
if ((node_type(*j) == node_type_form_visitor::Binop) if ((node_type(*j) == node_type_form_visitor::Binop)
&& &&
(dynamic_cast<binop*>(*j)->op() == binop::R) && (dynamic_cast<binop*>(*j)->op() == binop::R) &&