Browse Source

Allow -exportsteadystate with MTBDD engine

Now that non-sparse StateValueMTBDD printing is working, we can remove
this restriction.
accumulation-v4.7
Joachim Klein 7 years ago
parent
commit
3cb4f42ded
  1. 3
      prism/src/prism/Prism.java

3
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)

Loading…
Cancel
Save