|
|
|
@ -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: |
|
|
|
|