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

Support braces in addition to parentheses in rational expressions.

Browse source 
* src/ltlparse/ltlparse.yy (rationalexp): Allow bracedrationalexp.
* src/ltltest/consterm.test, src/tgbatest/ltl2tgba.test: Add more
tests.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-09 15:23:42 +01:00
parent 2f8c4ac8b7
commit 4e7233d9fa
3 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ltlparse/ltlparse.yy
View file

@ -234,6 +234,8 @@ booleanatom: ATOMIC_PROP
rationalexp: booleanatom rationalexp: booleanatom
| CONST_EMPTYWORD | CONST_EMPTYWORD
{ $$ = constant::empty_word_instance(); } { $$ = constant::empty_word_instance(); }
| bracedrationalexp
{ $$ = $1; }
| PAR_OPEN rationalexp PAR_CLOSE | PAR_OPEN rationalexp PAR_CLOSE
{ $$ = $2; } { $$ = $2; }
| PAR_OPEN error PAR_CLOSE | PAR_OPEN error PAR_CLOSE

1
src/ltltest/consterm.test
View file

@ -37,6 +37,7 @@ run 1 ../consterm '((a ; b) + #e)'
run 0 ../consterm '((a ; b) + #e) & e' run 0 ../consterm '((a ; b) + #e) & e'
run 1 ../consterm '((a ; b) + #e) & #e' run 1 ../consterm '((a ; b) + #e) & #e'
run 1 ../consterm '((a ; b) + #e) & (a* + b)' run 1 ../consterm '((a ; b) + #e) & (a* + b)'
run 1 ../consterm '{{a ; b} + {#e}} & {a* + b}' # test braces
run 1 ../consterm '(a + #e);(b + #e);(c + #e)' run 1 ../consterm '(a + #e);(b + #e);(c + #e)'
run 0 ../consterm '(a + #e);(b + e);(c + #e)' run 0 ../consterm '(a + #e);(b + e);(c + #e)'
run 1 ../consterm '(a + #e);(b + e)*;(c + #e)' run 1 ../consterm '(a + #e);(b + e)*;(c + #e)'

2
src/tgbatest/ltl2tgba.test
View file

@ -66,7 +66,7 @@ check_psl '{((a*;b;c)*)&((b*;a;c)*)}<>->x'
check_psl '{(g;y;r)*}<>->x' check_psl '{(g;y;r)*}<>->x'
check_psl 'G({(g;y;r)*}<>->x)' check_psl 'G({(g;y;r)*}<>->x)'
check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)' check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)'
check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)' check_psl 'G({{a;b}*}[]->x)&G({{c;d}*}[]->y)' # try sub-braces
check_psl '{(#e + a):c*:(#e + b)}<>->d' check_psl '{(#e + a):c*:(#e + b)}<>->d'
check_psl '{a;e;f:(g*);h}<>->d' check_psl '{a;e;f:(g*);h}<>->d'
check_psl '{(a:b)* & (c*:d)}<>->e' check_psl '{(a:b)* & (c*:d)}<>->e'