length_boolone: fix inconsistency
* src/ltlvisit/length.cc: Consider length of all Boolean expressions combined in a multop as one. * src/ltltest/length.test: Test it.
This commit is contained in:
parent
b6e5ce7e15
commit
02334867da
2 changed files with 20 additions and 2 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue