From e9280393b2041af1233a570913411f6ebfcf06cb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 21 Apr 2008 10:21:20 +0000 Subject: [PATCH] Output of non-boolean results in verbose mode. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@763 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StateModelChecker.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 6d48fe2c..b1f5034c 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -217,6 +217,17 @@ public class StateModelChecker implements ModelChecker // Non-Boolean results else { + // If in "verbose" mode, print out results vector to log + if (verbose) { + mainLog.print("\nResults (non-zero only) for all states:"); + if (vals.getNNZ() > 0) { + mainLog.print("\n"); + vals.print(mainLog); + } else { + mainLog.print(" (none)\n"); + } + } + if (filter == null) { if (model.getNumStartStates() > 1) { mainLog.print("\nWarning: There are multiple initial states;");