From 33a7f2c9e8adb671dd3fc0ca682a0bb68924464d Mon Sep 17 00:00:00 2001 From: Ernst Moritz Hahn Date: Wed, 27 Aug 2014 13:24:09 +0000 Subject: [PATCH] fixed computation of lost probability to take into account probability mass intentionally destroyed git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9138 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/FastAdaptiveUniformisation.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java index eccc8d25..a8ebddf2 100644 --- a/prism/src/explicit/FastAdaptiveUniformisation.java +++ b/prism/src/explicit/FastAdaptiveUniformisation.java @@ -77,7 +77,7 @@ import prism.Model; /** * Implementation of fast adaptive uniformisation (FAU). */ -public class FastAdaptiveUniformisation extends PrismComponent +public final class FastAdaptiveUniformisation extends PrismComponent { /** * Stores properties of states needed for fast adaptive method. @@ -457,7 +457,9 @@ public class FastAdaptiveUniformisation extends PrismComponent private AnalysisType analysisType; /** total loss of probability in discrete-time process */ private double totalProbLoss; - + /** probability mass intentionally set to zero */ + private double totalProbSetZero; + /** * Constructor. */ @@ -1096,6 +1098,8 @@ public class FastAdaptiveUniformisation extends PrismComponent for (StateProp prop : states.values()) { totalProb += prop.getSum(); } + totalProb += totalProbSetZero; + totalProbLoss = 1.0 - totalProb; } @@ -1123,6 +1127,7 @@ public class FastAdaptiveUniformisation extends PrismComponent Expression evSink = sink.deepCopy(); evSink = (Expression) evSink.expandLabels(specialLabels); if (evSink.evaluateBoolean(constantValues, state)) { + totalProbSetZero += prop.getProb(); prop.setProb(0.0); } }