From 98c019b1750cba307054da43ff4135912ea65e9e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 6 Dec 2018 13:20:42 +0100 Subject: [PATCH] Automatically switch to MTBDD engine before model checking if hybrid/sparse engine can not handle state space If, after model building with hybrid or sparse engine, we detect that the configured engine can definitely not handle the model (i.e., if number of states is larger than Integer.MAX_VALUE), we auto-switch to the MTBDD engine. --- prism/src/prism/Prism.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 423cfd08..3776d1ef 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2953,6 +2953,17 @@ public class Prism extends PrismComponent implements PrismSettingsListener + "Either switch to the explicit engine or add more action labels to the model"); } + if (!getExplicit() && !engineSwitch) { + // check if we need to switch to MTBDD engine + long n = currentModel.getNumStates(); + if (n == -1 || n > Integer.MAX_VALUE) { + mainLog.printWarning("Switching to MTBDD engine, as number of states is too large for " + engineStrings[getEngine()] + " engine."); + engineSwitch = true; + lastEngine = getEngine(); + setEngine(Prism.MTBDD); + } + } + // Create new model checker object and do model checking if (!getExplicit()) { ModelChecker mc = createModelChecker(propertiesFile);