From 3cb4f42dedfe9b953be286e4216d5d600fe0a621 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Sat, 27 Apr 2019 08:28:52 +0200 Subject: [PATCH] Allow -exportsteadystate with MTBDD engine Now that non-sparse StateValueMTBDD printing is working, we can remove this restriction. --- prism/src/prism/Prism.java | 3 --- 1 file changed, 3 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index b8f10076..be250def 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3367,9 +3367,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) - // TODO: auto-switch? - throw new PrismException("Steady-state probability export not supported for MTBDD engine"); if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; // no specific states format for MRMC if (exportType == EXPORT_ROWS)