Browse Source

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
master
Dave Parker 12 years ago
parent
commit
08abf1bffe
  1. 8
      prism/src/prism/Prism.java

8
prism/src/prism/Prism.java

@ -2706,6 +2706,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
setEngine(Prism.EXPLICIT); setEngine(Prism.EXPLICIT);
} }
} }
try {
// Build model, if necessary
buildModelIfRequired();
// Compatibility check // Compatibility check
if (genStrat && currentModelType.nondeterministic() && !getExplicit()) { if (genStrat && currentModelType.nondeterministic() && !getExplicit()) {
if (!((NondetModel) currentModel).areAllChoiceActionsUnique()) if (!((NondetModel) currentModel).areAllChoiceActionsUnique())
@ -2714,10 +2718,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
+ "Either switch to the explicit engine or add more action labels to the model"); + "Either switch to the explicit engine or add more action labels to the model");
} }
try {
// Build model, if necessary
buildModelIfRequired();
// Create new model checker object and do model checking // Create new model checker object and do model checking
if (!getExplicit()) { if (!getExplicit()) {
ModelChecker mc = createModelChecker(propertiesFile); ModelChecker mc = createModelChecker(propertiesFile);

Loading…
Cancel
Save