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

* src/ltlvisit/tostring.cc (to_spin_string_visitor,

Browse source 
to_string_visitor): Do not parenthesize the top-level formula.
* tgbatest/explicit.test, tgbatest/explpro2.test,
tgbatest/explpro3.test, tgbatest/explprod.test,
tgbatest/readsave.test, tgbatest/tgbaread.test,
tgbatest/tripprod.test: Adjust expected output.
* sanity/style.test: Fix regexes to catch an error seen in
tostring.cc.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-14 11:01:14 +00:00
parent 6f4ab3af6c
commit 35ef738ff9
10 changed files with 72 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,5 +1,14 @@
2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/tostring.cc (to_spin_string_visitor,
to_string_visitor): Do not parenthesize the top-level formula.
* tgbatest/explicit.test, tgbatest/explpro2.test,
tgbatest/explpro3.test, tgbatest/explprod.test,
tgbatest/readsave.test, tgbatest/tgbaread.test,
tgbatest/tripprod.test: Adjust expected output.
* sanity/style.test: Fix regexes to catch an error seen in
tostring.cc.
* src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component): * src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component):
Do not try to erase state that are not found in H. Do not try to erase state that are not found in H.
Report from Soheib Baarir. Report from Soheib Baarir.

46
src/ltlvisit/tostring.cc
View file

@ -35,7 +35,7 @@ namespace spot
{ {
public: public:
to_string_visitor(std::ostream& os = std::cout) to_string_visitor(std::ostream& os = std::cout)
: os_(os) : os_(os), top_level_(true)
{ {
} }
@ -69,10 +69,14 @@ namespace spot
void void
visit(const binop* bo) visit(const binop* bo)
{ {
os_ << "("; bool top_level = top_level_;
top_level_ = false;
if (!top_level)
os_ << "(";
bo->first()->accept(*this); bo->first()->accept(*this);
switch(bo->op()) switch (bo->op())
{ {
case binop::Xor: case binop::Xor:
os_ << " ^ "; os_ << " ^ ";
@ -92,7 +96,8 @@ namespace spot
} }
bo->second()->accept(*this); bo->second()->accept(*this);
os_ << ")"; if (!top_level)
os_ << ")";
} }
void void
@ -101,7 +106,7 @@ namespace spot
// The parser treats F0, F1, G0, G1, X0, and X1 as atomic // The parser treats F0, F1, G0, G1, X0, and X1 as atomic
// propositions. So make sure we output F(0), G(1), etc. // propositions. So make sure we output F(0), G(1), etc.
bool need_parent = !!dynamic_cast<const constant*>(uo->child()); bool need_parent = !!dynamic_cast<const constant*>(uo->child());
switch(uo->op()) switch (uo->op())
{ {
case unop::Not: case unop::Not:
os_ << "!"; os_ << "!";
@ -118,6 +123,7 @@ namespace spot
break; break;
} }
top_level_ = false;
if (need_parent) if (need_parent)
os_ << "("; os_ << "(";
uo->child()->accept(*this); uo->child()->accept(*this);
@ -128,7 +134,10 @@ namespace spot
void void
visit(const multop* mo) visit(const multop* mo)
{ {
os_ << "("; bool top_level = top_level_;
top_level_ = false;
if (!top_level)
os_ << "(";
unsigned max = mo->size(); unsigned max = mo->size();
mo->nth(0)->accept(*this); mo->nth(0)->accept(*this);
const char* ch = " "; const char* ch = " ";
@ -147,10 +156,12 @@ namespace spot
os_ << ch; os_ << ch;
mo->nth(n)->accept(*this); mo->nth(n)->accept(*this);
} }
os_ << ")"; if (!top_level)
os_ << ")";
} }
protected: protected:
std::ostream& os_; std::ostream& os_;
bool top_level_;
}; };
std::ostream& std::ostream&
@ -185,9 +196,12 @@ namespace spot
void void
visit(const binop* bo) visit(const binop* bo)
{ {
os_ << "("; bool top_level = top_level_;
top_level_ = false;
if (!top_level)
os_ << "(";
switch(bo->op()) switch (bo->op())
{ {
case binop::Xor: case binop::Xor:
os_ << "(!"; os_ << "(!";
@ -228,7 +242,8 @@ namespace spot
break; break;
} }
os_ << ")"; if (!top_level)
os_ << ")";
} }
void void
@ -237,7 +252,7 @@ namespace spot
// The parser treats X0, and X1 as atomic propositions. So // The parser treats X0, and X1 as atomic propositions. So
// make sure we output X(0) and X(1). // make sure we output X(0) and X(1).
bool need_parent = false; bool need_parent = false;
switch(uo->op()) switch (uo->op())
{ {
case unop::Not: case unop::Not:
os_ << "!"; os_ << "!";
@ -254,6 +269,7 @@ namespace spot
break; break;
} }
top_level_ = false;
if (need_parent) if (need_parent)
os_ << "("; os_ << "(";
uo->child()->accept(*this); uo->child()->accept(*this);
@ -264,7 +280,10 @@ namespace spot
void void
visit(const multop* mo) visit(const multop* mo)
{ {
os_ << "("; bool top_level = top_level_;
top_level_ = false;
if (!top_level)
os_ << "(";
unsigned max = mo->size(); unsigned max = mo->size();
mo->nth(0)->accept(*this); mo->nth(0)->accept(*this);
const char* ch = " "; const char* ch = " ";
@ -283,7 +302,8 @@ namespace spot
os_ << ch; os_ << ch;
mo->nth(n)->accept(*this); mo->nth(n)->accept(*this);
} }
os_ << ")"; if (!top_level)
os_ << ")";
} }
}; };

22
src/sanity/style.test
View file

@ -33,28 +33,28 @@ while read file; do
sed 's,//.*,,' < $file > $tmp sed 's,//.*,,' < $file > $tmp
grep ' if(' $tmp && grep '[ ]if(' $tmp &&
diag 'Missing space after "if"' diag 'Missing space after "if"'
grep ' if (.*).*{' $tmp && grep '[ ]if (.*).*{' $tmp &&
diag 'Opening { should be on its own line.' diag 'Opening { should be on its own line.'
grep ' while(' $tmp && grep '[ ]while(' $tmp &&
diag 'Missing space after "while"' diag 'Missing space after "while"'
grep ' while (.*).*{' $tmp && grep '[ ]while (.*).*{' $tmp &&
diag 'Opening { should be on its own line.' diag 'Opening { should be on its own line.'
grep ' for(' $tmp && grep '[ ]for(' $tmp &&
diag 'Missing space after "for"' diag 'Missing space after "for"'
grep ' for (.*).*{' $tmp && grep '[ ]for (.*).*{' $tmp &&
diag 'Opening { should be on its own line.' diag 'Opening { should be on its own line.'
grep ' switch(' $tmp && grep '[ ]switch(' $tmp &&
diag 'Missing space after "for"' diag 'Missing space after "switch"'
grep ' switch (.*).*{' $tmp && grep '[ ]switch (.*).*{' $tmp &&
diag 'Opening { should be on its own line.' diag 'Opening { should be on its own line.'
grep '( ' $tmp && grep '( ' $tmp &&
@ -69,10 +69,10 @@ while read file; do
grep ',[(a-zA-Z+=_!]' $tmp && grep ',[(a-zA-Z+=_!]' $tmp &&
diag 'Space after coma.' diag 'Space after coma.'
grep '[^ \t\n]&&[^ \t\n]' $tmp && grep '[^ ]&&[^ ]' $tmp &&
diag 'Space arround binary operators.' diag 'Space arround binary operators.'
grep '[^ \t\n]||[^ \t\n]' $tmp && grep '[^ ]||[^ ]' $tmp &&
diag 'Space arround binary operators.' diag 'Space arround binary operators.'
$fail && echo "$file" >>failures $fail && echo "$file" >>failures

2
src/tgbatest/explicit.test
View file

@ -38,7 +38,7 @@ digraph G {
2 [label="state 1"] 2 [label="state 1"]
2 -> 3 [label="a\n{Acc[r]}"] 2 -> 3 [label="a\n{Acc[r]}"]
3 [label="state 2"] 3 [label="state 2"]
3 -> 1 [label="(b & c)\n"] 3 -> 1 [label="b & c\n"]
} }
EOF EOF

6
src/tgbatest/explpro2.test
View file

@ -39,8 +39,8 @@ EOF
cat >expected <<EOF cat >expected <<EOF
acc = "p1" "p2" "p3"; acc = "p1" "p2" "p3";
"s1 * s1", "s2 * s2", "(!a & b)", "p1" "p2"; "s1 * s1", "s2 * s2", "!a & b", "p1" "p2";
"s1 * s1", "s3 * s3", "(a & !b)", "p2" "p3"; "s1 * s1", "s3 * s3", "a & !b", "p2" "p3";
EOF EOF
run 0 ./explprod input1 input2 > stdout run 0 ./explprod input1 input2 > stdout
@ -48,7 +48,7 @@ run 0 ./explprod input1 input2 > stdout
# Sort out some possible inversions in the output. # Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.) # (The order is not guaranteed by SPOT.)
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g; perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;
s/\(!b & a\)/(a & !b)/g;s/\(b & !a\)/(!a & b)/g' \ s/!b & a/a & !b/g;s/b & !a/!a & b/g' \
stdout > tmp_ && mv tmp_ stdout stdout > tmp_ && mv tmp_ stdout
cat stdout cat stdout

8
src/tgbatest/explpro3.test
View file

@ -39,16 +39,16 @@ EOF
cat >expected <<EOF cat >expected <<EOF
acc = "p2" "p3"; acc = "p2" "p3";
"s1 * s1", "s2 * s2", "(!a & b)", "p2"; "s1 * s1", "s2 * s2", "!a & b", "p2";
"s1 * s1", "s3 * s3", "(a & !b)", "p3"; "s1 * s1", "s3 * s3", "a & !b", "p3";
EOF EOF
run 0 ./explprod input1 input2 > stdout run 0 ./explprod input1 input2 > stdout
# Sort out some possible inversions in the output. # Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.) # (The order is not guaranteed by SPOT.)
sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g; sed 's/"p3" "p2"/"p2" "p3"/g;s/!b & a/a \& !b/g;
s/(b & !a)/(!a \& b)/g' stdout > tmp_ && mv tmp_ stdout s/b & !a/!a \& b/g' stdout > tmp_ && mv tmp_ stdout
cat stdout cat stdout
diff stdout expected diff stdout expected

6
src/tgbatest/explprod.test
View file

@ -41,16 +41,16 @@ EOF
cat >expected <<EOF cat >expected <<EOF
acc = "p1" "p2" "p3"; acc = "p1" "p2" "p3";
"s1 * s1", "s3 * s2", "(a & b)", "p1" "p2"; "s1 * s1", "s3 * s2", "a & b", "p1" "p2";
"s1 * s1", "s2 * s2", "b", "p1" "p2"; "s1 * s1", "s2 * s2", "b", "p1" "p2";
"s2 * s2", "s3 * s1", "(a & c)", "p1" "p3"; "s2 * s2", "s3 * s1", "a & c", "p1" "p3";
EOF EOF
run 0 ./explprod input1 input2 > stdout run 0 ./explprod input1 input2 > stdout
# Sort out some possible inversions in the output. # Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.) # (The order is not guaranteed by SPOT.)
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g; perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;
s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \ s/c & a/a & c/g;s/b & a/a & b/g' \
stdout > tmp_ && mv tmp_ stdout stdout > tmp_ && mv tmp_ stdout
cat stdout cat stdout

2
src/tgbatest/readsave.test
View file

@ -36,7 +36,7 @@ EOF
cat >expected <<\EOF cat >expected <<\EOF
acc = "c" "d"; acc = "c" "d";
"s1", "s2", "(a & !b)", "c" "d"; "s1", "s2", "a & !b", "c" "d";
"s2", "state 3", "\"F\\G\"", "c"; "s2", "state 3", "\"F\\G\"", "c";
"state 3", "s1", "1",; "state 3", "s1", "1",;
EOF EOF

2
src/tgbatest/tgbaread.test
View file

@ -39,7 +39,7 @@ digraph G {
0 [label="", style=invis, height=0] 0 [label="", style=invis, height=0]
0 -> 1 0 -> 1
1 [label="s1"] 1 [label="s1"]
1 -> 2 [label="(a & !b)\n{Acc[d], Acc[c]}"] 1 -> 2 [label="a & !b\n{Acc[d], Acc[c]}"]
2 [label="s2"] 2 [label="s2"]
2 -> 3 [label="a\n{Acc[c]}"] 2 -> 3 [label="a\n{Acc[c]}"]
3 [label="state 3"] 3 [label="state 3"]

12
src/tgbatest/tripprod.test
View file

@ -49,12 +49,12 @@ EOF
cat >expected <<EOF cat >expected <<EOF
acc = "p1" "p2" "p3" "p4"; acc = "p1" "p2" "p3" "p4";
"s1 * s1 * s1", "s3 * s2 * s2", "(a & b)", "p1" "p2"; "s1 * s1 * s1", "s3 * s2 * s2", "a & b", "p1" "p2";
"s1 * s1 * s1", "s2 * s2 * s2", "(a & b)", "p1" "p2"; "s1 * s1 * s1", "s2 * s2 * s2", "a & b", "p1" "p2";
"s1 * s1 * s1", "s3 * s2 * s3", "(a & b)", "p1" "p2"; "s1 * s1 * s1", "s3 * s2 * s3", "a & b", "p1" "p2";
"s1 * s1 * s1", "s2 * s2 * s3", "b", "p1" "p2"; "s1 * s1 * s1", "s2 * s2 * s3", "b", "p1" "p2";
"s2 * s2 * s2", "s3 * s1 * s3", "(a & c)", "p3" "p4"; "s2 * s2 * s2", "s3 * s1 * s3", "a & c", "p3" "p4";
"s2 * s2 * s3", "s3 * s1 * s2", "(a & c)", "p3" "p4"; "s2 * s2 * s3", "s3 * s1 * s2", "a & c", "p3" "p4";
EOF EOF
run 0 ./tripprod input1 input2 input3 > stdout run 0 ./tripprod input1 input2 input3 > stdout
@ -62,7 +62,7 @@ run 0 ./tripprod input1 input2 input3 > stdout
# Sort out some possible inversions in the output. # Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.) # (The order is not guaranteed by SPOT.)
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1,$2,$3,$4]}/g; perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1,$2,$3,$4]}/g;
s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \ s/c & a/a & c/g;s/b & a/a & b/g' \
stdout > tmp_ && stdout > tmp_ &&
mv tmp_ stdout mv tmp_ stdout