Browse Source

collect variables during collection of constraints

tempestpy_adaptions
Sebastian Junges 7 years ago
parent
commit
ca3b475ce5
  1. 8
      src/storm/analysis/GraphConditions.cpp
  2. 9
      src/storm/analysis/GraphConditions.h

8
src/storm/analysis/GraphConditions.cpp

@ -23,6 +23,12 @@ namespace storm {
return this->graphPreservingConstraintSet;
}
template <typename ValueType>
std::set<storm::RationalFunctionVariable> const& ConstraintCollector<ValueType>::getVariables() const {
return this->variableSet;
}
template <typename ValueType>
void ConstraintCollector<ValueType>::wellformedRequiresNonNegativeEntries(std::vector<ValueType> 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);

9
src/storm/analysis/GraphConditions.h

@ -32,6 +32,9 @@ namespace storm {
// on the parameter values.
std::unordered_set<typename ConstraintType<ValueType>::val> graphPreservingConstraintSet;
// A set of variables
std::set<storm::RationalFunctionVariable> variableSet;
void wellformedRequiresNonNegativeEntries(std::vector<ValueType> const&);
public:
/*!
@ -56,6 +59,12 @@ namespace storm {
*/
std::unordered_set<typename ConstraintType<ValueType>::val> const& getGraphPreservingConstraints() const;
/*!
* Returns the set of variables in the model
* @return
*/
std::set<storm::RationalFunctionVariable> const& getVariables() const;
/*!
* Constructs the constraints for the given DTMC.
*

Loading…
Cancel
Save