From 08abf1bffee76c4c44956c647131fdfeb4227d51 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 5 Apr 2014 20:05:39 +0000 Subject: [PATCH] Bug fix: pre-strategy generation check done before model construction. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8072 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 3e3049c8..3737f0cb 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2706,18 +2706,18 @@ public class Prism extends PrismComponent implements PrismSettingsListener setEngine(Prism.EXPLICIT); } } - // Compatibility check - if (genStrat && currentModelType.nondeterministic() && !getExplicit()) { - if (!((NondetModel) currentModel).areAllChoiceActionsUnique()) - throw new PrismException("Cannot generate strategies with the current engine " - + "because some state of the model do not have unique action labels for each choice. " - + "Either switch to the explicit engine or add more action labels to the model"); - } - try { // Build model, if necessary buildModelIfRequired(); + // Compatibility check + if (genStrat && currentModelType.nondeterministic() && !getExplicit()) { + if (!((NondetModel) currentModel).areAllChoiceActionsUnique()) + throw new PrismException("Cannot generate strategies with the current engine " + + "because some state of the model do not have unique action labels for each choice. " + + "Either switch to the explicit engine or add more action labels to the model"); + } + // Create new model checker object and do model checking if (!getExplicit()) { ModelChecker mc = createModelChecker(propertiesFile);