From 8f942729185ae738eba2df530da63d798302f585 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 14 Dec 2009 14:00:52 +0000 Subject: [PATCH] Code tidy: NondetModelChecker. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1642 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 471145e5..54f5bc6e 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -942,19 +942,21 @@ public class NondetModelChecker extends NonProbModelChecker JDDNode probsMTBDD; DoubleVector probsDV; StateProbs probs = null; - + // If required, export info about target states if (prism.getExportTarget()) { JDDNode labels[] = { model.getStart(), b2 }; String labelNames[] = { "init", "target" }; try { mainLog.print("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); - PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename()); + PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), + Prism.EXPORT_PLAIN, prism.getExportTargetFilename()); } catch (FileNotFoundException e) { - mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\""); + mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + + "\""); } } - + // compute yes/no/maybe states if (b2.equals(JDD.ZERO)) { yes = JDD.Constant(0); @@ -1029,8 +1031,8 @@ public class NondetModelChecker extends NonProbModelChecker probs = new StateProbsMTBDD(probsMTBDD, model); break; case Prism.SPARSE: - probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, - min); + probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, + allDDNondetVars, yes, maybe, min); probs = new StateProbsDV(probsDV, model); break; case Prism.HYBRID: