From f33dea0f43bb5ca39886bfbf2259f80b68ec1934 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 18 Sep 2017 14:43:55 +0200 Subject: [PATCH] Interval iteration: Only print max finite value if it actually exists --- prism/src/explicit/DTMCModelChecker.java | 4 +++- prism/src/explicit/MDPModelChecker.java | 4 +++- prism/src/prism/NondetModelChecker.java | 4 +++- prism/src/prism/ProbModelChecker.java | 4 +++- 4 files changed, 12 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index aa8f9b39..7e33180c 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -2137,7 +2137,9 @@ public class DTMCModelChecker extends ProbModelChecker } double max_v = PrismUtils.findMaxFinite(rv.soln, unknownStates.iterator()); - mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + if (max_v != Double.NEGATIVE_INFINITY) { + mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + } return rv; } diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index b187fb1a..5f4696b1 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -2508,7 +2508,9 @@ public class MDPModelChecker extends ProbModelChecker } double max_v = PrismUtils.findMaxFinite(rv.soln, unknownStates.iterator()); - mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + if (max_v != Double.NEGATIVE_INFINITY) { + mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + } return rv; } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index d983aae7..c1a6b446 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -2567,7 +2567,9 @@ public class NondetModelChecker extends NonProbModelChecker if (doIntervalIteration) { double max_v = rewards.maxFiniteOverBDD(maybe); - mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + if (max_v != Double.NEGATIVE_INFINITY) { + mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + } } // derefs diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 6f6d8fe0..71305916 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -2363,7 +2363,9 @@ public class ProbModelChecker extends NonProbModelChecker if (doIntervalIteration) { double max_v = rewards.maxFiniteOverBDD(maybe); - mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + if (max_v != Double.NEGATIVE_INFINITY) { + mainLog.println("Maximum finite value in solution vector at end of interval iteration: " + max_v); + } } // derefs