diff --git a/src/ltltest/length.test b/src/ltltest/length.test index 0a0cfc36b..f7893c1da 100755 --- a/src/ltltest/length.test +++ b/src/ltltest/length.test @@ -34,3 +34,5 @@ len 'a|b|c' 5 1 len '!a|b|!c' 7 1 len '!(!a|b|!c)' 8 1 len '!X(!a|b|!c)' 9 3 +len 'Xa|(b|c)' 6 4 +len 'Xa&(b|c)' 6 4 diff --git a/src/ltlvisit/length.cc b/src/ltlvisit/length.cc index 61af7206e..f22c45c3d 100644 --- a/src/ltlvisit/length.cc +++ b/src/ltlvisit/length.cc @@ -88,11 +88,27 @@ namespace spot } unsigned s = mo->size(); + unsigned operator_count = s - 1; for (unsigned i = 0; i < s; ++i) - mo->nth(i)->accept(*this); + { + // Ignore all boolean values. We only want to count them once. + if (!mo->nth(i)->is_boolean()) + mo->nth(i)->accept(*this); + else + --operator_count; + } + + // if operator_count has decreased, it means that we have encountered + // boolean values. + if (operator_count < s - 1) + { + ++result_; + ++operator_count; + } + // "a & b & c" should count for 5, even though it is // stored as And(a,b,c). - result_ += s - 1; + result_ += operator_count; } };