diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index fb7b9e84a..bf3beeb0c 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -23,6 +23,12 @@ namespace storm { return this->graphPreservingConstraintSet; } + template + std::set const& ConstraintCollector::getVariables() const { + return this->variableSet; + } + + template void ConstraintCollector::wellformedRequiresNonNegativeEntries(std::vector const& vec) { for(auto const& entry : vec) { @@ -50,6 +56,8 @@ namespace storm { for (auto const& transition : dtmc.getRows(state)) { sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { + auto const& transitionVars = transition.getValue().gatherVariables(); + variableSet.insert(transitionVars.begin(), transitionVars.end()); // Assert: 0 <= transition <= 1 if (transition.getValue().denominator().isConstant()) { assert(transition.getValue().denominator().constantPart() != 0); diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index c6043fd5a..48b4aee64 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -31,6 +31,9 @@ namespace storm { // A set of constraints that makes sure that the underlying graph of the model does not change depending // on the parameter values. std::unordered_set::val> graphPreservingConstraintSet; + + // A set of variables + std::set variableSet; void wellformedRequiresNonNegativeEntries(std::vector const&); public: @@ -55,6 +58,12 @@ namespace storm { * @return The set of graph-preserving constraints. */ std::unordered_set::val> const& getGraphPreservingConstraints() const; + + /*! + * Returns the set of variables in the model + * @return + */ + std::set const& getVariables() const; /*! * Constructs the constraints for the given DTMC.