From 1ec571a1c8f18fc6a24fac411f0879fe493d4db2 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 18 Sep 2017 14:43:56 +0200 Subject: [PATCH] explicit interval iteration: skip upper bound computation if there are no unknown states --- prism/src/explicit/DTMCModelChecker.java | 5 +++++ prism/src/explicit/MDPModelChecker.java | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 7e33180c..d689a759 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -1345,6 +1345,11 @@ public class DTMCModelChecker extends ProbModelChecker */ double computeReachRewardsUpperBound(DTMC dtmc, MCRewards mcRewards, BitSet target, BitSet unknown, BitSet inf) throws PrismException { + if (unknown.isEmpty()) { + mainLog.println("Skipping upper bound computation, no unknown states..."); + return 0; + } + // inf and target states become trap states (with self-loops) BitSet trapStates = (BitSet) target.clone(); trapStates.or(inf); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 5f4696b1..8b01a24f 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -1414,6 +1414,11 @@ public class MDPModelChecker extends ProbModelChecker */ double computeReachRewardsMaxUpperBound(MDP mdp, MDPRewards mdpRewards, BitSet target, BitSet unknown, BitSet inf) throws PrismException { + if (unknown.isEmpty()) { + mainLog.println("Skipping upper bound computation, no unknown states..."); + return 0; + } + // inf and target states become trap states (with dropped choices) BitSet trapStates = (BitSet) target.clone(); trapStates.or(inf);