diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index edd17c3d0..aea47fd09 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1552,7 +1552,79 @@ namespace storm { storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); return Program(manager, this->getModelType(), this->getConstants(), std::vector(), std::vector(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true); } - + + std::vector Program::usedConstants() const { + std::unordered_set vars; + for(auto const& m : this->modules) { + for(auto const& c : m.getCommands()) { + auto const& found_gex = c.getGuardExpression().getVariables(); + vars.insert(found_gex.begin(), found_gex.end()); + for (auto const& u : c.getUpdates()) { + auto const& found_lex = u.getLikelihoodExpression().getVariables(); + vars.insert(found_lex.begin(), found_lex.end()); + for (auto const& a : u.getAssignments()) { + auto const& found_ass = a.getExpression().getVariables(); + vars.insert(found_ass.begin(), found_ass.end()); + } + } + } + for (auto const& v : m.getBooleanVariables()) { + if (v.hasInitialValue()) { + auto const& found_def = v.getInitialValueExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + for (auto const& v : m.getIntegerVariables()) { + if (v.hasInitialValue()) { + auto const& found_def = v.getInitialValueExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + } + + for (auto const& f : this->formulas) { + auto const& found_def = f.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + + for (auto const& v : this->constants) { + if (v.isDefined()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + for (auto const& v : this->globalBooleanVariables) { + if (v.hasInitialValue()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + for (auto const& v : this->globalIntegerVariables) { + if (v.hasInitialValue()) { + auto const& found_def = v.getExpression().getVariables(); + vars.insert(found_def.begin(), found_def.end()); + } + } + + + std::unordered_set varIndices; + for (auto const& v : vars) { + varIndices.insert(v.getIndex()); + } + + std::vector usedConstants; + for(auto const& c : this->constants) { + if (varIndices.count(c.getExpressionVariable().getIndex())) { + usedConstants.push_back(c); + } + } + + return usedConstants; + + } + std::unordered_map Program::buildCommandIndexToActionNameMap() const { std::unordered_map res; for(auto const& m : this->modules) { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 46d704803..7dedc6667 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -151,6 +151,12 @@ namespace storm { * @return The number of constants defined in the program. */ std::size_t getNumberOfConstants() const; + + /*! + * Retrieves the constants that are actually used in the program. + * @return + */ + std::vector usedConstants() const; /*! * Retrieves whether a global Boolean variable with the given name exists