From 280bb048685588d2db62c1b8fe9311e64e8f98e2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 17 Jan 2015 00:05:37 +0000 Subject: [PATCH] Initial states also exported by -exporttarget for multi-objective. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9529 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/MultiObjModelChecker.java | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index fc0d6171..64cd02c6 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -538,7 +538,6 @@ public class MultiObjModelChecker extends PrismComponent n = targets.size(); JDDNode labels[] = new JDDNode[n]; - String labelNames[] = new String[n]; // Build temporary DDs for combined targets for (i = 0; i < n; i++) { JDD.Ref(targets.get(i)); @@ -552,13 +551,21 @@ public class MultiObjModelChecker extends PrismComponent } } labels[i] = tmp; - labelNames[i] = "target" + i; } + // If required, export info about target states if (prism.getExportTarget()) { + JDDNode labels2[] = new JDDNode[n + 1]; + String labelNames[] = new String[n + 1]; + labels2[0] = modelProduct.getStart(); + labelNames[0] = "init"; + for (i = 0; i < n; i++) { + labels2[i + 1] = labels[i]; + labelNames[i + 1] = "target" + i; + } try { mainLog.print("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"..."); - PrismMTBDD.ExportLabels(labels, labelNames, "l", modelProduct.getAllDDRowVars(), modelProduct.getODD(), Prism.EXPORT_PLAIN, + PrismMTBDD.ExportLabels(labels2, labelNames, "l", modelProduct.getAllDDRowVars(), modelProduct.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename()); } catch (FileNotFoundException e) { mainLog.println("\nWarning: Could not export target to file \"" + prism.getExportTargetFilename() + "\"");