From fd53ce813ceb317d62d773f96f2d0514a3936f30 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 30 Aug 2012 21:46:40 +0000 Subject: [PATCH] Refactor (symbolic) steady-state computation for S operator. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5620 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ProbModelChecker.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 5bfc48ba..eee6d202 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -384,7 +384,7 @@ public class ProbModelChecker extends NonProbModelChecker // If every state is in a BSCC, it's much easier... if (notInBSCCs.equals(JDD.ZERO)) { - mainLog.println("\nAll states are in a BSCC (so no reachability probabilities computed)"); + mainLog.println("\nAll states are in BSCCs (so no reachability probabilities computed)"); // There are more efficient ways to do this if we just create the solution BDD directly // But we actually build the prob vector so it can be printed out if necessary tmp = JDD.Constant(0); @@ -432,7 +432,7 @@ public class ProbModelChecker extends NonProbModelChecker } } - // Print out probabilities + // print out probabilities if (verbose) { mainLog.print("\nS operator probabilities: \n"); totalProbs.print(mainLog); @@ -940,7 +940,7 @@ public class ProbModelChecker extends NonProbModelChecker // if every state is in a bscc, it's much easier... if (notInBSCCs.equals(JDD.ZERO)) { - mainLog.println("\nAll states are in a BSCC (so no reachability probabilities computed)"); + mainLog.println("\nAll states are in BSCCs (so no reachability probabilities computed)"); // build the reward vector tmp = JDD.Constant(0);