Browse Source

HOAF2DA: Fix handling of acceptance signatures [with David Müller]

Parsing a HOA automaton, if a state has an acceptance signature that
contains an acceptance set that is not actually referenced in the
acceptance condition, we simply skip these entries, as they are not
relevant for acceptance.

This commit fixes the handling for this situation:

Acceptance: 2 Inf(0)
...
State: 1 {1}

I.e., when the acceptance set index is valid but larger than the
largest used one. Previously, would throw an IndexOutOfBoundsException
trying to access a non-existant set.



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11218 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
commit
f1fbd23376
  1. 1
      prism/src/automata/HOAF2DA.java

1
prism/src/automata/HOAF2DA.java

@ -420,6 +420,7 @@ public class HOAF2DA implements HOAConsumer {
for (int index : accSignature) {
if (index >= acceptanceSets.size()) {
// acceptance set index not used in acceptance condition, ignore
continue;
}
BitSet accSet = acceptanceSets.get(index);
if (accSet == null) {

Loading…
Cancel
Save