From 8d644f240d132cc9ff388c1cbf8232620403bd6b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 Nov 2013 00:25:08 +0000 Subject: [PATCH] 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 --- prism/src/prism/Prism.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 8e649263..2b9f66e4 100644 --- a/prism/src/prism/Prism.java +++ b/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