From 9f4a6dba5fd95f396be58d1d78690e2ad1152ec6 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 7 Jan 2015 13:19:59 +0000 Subject: [PATCH] LTL explicit engine bug fix (from Joachim Klein). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9501 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 02dfaf07..b91e85ca 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -355,9 +355,11 @@ public class LTLModelChecker extends PrismComponent BitSet result = new BitSet(); for (BitSet bscc : bsccs) { - boolean isLEmpty = true; - boolean isKEmpty = true; - for (int acceptancePair = 0; acceptancePair < numAcceptancePairs && isLEmpty && isKEmpty; acceptancePair++) { + for (int acceptancePair = 0; acceptancePair < numAcceptancePairs; acceptancePair++) { + // accepting for L,K <=> BSCC does not intersect L but does intersect K + boolean isLEmpty = true; + boolean isKEmpty = true; + BitSet L = dra.getAcceptanceL(acceptancePair); BitSet K = dra.getAcceptanceK(acceptancePair); for (int state = bscc.nextSetBit(0); state != -1; state = bscc.nextSetBit(state + 1)) { @@ -365,9 +367,10 @@ public class LTLModelChecker extends PrismComponent isLEmpty &= !L.get(draState); isKEmpty &= !K.get(draState); } - // Stop as soon as we find the first acceptance pair that is satisfied if (isLEmpty && !isKEmpty) { + // this BSCC is accepting result.or(bscc); + // we do not have to consider the other acceptance pairs, continue with next BSCC break; } }