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);