Browse Source

dont go on as soon as trivial command set is necessary

tempestpy_adaptions
Sebastian Junges 6 years ago
parent
commit
a34ca5c9ac
  1. 4
      src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

4
src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

@ -1776,6 +1776,10 @@ namespace storm {
break; break;
} }
if (commandSet.size() == nrCommands(symbolicModel)) {
result.push_back(commandSet);
break;
}
auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0)); auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0));
std::shared_ptr<storm::models::sparse::Model<T>> const& subModel = subChoiceOrigins.first; std::shared_ptr<storm::models::sparse::Model<T>> const& subModel = subChoiceOrigins.first;

Loading…
Cancel
Save