From c6df34232c0b284c8911592257ccb364c7dae526 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 17:33:07 +0000 Subject: [PATCH] DTMC total reward, explicit: fix output glitch git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12148 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 6f8d241c..14239627 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -382,8 +382,8 @@ public class DTMCModelChecker extends ProbModelChecker } } } - mainLog.print("States in non-zero reward BSCCs: " + bsccsNonZero.cardinality()); - + mainLog.print("States in non-zero reward BSCCs: " + bsccsNonZero.cardinality() + "\n"); + // Find states with infinite reward (those reach a non-zero reward BSCC with prob > 0) BitSet inf; if (preRel) { @@ -396,7 +396,7 @@ public class DTMCModelChecker extends ProbModelChecker } inf.flip(0, n); int numInf = inf.cardinality(); - mainLog.println(", inf=" + numInf + ", maybe=" + (n - numInf)); + mainLog.println("inf=" + numInf + ", maybe=" + (n - numInf)); // Compute rewards // (do this using the functions for "reward reachability" properties but with no targets)