From 4e7233d9fadfde70a7bb3b114066d4873b520233 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 9 Mar 2010 15:23:42 +0100 Subject: [PATCH] Support braces in addition to parentheses in rational expressions. * src/ltlparse/ltlparse.yy (rationalexp): Allow bracedrationalexp. * src/ltltest/consterm.test, src/tgbatest/ltl2tgba.test: Add more tests. --- src/ltlparse/ltlparse.yy | 2 ++ src/ltltest/consterm.test | 1 + src/tgbatest/ltl2tgba.test | 2 +- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index c5da4b790..194457f35 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -234,6 +234,8 @@ booleanatom: ATOMIC_PROP rationalexp: booleanatom | CONST_EMPTYWORD { $$ = constant::empty_word_instance(); } + | bracedrationalexp + { $$ = $1; } | PAR_OPEN rationalexp PAR_CLOSE { $$ = $2; } | PAR_OPEN error PAR_CLOSE diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test index 2810a9d13..cb2e5fcb2 100755 --- a/src/ltltest/consterm.test +++ b/src/ltltest/consterm.test @@ -37,6 +37,7 @@ 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)' +run 1 ../consterm '{{a ; b} + {#e}} & {a* + b}' # test braces run 1 ../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)' diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 0b535b7e3..06fab7e81 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -66,7 +66,7 @@ check_psl '{((a*;b;c)*)&((b*;a;c)*)}<>->x' check_psl '{(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)' # try sub-braces check_psl '{(#e + a):c*:(#e + b)}<>->d' check_psl '{a;e;f:(g*);h}<>->d' check_psl '{(a:b)* & (c*:d)}<>->e'