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

more tests for rational operator simplifications.

Browse source 
* src/ltltest/nenoform.test, src/ltltest/equals.test,
src/ltltest/consterm.test: Update tests for rational ops.
* src/ltltest/consterm.cc: Use parse_ratexp().
* src/ltlast/binop.cc: Fix simplification rules for []-> and
<>->.
This commit is contained in:
Alexandre Duret-Lutz 2010-02-08 12:48:15 +01:00
parent 9aebb80e08
commit fc7c2943de
5 changed files with 42 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ltlast/binop.cc
View file

@ -258,17 +258,24 @@ namespace spot
case EConcat:
// - 0 <>-> Exp = 0
// - 1 <>-> Exp = Exp
if (first == constant::false_instance())
return second;
// - Exp <>-> 0 = 0
if (first == constant::true_instance())
return second;
if (first == constant::false_instance())
{
second->destroy();
return first;
}
if (second == constant::false_instance())
{
first->destroy();
return second;
}
break;
case UConcat:
// - 0 []-> Exp = 1
// - 1 []-> Exp = Exp
// - Exp []-> 1 = 1
if (first == constant::false_instance())
return constant::true_instance();
if (first == constant::true_instance())
@ -276,6 +283,11 @@ namespace spot
second->destroy();
return first;
}
if (second == constant::true_instance())
{
first->destroy();
return second;
}
break;
}

2
src/ltltest/consterm.cc
View file

@ -39,7 +39,7 @@ main(int argc, char **argv)
syntax(argv[0]);
spot::ltl::parse_error_list p1;
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
spot::ltl::formula* f1 = spot::ltl::parse_ratexp(argv[1], p1);
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
return 2;

11
src/ltltest/consterm.test
View file

@ -32,9 +32,8 @@ run 0 ../consterm '0'
run 1 ../consterm '#e'
run 1 ../consterm 'a*'
run 1 ../consterm '0*'
run 0 ../consterm '!#e'
run 0 ../consterm '((a U b) + c)'
run 1 ../consterm '((a U b) + #e)'
run 0 ../consterm '((a U b) + #e) & e'
run 1 ../consterm '((a U b) + #e) & #e'
run 1 ../consterm '((a U b) + #e) & (a* + b)'
run 0 ../consterm '((a ; b) + c)'
run 1 ../consterm '((a ; b) + #e)'
run 0 ../consterm '((a ; b) + #e) & e'
run 1 ../consterm '((a ; b) + #e) & #e'
run 1 ../consterm '((a ; b) + #e) & (a* + b)'

34
src/ltltest/equals.test
View file

@ -70,17 +70,19 @@ run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a'
run 0 ../equals 'FFG__GFF' 'F(F(G("__GFF")))'
# Trivial simplifications
run 0 ../equals '0*' '#e'
run 0 ../equals '#e*' '#e'
run 0 ../equals 'Exp**' 'Exp*'
run 0 ../equals '{0*}<>->a' '{#e}<>->a'
run 0 ../equals '{#e*}<>->a' '{#e}<>->a'
run 0 ../equals '{Exp**}<>->a' '{Exp*}<>->a'
run 0 ../equals 'FF(Exp)' 'F(Exp)'
run 0 ../equals 'GG(Exp)' 'G(Exp)'
run 0 ../equals 'F(0)' '0'
run 0 ../equals 'G(0)' '0'
run 0 ../equals 'F(1)' '1'
run 0 ../equals 'G(1)' '1'
run 0 ../equals 'F(#e)' '1'
run 0 ../equals 'G(#e)' '1'
run 0 ../equals 'F({#e}<>->1)' 'F({#e}<>->1)'
run 0 ../equals 'G({#e}<>->1)' 'G({#e}<>->1)'
run 0 ../equals 'F({1}<>->1)' '1'
run 0 ../equals 'G({1}<>->1)' '1'
run 0 ../equals '!1' '0'
run 0 ../equals '!0' '1'
run 0 ../equals '!!Exp' 'Exp'
@ -105,12 +107,16 @@ run 0 ../equals GGx Gx
run 0 ../equals GGGGGx Gx
run 0 ../equals '!!x' x
run 0 ../equals '!!!!!x' '!x'
run 0 ../equals '#e;x' x
run 0 ../equals 'x;#e' x
run 0 ../equals '#e;x;#e;#e' x
run 0 ../equals '#e;x;#e;x;#e' 'x;x'
run 0 ../equals 'x;x;x;#e;x;x' 'x;x;x;x;x'
run 0 ../equals 'x;0;x;x;x' '0'
run 0 ../equals '0*' '#e'
run 0 ../equals '#e*' '#e'
run 0 ../equals 'x;x;FF(0)' '0'
run 0 ../equals '{#e;x}<>->1' '{x}<>->1'
run 0 ../equals '{x;#e}<>->1' '{x}<>-> 1'
run 0 ../equals '{#e;x;#e;#e}<>->1' '{x}<>->1'
run 0 ../equals '{#e;x;#e;x;#e}<>->1' '{x;x}<>->1'
run 0 ../equals '{x;x;x;#e;x;x}<>->1' '{x;x;x;x;x}<>->1'
run 0 ../equals '{x;0;x;x;x}<>->1' '0'
run 0 ../equals '{x;0;x;x;x}[]->1' '1'
run 0 ../equals '{0*;1}<>->x' 'x'
run 0 ../equals '{#e*;1}<>->x' 'x'
run 0 ../equals '{x;x}<>->FF(0)' '0'
run 0 ../equals '{x;x}<>->GX(1)' '{x;x}<>->1'
run 0 ../equals '{x;x}[]->GX(1)' '1'
run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0'

5
src/ltltest/nenoform.test
View file

@ -68,6 +68,5 @@ run 0 ../nenoform '!(a U (!b U ((a & b & c) R d)))' \
run 0 ../nenoform '!(GF a => FG b)' 'GFa & GF!b'
# Rational operators
run 0 ../nenoform '!(X((!Xa)*))' 'X!((X!a)*)'
run 0 ../nenoform 'X((Xa)*)' 'X((Xa)*)'
run 0 ../nenoform '!F!X!(GF(a);!FG(a);x)' 'GX!(GFa;GF!a;x)'
run 0 ../nenoform '!X{a;b}<>->Fx' 'X{a;b}[]->G!x'
run 0 ../nenoform '!F({a*}<>->{b*}<>->c)' 'G({a*}[]->{b*}[]->!c)'