From f1fbd233769158b26fd1bd50835eddb8a3096604 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 25 Feb 2016 09:39:14 +0000 Subject: [PATCH] =?UTF-8?q?HOAF2DA:=20Fix=20handling=20of=20acceptance=20s?= =?UTF-8?q?ignatures=20[with=20David=20M=C3=BCller]?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- prism/src/automata/HOAF2DA.java | 1 + 1 file changed, 1 insertion(+) diff --git a/prism/src/automata/HOAF2DA.java b/prism/src/automata/HOAF2DA.java index 43024a1d..576d6ba5 100644 --- a/prism/src/automata/HOAF2DA.java +++ b/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) {