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

* src/sanity/style.test: Catch {.*{ and }.*}.

Browse source 
* src/sanity/80columns.test: Untabify files.
* iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-25 11:05:07 +00:00
parent 3426ece95c
commit 7eb5f3d81a
5 changed files with 131 additions and 106 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/sanity/style.test: Catch {.*{ and }.*}.
* src/sanity/80columns.test: Untabify files.
* iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines.
* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes. src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes.

3
iface/gspn/ltlgspn.cc
View file

@ -63,7 +63,8 @@ syntax(char* prog)
#ifdef SSP #ifdef SSP
<< " -e3 use semi-d. incl. Couvreur's emptiness-check" << " -e3 use semi-d. incl. Couvreur's emptiness-check"
<< std::endl << std::endl
<< " -e4 use semi-d. incl. Couvreur's emptiness-check's shy variant" << " -e4 use semi-d. incl. Couvreur's emptiness-check's "
<< "shy variant"
<< std::endl << std::endl
<< " -e5 use d. incl. Couvreur's emptiness-check's shy variant" << " -e5 use d. incl. Couvreur's emptiness-check's shy variant"
<< std::endl << std::endl

140
src/ltlvisit/basereduc.cc
View file

@ -80,24 +80,27 @@ namespace spot
return; return;
case unop::X: case unop::X:
/* X(true) = true // X(true) = true
X(false) = false */ // X(false) = false
if (node_type(result_) == (node_type_form_visitor::Const)) if (node_type(result_) == (node_type_form_visitor::Const))
return; return;
/* XGF(f) = GF(f) */ // XGF(f) = GF(f)
if (is_GF(result_)) if (is_GF(result_))
return; 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)
mo = dynamic_cast<multop*>(result_); mo = dynamic_cast<multop*>(result_);
if (mo && mo->size() == 2) if (mo && mo->size() == 2)
{ {
// FIXME: This is incomplete. It should be done for
// multops of any size.
if (is_GF(mo->nth(0))) if (is_GF(mo->nth(0)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, res->push_back
(unop::instance(unop::F,
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);
@ -107,7 +110,8 @@ namespace spot
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, res->push_back
(unop::instance(unop::F,
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);
@ -116,18 +120,17 @@ namespace spot
} }
} }
result_ = unop::instance(unop::X, result_); result_ = unop::instance(unop::X, result_);
return; return;
case unop::F: case unop::F:
/* F(true) = true // F(true) = true
F(false) = false */ // F(false) = false
if (node_type(result_) == (node_type_form_visitor::Const)) if (node_type(result_) == (node_type_form_visitor::Const))
return; return;
/* FX(a) = XF(a) */ // FX(a) = XF(a)
u = dynamic_cast<unop*>(result_); u = dynamic_cast<unop*>(result_);
if (u && u->op() == unop::X) if (u && u->op() == unop::X)
{ {
@ -139,16 +142,18 @@ namespace spot
return; return;
} }
/* F(f1 & GF(f2)) = F(f1) & GF(F2) */ // F(f1 & GF(f2)) = F(f1) & GF(F2)
mo = dynamic_cast<multop*>(result_); mo = dynamic_cast<multop*>(result_);
if (mo && mo->op() == multop::And) if (mo && mo->op() == multop::And
{ // FIXME: This is incomplete. It should be done for
if (mo->size() == 2) // "And"s of any size.
&& mo->size() == 2)
{ {
if (is_GF(mo->nth(0))) if (is_GF(mo->nth(0)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, res->push_back
(unop::instance(unop::F,
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);
@ -158,7 +163,8 @@ namespace spot
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, res->push_back
(unop::instance(unop::F,
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);
@ -166,7 +172,6 @@ namespace spot
return; return;
} }
} }
}
result_ = unop::instance(unop::F, result_); result_ = unop::instance(unop::F, result_);
@ -174,12 +179,12 @@ namespace spot
case unop::G: case unop::G:
/* G(true) = true // G(true) = true
G(false) = false */ // G(false) = false
if (node_type(result_) == (node_type_form_visitor::Const)) if (node_type(result_) == (node_type_form_visitor::Const))
return; return;
/* G(a R b) = G(b) */ // G(a R b) = G(b)
bo = dynamic_cast<binop*>(result_); bo = dynamic_cast<binop*>(result_);
if (bo && bo->op() == binop::R) if (bo && bo->op() == binop::R)
{ {
@ -189,7 +194,7 @@ namespace spot
return; return;
} }
/* GX(a) = XG(a) */ // GX(a) = XG(a)
u = dynamic_cast<unop*>(result_); u = dynamic_cast<unop*>(result_);
if (u && u->op() == unop::X) if (u && u->op() == unop::X)
{ {
@ -201,16 +206,18 @@ namespace spot
return; return;
} }
/* G(f1 | GF(f2)) = G(f1) | GF(F2) */ // G(f1 | GF(f2)) = G(f1) | GF(F2)
mo = dynamic_cast<multop*>(result_); mo = dynamic_cast<multop*>(result_);
if (mo && mo->op() == multop::Or) if (mo && mo->op() == multop::Or
{ // FIXME: This is incomplete. It should be done for
if (mo->size() == 2) // "Or"s of any size.
&& mo->size() == 2)
{ {
if (is_GF(mo->nth(0))) if (is_GF(mo->nth(0)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, res->push_back
(unop::instance(unop::F,
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);
@ -220,7 +227,8 @@ namespace spot
if (is_GF(mo->nth(1))) if (is_GF(mo->nth(1)))
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, res->push_back
(unop::instance(unop::F,
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);
@ -228,8 +236,6 @@ namespace spot
return; return;
} }
} }
}
result_ = unop::instance(unop::G, result_); result_ = unop::instance(unop::G, result_);
return; return;
@ -268,8 +274,8 @@ namespace spot
case binop::U: case binop::U:
f2 = basic_reduce_form(f2); f2 = basic_reduce_form(f2);
/* a U false = false // a U false = false
a U true = true */ // a U true = true
if (node_type(f2) == (node_type_form_visitor::Const)) if (node_type(f2) == (node_type_form_visitor::Const))
{ {
result_ = f2; result_ = f2;
@ -278,7 +284,7 @@ namespace spot
f1 = basic_reduce_form(f1); f1 = basic_reduce_form(f1);
/* X(a) U X(b) = X(a U b) */ // X(a) U X(b) = X(a U b)
fu1 = dynamic_cast<unop*>(f1); fu1 = dynamic_cast<unop*>(f1);
fu2 = dynamic_cast<unop*>(f2); fu2 = dynamic_cast<unop*>(f2);
if ((fu1 && fu2) && if ((fu1 && fu2) &&
@ -301,8 +307,8 @@ namespace spot
case binop::R: case binop::R:
f2 = basic_reduce_form(f2); f2 = basic_reduce_form(f2);
/* a R false = false // a R false = false
a R true = true */ // a R true = true
if (node_type(f2) == (node_type_form_visitor::Const)) if (node_type(f2) == (node_type_form_visitor::Const))
{ {
result_ = f2; result_ = f2;
@ -311,7 +317,7 @@ namespace spot
f1 = basic_reduce_form(f1); f1 = basic_reduce_form(f1);
/* X(a) R X(b) = X(a R b) */ // X(a) R X(b) = X(a R b)
fu1 = dynamic_cast<unop*>(f1); fu1 = dynamic_cast<unop*>(f1);
fu2 = dynamic_cast<unop*>(f2); fu2 = dynamic_cast<unop*>(f2);
if ((fu1 && fu2) && if ((fu1 && fu2) &&
@ -375,7 +381,7 @@ namespace spot
case node_type_form_visitor::Unop: case node_type_form_visitor::Unop:
/* Xa & Xb = X(a & b)*/ // Xa & Xb = X(a & b)
uo = dynamic_cast<unop*>(*i); uo = dynamic_cast<unop*>(*i);
if (uo && uo->op() == unop::X) if (uo && uo->op() == unop::X)
{ {
@ -383,7 +389,7 @@ namespace spot
break; break;
} }
/* FG(a) & FG(b) = FG(a & b)*/ // FG(a) & FG(b) = FG(a & b)
if (is_FG(*i)) if (is_FG(*i))
{ {
uo2 = dynamic_cast<unop*>(uo->child()); uo2 = dynamic_cast<unop*>(uo->child());
@ -395,19 +401,18 @@ namespace spot
case node_type_form_visitor::Binop: case node_type_form_visitor::Binop:
/* (a U b) & (c U b) = (a & c) U b */ // (a U b) & (c U b) = (a & c) U b
if (dynamic_cast<binop*>(*i)->op() == binop::U) if (dynamic_cast<binop*>(*i)->op() == binop::U)
{ {
ftmp = dynamic_cast<binop*>(*i)->second(); ftmp = dynamic_cast<binop*>(*i)->second();
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) if (!*j)
continue; 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) && && ftmp == dynamic_cast<binop*>(*j)->second())
(ftmp == dynamic_cast<binop*>(*j)->second()))
{ {
bo = dynamic_cast<binop*>(*j); bo = dynamic_cast<binop*>(*j);
tmpUright tmpUright
@ -415,7 +420,7 @@ namespace spot
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
*j = NULL; *j = 0;
} }
} }
} }
@ -429,19 +434,18 @@ namespace spot
break; break;
} }
/* (a R b) & (a R c) = a R (b & c) */ // (a R b) & (a R c) = a R (b & c)
if (dynamic_cast<binop*>(*i)->op() == binop::R) if (dynamic_cast<binop*>(*i)->op() == binop::R)
{ {
ftmp = dynamic_cast<binop*>(*i)->first(); ftmp = dynamic_cast<binop*>(*i)->first();
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) if (!*j)
continue; 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) && && ftmp == dynamic_cast<binop*>(*j)->first())
(ftmp == dynamic_cast<binop*>(*j)->first()))
{ {
bo = dynamic_cast<binop*>(*j); bo = dynamic_cast<binop*>(*j);
tmpRright tmpRright
@ -449,7 +453,7 @@ namespace spot
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
*j = NULL; *j = 0;
} }
} }
} }
@ -479,14 +483,14 @@ 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) if (!*i)
continue; continue;
switch (node_type(*i)) switch (node_type(*i))
{ {
case node_type_form_visitor::Unop: case node_type_form_visitor::Unop:
/* Xa | Xb = X(a | b)*/ // Xa | Xb = X(a | b)
uo = dynamic_cast<unop*>(*i); uo = dynamic_cast<unop*>(*i);
if (uo && uo->op() == unop::X) if (uo && uo->op() == unop::X)
{ {
@ -494,7 +498,7 @@ namespace spot
break; break;
} }
/* GF(a) | GF(b) = GF(a | b)*/ // GF(a) | GF(b) = GF(a | b)
if (is_GF(*i)) if (is_GF(*i))
{ {
uo2 = dynamic_cast<unop*>(uo->child()); uo2 = dynamic_cast<unop*>(uo->child());
@ -506,19 +510,18 @@ namespace spot
case node_type_form_visitor::Binop: case node_type_form_visitor::Binop:
/* (a U b) | (a U c) = a U (b | c) */ // (a U b) | (a U c) = a U (b | c)
if (dynamic_cast<binop*>(*i)->op() == binop::U) if (dynamic_cast<binop*>(*i)->op() == binop::U)
{ {
ftmp = dynamic_cast<binop*>(*i)->first(); ftmp = dynamic_cast<binop*>(*i)->first();
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) if (!*j)
continue; 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) && && ftmp == dynamic_cast<binop*>(*j)->first())
(ftmp == dynamic_cast<binop*>(*j)->first()))
{ {
bo = dynamic_cast<binop*>(*j); bo = dynamic_cast<binop*>(*j);
tmpUright tmpUright
@ -526,7 +529,7 @@ namespace spot
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
*j = NULL; *j = 0;
} }
} }
} }
@ -538,19 +541,18 @@ namespace spot
break; break;
} }
/* (a R b) | (c R b) = (a | c) R b */ // (a R b) | (c R b) = (a | c) R b
if (dynamic_cast<binop*>(*i)->op() == binop::R) if (dynamic_cast<binop*>(*i)->op() == binop::R)
{ {
ftmp = dynamic_cast<binop*>(*i)->second(); ftmp = dynamic_cast<binop*>(*i)->second();
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) if (!*j)
continue; 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) && && ftmp == dynamic_cast<binop*>(*j)->second())
(ftmp == dynamic_cast<binop*>(*j)->second()))
{ {
bo = dynamic_cast<binop*>(*j); bo = dynamic_cast<binop*>(*j);
tmpRright tmpRright
@ -558,7 +560,7 @@ namespace spot
if (j != i) if (j != i)
{ {
destroy(*j); destroy(*j);
*j = NULL; *j = 0;
} }
} }
} }

16
src/sanity/80columns.test
View file

@ -4,6 +4,18 @@
set -e set -e
untabify()
{
perl -pe 's/^((.{8})*)\t/$1 /g;
s/^(.(.{8})*)\t/$1 /g;
s/^(..(.{8})*)\t/$1 /g;
s/^(...(.{8})*)\t/$1 /g;
s/^(....(.{8})*)\t/$1 /g;
s/^(.....(.{8})*)\t/$1 /g;
s/^(......(.{8})*)\t/$1 /g;
s/^(.......(.{8})*)\t/$1 /g;' $1
}
rm -f failures rm -f failures
for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
@ -11,8 +23,8 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
find "$dir" \( -name "${1-*}.hh" -o -name "${1-*}.cc" \ find "$dir" \( -name "${1-*}.hh" -o -name "${1-*}.cc" \
-o -name "${1-*}.test" \) -a -type f -a -print | -o -name "${1-*}.test" \) -a -type f -a -print |
while read file; do while read file; do
x='.........................................' x='........................................'
if grep -q $x$x "$file"; then if (untabify $file | grep -q $x.$x) 2>/dev/null; then
if grep 'GNU Bison' "$file" >/dev/null || if grep 'GNU Bison' "$file" >/dev/null ||
grep 'generated by flex' "$file" >/dev/null ; then grep 'generated by flex' "$file" >/dev/null ; then
: :

6
src/sanity/style.test
View file

@ -98,6 +98,12 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep -v 'for (;;)' $tmp | grep ';[^ ")]' && grep -v 'for (;;)' $tmp | grep ';[^ ")]' &&
diag 'Must have space or newline after semicolon.' diag 'Must have space or newline after semicolon.'
grep '}.*}' $tmp &&
diag 'No two } on the same line.'
grep '{.*{' $tmp &&
diag 'No two { on the same line.'
$fail && echo "$file" >>failures $fail && echo "$file" >>failures
done done
done done