From b6df2a88c6bdad6ac44e6e40863a8afccdab5595 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 17 Apr 2020 11:11:35 +0100 Subject: [PATCH] Enable export of transient probability computation for MTBDD engine. Was already enabled for steady-state probabilities in 3cb4f42d, following addition of no-sparse printing for MTBDD vectors. Not sure why this was not enabled too. --- prism/src/prism/Prism.java | 4 ---- 1 file changed, 4 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 841fbc82..862af7c5 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3607,8 +3607,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); if (time < 0) throw new PrismException("Cannot compute transient probabilities for negative time value"); - if (fileOut != null && getEngine() == MTBDD) - throw new PrismException("Transient probability export only supported for sparse/hybrid engines"); if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; // no specific states format for MRMC if (exportType == EXPORT_ROWS) @@ -3704,8 +3702,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Do some checks if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC)) throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); - if (fileOut != null && getEngine() == MTBDD) - throw new PrismException("Transient probability export only supported for sparse/hybrid engines"); if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; // no specific states format for MRMC if (exportType == EXPORT_ROWS)