diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java index 850f1c30..718840b8 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java @@ -135,6 +135,12 @@ public class SamplerBoundedUntilCont extends SamplerBoolean value = true; } } + // Or, if we are now at a deadlock + else if (transList != null && transList.isDeadlock()) { + valueKnown = true; + value = false; + } + // Otherwise, don't know } } diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java index b182ba8c..43c61616 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java @@ -87,11 +87,16 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean valueKnown = true; value = true; } - // Or, if not, have we violated the LJS of the until? + // Or, if not, have we violated the LHS of the until? else if (!left.evaluateBoolean(currentState)) { valueKnown = true; value = false; } + // Or, if we are now at a deadlock + else if (transList != null && transList.isDeadlock()) { + valueKnown = true; + value = false; + } // Otherwise, don't know } diff --git a/prism/src/simulator/sampler/SamplerRewardCumulCont.java b/prism/src/simulator/sampler/SamplerRewardCumulCont.java index d2508ca4..a48e3378 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulCont.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulCont.java @@ -79,6 +79,14 @@ public class SamplerRewardCumulCont extends SamplerDouble value -= path.getPreviousTransitionReward(rewardStructIndex); } } + // Or, if we are now at a deadlock + else if (transList != null && transList.isDeadlock()) { + valueKnown = true; + value = path.getTotalCumulativeReward(rewardStructIndex); + // Compute remaining time, i.e. how long left until time bound will be reached + double remainingTime = timeBound - path.getTotalTime(); + value += path.getCurrentStateReward(rewardStructIndex) * remainingTime; + } return valueKnown; }