diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index c991d88a1..53ee395f9 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -2121,7 +2121,11 @@ namespace storm { if (symbolicModel.isPrismProgram()) { - return std::make_shared<HighLevelCounterexample>(symbolicModel.asPrismProgram().restrictCommands(labelSets[0])); + storm::prism::Program program = symbolicModel.asPrismProgram().restrictCommands(labelSets[0]); + if(formula->isProbabilityOperatorFormula()) { + program.removeRewardModels(); + } + return std::make_shared<HighLevelCounterexample>(program); } else { STORM_LOG_ASSERT(symbolicModel.isJaniModel(), "Unknown symbolic model description type."); return std::make_shared<HighLevelCounterexample>(symbolicModel.asJaniModel().restrictEdges(labelSets[0])); diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index db45f503e..49381ca8e 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -732,6 +732,11 @@ namespace storm { STORM_LOG_THROW(it != this->labels.end(), storm::exceptions::InvalidArgumentException, "Canno remove unknown label '" << name << "'."); this->labels.erase(it); } + + void Program::removeRewardModels() { + this->rewardModels.clear(); + this->rewardModelToIndexMap.clear(); + } void Program::filterLabels(std::set<std::string> const& labelSet) { std::vector<storm::prism::Label> newLabels; diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index e00d36e32..502cd2a46 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -575,6 +575,8 @@ namespace storm { */ void filterLabels(std::set<std::string> const& labelSet); + void removeRewardModels(); + /*! * Retrieves all observation labels that are defined by this program *