Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GraphConditions.cpp
Go to the documentation of this file.
1
2#include "GraphConditions.h"
3#include "storm/exceptions/NotImplementedException.h"
4#include "storm/exceptions/UnexpectedException.h"
5#include "storm/models/sparse/Ctmc.h"
6#include "storm/models/sparse/MarkovAutomaton.h"
7#include "storm/models/sparse/StandardRewardModel.h"
8#include "storm/utility/constants.h"
9
10namespace storm {
11namespace analysis {
12
13template<typename ValueType>
17
18template<typename ValueType>
19std::unordered_set<typename ConstraintType<ValueType>::val> const& ConstraintCollector<ValueType>::getWellformedConstraints() const {
20 return this->wellformedConstraintSet;
21}
22
23template<typename ValueType>
24std::unordered_set<typename ConstraintType<ValueType>::val> const& ConstraintCollector<ValueType>::getGraphPreservingConstraints() const {
25 return this->graphPreservingConstraintSet;
26}
27
28template<typename ValueType>
29std::set<storm::RationalFunctionVariable> const& ConstraintCollector<ValueType>::getVariables() const {
30 return this->variableSet;
31}
32
33template<typename ValueType>
34void ConstraintCollector<ValueType>::wellformedRequiresNonNegativeEntries(std::vector<ValueType> const& vec) {
35 for (auto const& entry : vec) {
36 if (!storm::utility::isConstant(entry)) {
37 auto const& transitionVars = entry.gatherVariables();
38 variableSet.insert(transitionVars.begin(), transitionVars.end());
39 if (entry.denominator().isConstant()) {
40 assert(entry.denominator().constantPart() != 0);
41 if (entry.denominator().constantPart() > 0) {
42 wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
43 } else if (entry.denominator().constantPart() < 0) {
44 wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
45 } else {
46 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before.");
47 }
48 } else {
49 wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
50 wellformedConstraintSet.emplace(
51 carl::FormulaType::ITE,
52 typename ConstraintType<ValueType>::val(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER),
53 typename ConstraintType<ValueType>::val(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ),
54 typename ConstraintType<ValueType>::val(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
55 }
56 }
57 }
58}
59
60template<typename ValueType>
61void ConstraintCollector<ValueType>::process(storm::models::sparse::Model<ValueType> const& model) {
62 if (model.getType() != storm::models::ModelType::Ctmc) {
63 for (uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
64 ValueType sum = storm::utility::zero<ValueType>();
65
66 for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
67 auto const& transition = *transitionIt;
68 sum += transition.getValue();
69 if (!storm::utility::isConstant(transition.getValue())) {
70 auto const& transitionVars = transition.getValue().gatherVariables();
71 variableSet.insert(transitionVars.begin(), transitionVars.end());
72 // Assert: 0 <= transition <= 1
73 if (transition.getValue().denominator().isConstant()) {
74 assert(transition.getValue().denominator().constantPart() != 0);
75 if (transition.getValue().denominator().constantPart() > 0) {
76 // Assert: nom <= denom
77 wellformedConstraintSet.emplace(
78 (transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(),
79 storm::CompareRelation::LEQ);
80 // Assert: nom >= 0
81 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
82 } else if (transition.getValue().denominator().constantPart() < 0) {
83 // Assert nom >= denom
84 wellformedConstraintSet.emplace(
85 (transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(),
86 storm::CompareRelation::GEQ);
87 // Assert: nom <= 0
88 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
89 } else {
90 STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
91 }
92 } else {
93 // Assert: denom != 0
94 wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
95 // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
96 wellformedConstraintSet.emplace(
97 carl::FormulaType::ITE,
98 typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(),
99 storm::CompareRelation::GREATER),
100 typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ),
101 typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(),
102 storm::CompareRelation::LEQ));
103 // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
104 }
105 // Assert: transition > 0
106 graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
107 }
108 }
109 STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
110 if (!storm::utility::isConstant(sum)) {
111 // Assert: sum == 1
112 wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
113 }
114 }
115 } else {
116 for (auto const& transition : model.getTransitionMatrix()) {
117 if (!transition.getValue().isConstant()) {
118 if (transition.getValue().denominator().isConstant()) {
119 assert(transition.getValue().denominator().constantPart() != 0);
120 if (transition.getValue().denominator().constantPart() > 0) {
121 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
122 } else if (transition.getValue().denominator().constantPart() < 0) {
123 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
124 } else {
125 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before.");
126 }
127 } else {
128 wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
129 wellformedConstraintSet.emplace(
130 carl::FormulaType::ITE,
131 typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(),
132 storm::CompareRelation::GREATER),
133 typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ),
134 typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
135 }
136 graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
137 }
138 }
139 }
140
141 if (model.getType() == storm::models::ModelType::Ctmc) {
142 auto const& exitRateVector = static_cast<storm::models::sparse::Ctmc<ValueType> const&>(model).getExitRateVector();
143 wellformedRequiresNonNegativeEntries(exitRateVector);
144 } else if (model.getType() == storm::models::ModelType::MarkovAutomaton) {
145 auto const& exitRateVector = static_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getExitRates();
146 wellformedRequiresNonNegativeEntries(exitRateVector);
147 }
148
149 for (auto const& rewModelEntry : model.getRewardModels()) {
150 if (rewModelEntry.second.hasStateRewards()) {
151 wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateRewardVector());
152 }
153 if (rewModelEntry.second.hasStateActionRewards()) {
154 wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateActionRewardVector());
155 }
156 if (rewModelEntry.second.hasTransitionRewards()) {
157 for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) {
158 if (!entry.getValue().isConstant()) {
159 if (entry.getValue().denominator().isConstant()) {
160 assert(entry.getValue().denominator().constantPart() != 0);
161 if (entry.getValue().denominator().constantPart() > 0) {
162 wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
163 } else if (entry.getValue().denominator().constantPart() < 0) {
164 wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
165 } else {
166 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before.");
167 }
168 } else {
169 wellformedConstraintSet.emplace(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
170 wellformedConstraintSet.emplace(
171 carl::FormulaType::ITE,
172 typename ConstraintType<ValueType>::val(entry.getValue().denominator().polynomialWithCoefficient(),
173 storm::CompareRelation::GREATER),
174 typename ConstraintType<ValueType>::val(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ),
175 typename ConstraintType<ValueType>::val(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
176 }
177 }
178 }
179 }
180 }
181}
182
183template<typename ValueType>
187
188template class ConstraintCollector<storm::RationalFunction>;
189} // namespace analysis
190} // namespace storm
storm::analysis::ConstraintCollector
Class to collect constraints on parametric Markov chains.
Definition GraphConditions.h:26
storm::analysis::ConstraintCollector::getWellformedConstraints
std::unordered_set< typename ConstraintType< ValueType >::val > const & getWellformedConstraints() const
Returns the set of wellformed-ness constraints.
Definition GraphConditions.cpp:19
storm::analysis::ConstraintCollector::getGraphPreservingConstraints
std::unordered_set< typename ConstraintType< ValueType >::val > const & getGraphPreservingConstraints() const
Returns the set of graph-preserving constraints.
Definition GraphConditions.cpp:24
storm::analysis::ConstraintCollector::ConstraintCollector
ConstraintCollector(storm::models::sparse::Model< ValueType > const &model)
Constructs a constraint collector for the given Model.
Definition GraphConditions.cpp:14
storm::analysis::ConstraintCollector::process
void process(storm::models::sparse::Model< ValueType > const &model)
Constructs the constraints for the given Model.
Definition GraphConditions.cpp:61
storm::analysis::ConstraintCollector::getVariables
std::set< storm::RationalFunctionVariable > const & getVariables() const
Returns the set of variables in the model.
Definition GraphConditions.cpp:29
storm::analysis::ConstraintCollector::operator()
void operator()(storm::models::sparse::Model< ValueType > const &model)
Constructs the constraints for the given Model by calling the process method.
Definition GraphConditions.cpp:184
storm::expressions::Expression::gatherVariables
void gatherVariables(std::set< storm::expressions::Variable > &variables) const
Retrieves the set of all variables that appear in the expression.
Definition Expression.cpp:136
storm::models::ModelBase::getType
virtual ModelType getType() const
Return the actual type of the model.
Definition ModelBase.cpp:7
storm::models::sparse::Ctmc
This class represents a continuous-time Markov chain.
Definition Ctmc.h:15
storm::models::sparse::MarkovAutomaton
This class represents a Markov automaton.
Definition MarkovAutomaton.h:16
storm::models::sparse::Model
Base class for all sparse models.
Definition Model.h:33
storm::models::sparse::Model::getTransitionMatrix
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:197
storm::models::sparse::Model::getRewardModels
std::unordered_map< std::string, RewardModelType > const & getRewardModels() const
Retrieves the reward models.
Definition Model.cpp:699
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
storm::utility::isOne
bool isOne(ValueType const &a)
Definition constants.cpp:36
storm::utility::isConstant
bool isConstant(ValueType const &)
Definition constants.cpp:66
storm
LabParser.cpp.
Definition cli.cpp:18
process
void process()
Definition storm-dft.cpp:238