From e4d1d0c10c8e0fd8a85df15bff98f0ce3cf3ff95 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 16 Apr 2011 18:27:07 +0000 Subject: [PATCH] =?UTF-8?q?Bugfix=20in=20simulator:=20Wrong=20answers=20fo?= =?UTF-8?q?r=20R=3D=3F[C<=3Dt]=20properties=20on=20CTMCs.?= git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2778 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/sampler/SamplerRewardCumulCont.java | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/prism/src/simulator/sampler/SamplerRewardCumulCont.java b/prism/src/simulator/sampler/SamplerRewardCumulCont.java index fdf8f91c..dc657660 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulCont.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulCont.java @@ -66,16 +66,15 @@ public class SamplerRewardCumulCont extends SamplerDouble valueKnown = true; value = path.getTotalCumulativeReward(rewardStructIndex); // Compute excess time, i.e. how long ago time bound was reached - double excessTime = timeBound - path.getTotalTime(); + double excessTime = path.getTotalTime() - timeBound; // If this is > 0 (very likely, unless time bound = 0), - // need to subtract reward accumulated in excess time - // (i.e. fraction of previous state reward, and transition reward) + // need to subtract reward accumulated in excess time and transition reward // Note that this cannot be the case for the first state of path, // so the call to getTimeInPreviousState() is safe. if (excessTime > 0) { // Note: Time so far > 0 so cannot be first state, // so safe to look at previous state. - value -= path.getPreviousStateReward(rewardStructIndex) * (excessTime / path.getTimeInPreviousState()); + value -= path.getPreviousStateReward(rewardStructIndex) * excessTime; value -= path.getPreviousTransitionReward(rewardStructIndex); } }