Browse Source

Don't do strategy generation with symbolic engines if there are duplicate actions.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7605 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
commit
8d644f240d
  1. 7
      prism/src/prism/Prism.java

7
prism/src/prism/Prism.java

@ -2679,6 +2679,13 @@ 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

Loading…
Cancel
Save