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

acc: strengthen is_generalized_rabin() and is_generalized_streett()

Browse source 
* spot/twa/acc.cc: These functions were segfaulting on acceptance
conditions such as "Acceptance: 3 t" or "Acceptance: 3 f".
The issue was revealed on branch "next" by the change that print_dot()
display the acceptance condition by default, but we want the fix on
master as well.
* NEWS: Mention the issue.
This commit is contained in:
Alexandre Duret-Lutz 2018-03-10 20:30:14 +01:00
parent 057e67e7f6
commit 15fdac6059
2 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -11,6 +11,12 @@ New in spot 2.5.1.dev (not yet released)
update an external structure that references states of the twa update an external structure that references states of the twa
that we want to purge. that we want to purge.
Bugs fixed:
- acc_cond::is_generalized_rabin() and
acc_cond::is_generalized_streett() would segfault on weird
acceptance conditions such as "3 t" or "3 f".
New in spot 2.5.1 (2018-02-20) New in spot 2.5.1 (2018-02-20)
Library: Library:

10
spot/twa/acc.cc
View file

@ -660,7 +660,10 @@ namespace spot
pairs.resize(num_); pairs.resize(num_);
return true; return true;
} }
if (code_.is_t() // "Acceptance: 0 f" is caught by is_generalized_rabin() above.
// Therefore is_f() below catches "Acceptance: n f" with n>0.
if (code_.is_f()
|| code_.is_t()
|| code_.back().sub.op != acc_op::Or) || code_.back().sub.op != acc_op::Or)
return false; return false;
@ -741,7 +744,10 @@ namespace spot
pairs.resize(num_); pairs.resize(num_);
return true; return true;
} }
if (code_.is_f() // "Acceptance: 0 t" is caught by is_generalized_buchi() above.
// Therefore is_t() below catches "Acceptance: n t" with n>0.
if (code_.is_t()
|| code_.is_f()
|| code_.back().sub.op != acc_op::And) || code_.back().sub.op != acc_op::And)
return false; return false;