From aca617849bcd0c65accd7a6381f07e3c7f3b280c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 6 Oct 2011 15:45:08 +0000 Subject: [PATCH] Some optimisations for approximate model checking on models with deadlocks (could do other operators too). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3876 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/sampler/SamplerRewardInstCont.java | 6 ++++++ prism/src/simulator/sampler/SamplerRewardInstDisc.java | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/prism/src/simulator/sampler/SamplerRewardInstCont.java b/prism/src/simulator/sampler/SamplerRewardInstCont.java index 53e465cb..c069717c 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstCont.java +++ b/prism/src/simulator/sampler/SamplerRewardInstCont.java @@ -74,6 +74,12 @@ public class SamplerRewardInstCont extends SamplerDouble value = path.getCurrentStateReward(rewardStructIndex); } } + // Or, if we are now at a deadlock + else if (transList != null && transList.isDeadlock()) { + valueKnown = true; + value = path.getCurrentStateReward(rewardStructIndex); + } + // Otherwise, don't know return valueKnown; } diff --git a/prism/src/simulator/sampler/SamplerRewardInstDisc.java b/prism/src/simulator/sampler/SamplerRewardInstDisc.java index 8d22616f..dfb60b23 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardInstDisc.java @@ -66,6 +66,12 @@ public class SamplerRewardInstDisc extends SamplerDouble valueKnown = true; value = path.getCurrentStateReward(rewardStructIndex); } + // Or, if we are now at a deadlock + else if (transList != null && transList.isDeadlock()) { + valueKnown = true; + value = path.getCurrentStateReward(rewardStructIndex); + } + // Otherwise, don't know return valueKnown; }