From ad519b85680a3493decad8731f74ae06f795a001 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 2 Mar 2010 12:44:46 +0100 Subject: [PATCH] Do not assume that concatenation cannot accept the empty word. For instance "(a+#e);(b+#e);(c*)" does. * src/ltlvisit/consterm.cc: Fix handling of Concat operator. * src/ltltest/consterm.test: Add more tests. --- src/ltltest/consterm.test | 3 +++ src/ltlvisit/consterm.cc | 10 +--------- 2 files changed, 4 insertions(+), 9 deletions(-) diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test index 9bab7b9b0..2810a9d13 100755 --- a/src/ltltest/consterm.test +++ b/src/ltltest/consterm.test @@ -37,3 +37,6 @@ 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 + #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/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc index 44fa95b0f..74b93e4e3 100644 --- a/src/ltlvisit/consterm.cc +++ b/src/ltlvisit/consterm.cc @@ -97,12 +97,6 @@ namespace spot void visit(const multop* mo) { - if (mo->op() == multop::Concat) - { - result_ = false; - return; - } - unsigned max = mo->size(); // This sets the initial value of result_. mo->nth(0)->accept(*this); @@ -119,13 +113,11 @@ namespace spot return; break; case multop::And: + case multop::Concat: result_ &= r; if (!result_) return; break; - case multop::Concat: - assert(!"unreachable code"); - break; } } }