Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
stateelimination.cpp
Go to the documentation of this file.
1#include "storm/utility/stateelimination.h"
2
3#include <random>
4
5#include "storm/solver/stateelimination/DynamicStatePriorityQueue.h"
6#include "storm/solver/stateelimination/StatePriorityQueue.h"
7#include "storm/solver/stateelimination/StaticStatePriorityQueue.h"
8
9#include "storm/storage/BitVector.h"
10#include "storm/storage/FlexibleSparseMatrix.h"
11
12#include "storm/settings/SettingsManager.h"
13
14#include "storm/adapters/RationalFunctionAdapter.h"
15#include "storm/exceptions/InvalidSettingsException.h"
16#include "storm/exceptions/InvalidStateException.h"
17#include "storm/utility/constants.h"
18#include "storm/utility/graph.h"
19#include "storm/utility/macros.h"
20
21namespace storm {
22namespace utility {
23namespace stateelimination {
24
31
36
41
47
51
52template<typename ValueType>
53uint_fast64_t estimateComplexity(ValueType const&) {
54 return 1;
55}
56
57#ifdef STORM_HAVE_CARL
58template<>
59uint_fast64_t estimateComplexity(storm::RationalFunction const& value) {
60 if (storm::utility::isConstant(value)) {
61 return 1;
62 }
63 if (value.denominator().isConstant()) {
64 return value.nominator().complexity();
65 } else {
66 return value.denominator().complexity() * value.nominator().complexity();
67 }
68}
69#endif
70
71template<typename ValueType>
72uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix,
73 storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions,
74 std::vector<ValueType> const& oneStepProbabilities) {
75 uint_fast64_t penalty = 0;
76 bool hasParametricSelfLoop = false;
77
78 for (auto const& predecessor : backwardTransitions.getRow(state)) {
79 for (auto const& successor : transitionMatrix.getRow(state)) {
80 penalty += estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue());
81 }
82 if (predecessor.getColumn() == state) {
83 hasParametricSelfLoop = !storm::utility::isConstant(predecessor.getValue());
84 }
85 penalty += estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) *
86 estimateComplexity(oneStepProbabilities[state]);
87 }
88
89 // If it is a self-loop that is parametric, we increase the penalty a lot.
90 if (hasParametricSelfLoop) {
91 penalty *= 10;
92 }
93
94 return penalty;
95}
96
97template<typename ValueType>
98uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state,
99 storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix,
100 storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const&) {
101 return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size();
102}
103
104template<typename ValueType>
105std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities,
106 storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix,
107 storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions,
108 std::vector<ValueType> const& oneStepProbabilities, storm::storage::BitVector const& states) {
109 STORM_LOG_TRACE("Creating state priority queue for states " << states);
110
111 // Get the settings to customize the priority queue.
112 storm::settings::modules::EliminationSettings::EliminationOrder order =
113 storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder();
114
115 std::vector<storm::storage::sparse::state_type> sortedStates(states.begin(), states.end());
116
117 if (order == storm::settings::modules::EliminationSettings::EliminationOrder::Random) {
118 std::random_device randomDevice;
119 std::mt19937 generator(randomDevice());
120 std::shuffle(sortedStates.begin(), sortedStates.end(), generator);
121 return std::make_unique<StaticStatePriorityQueue>(sortedStates);
122 } else {
123 if (eliminationOrderNeedsDistances(order)) {
124 STORM_LOG_THROW(static_cast<bool>(distanceBasedStatePriorities), storm::exceptions::InvalidStateException,
125 "Unable to build state priority queue without distance-based priorities.");
126 std::sort(sortedStates.begin(), sortedStates.end(),
127 [&distanceBasedStatePriorities](storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) {
128 return distanceBasedStatePriorities.get()[state1] < distanceBasedStatePriorities.get()[state2];
129 });
130 return std::make_unique<StaticStatePriorityQueue>(sortedStates);
131 } else if (eliminationOrderIsPenaltyBased(order)) {
132 std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> statePenalties(sortedStates.size());
133 typename DynamicStatePriorityQueue<ValueType>::PenaltyFunctionType penaltyFunction =
134 order == storm::settings::modules::EliminationSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression<ValueType>
135 : computeStatePenalty<ValueType>;
136 for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) {
137 statePenalties[index] =
138 std::make_pair(sortedStates[index], penaltyFunction(sortedStates[index], transitionMatrix, backwardTransitions, oneStepProbabilities));
139 }
140
141 std::sort(
142 statePenalties.begin(), statePenalties.end(),
143 [](std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& statePenalty1,
144 std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& statePenalty2) { return statePenalty1.second < statePenalty2.second; });
145
146 if (eliminationOrderIsStatic(order)) {
147 // For the static penalty version, we need to strip the penalties to create the queue.
148 for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) {
149 sortedStates[index] = statePenalties[index].first;
150 }
151 return std::make_unique<StaticStatePriorityQueue>(sortedStates);
152 } else {
153 // For the dynamic penalty version, we need to give the full state-penalty pairs.
154 return std::make_unique<DynamicStatePriorityQueue<ValueType>>(statePenalties, transitionMatrix, backwardTransitions, oneStepProbabilities,
155 penaltyFunction);
156 }
157 }
158 }
159 STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Illegal elimination order selected.");
160}
161
162std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(storm::storage::BitVector const& states) {
163 std::vector<storm::storage::sparse::state_type> sortedStates(states.begin(), states.end());
164 return std::make_shared<StaticStatePriorityQueue>(sortedStates);
165}
166
167std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(std::vector<storm::storage::sparse::state_type> const& states) {
168 return std::make_shared<StaticStatePriorityQueue>(states);
169}
170
171template<typename ValueType>
172std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
173 storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed,
174 storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities,
175 bool forward, bool reverse) {
176 std::vector<uint_fast64_t> statePriorities(transitionMatrix.getRowCount());
177 std::vector<storm::storage::sparse::state_type> states(transitionMatrix.getRowCount());
178 for (std::size_t index = 0; index < states.size(); ++index) {
179 states[index] = index;
180 }
181
182 std::vector<uint_fast64_t> distances =
183 getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities,
184 storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() ==
185 storm::settings::modules::EliminationSettings::EliminationOrder::Forward ||
186 storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() ==
187 storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed);
188
189 // In case of the forward or backward ordering, we can sort the states according to the distances.
190 if (forward ^ reverse) {
191 std::sort(states.begin(), states.end(),
192 [&distances](storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) {
193 return distances[state1] < distances[state2];
194 });
195 } else {
196 // Otherwise, we sort them according to descending distances.
197 std::sort(states.begin(), states.end(),
198 [&distances](storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) {
199 return distances[state1] > distances[state2];
200 });
201 }
202
203 // Now convert the ordering of the states to priorities.
204 for (uint_fast64_t index = 0; index < states.size(); ++index) {
205 statePriorities[states[index]] = index;
206 }
207
208 return statePriorities;
209}
210
211template<typename ValueType>
212std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
213 storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed,
214 storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities, bool forward) {
215 if (forward) {
216 return storm::utility::graph::getDistances(transitionMatrix, initialStates);
217 } else {
218 // Since the target states were eliminated from the matrix already, we construct a replacement by
219 // treating all states that have some non-zero probability to go to a target state in one step as target
220 // states.
221 storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount());
222 for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) {
223 if (oneStepProbabilities[index] != storm::utility::zero<ValueType>()) {
224 pseudoTargetStates.set(index);
225 }
226 }
227
228 return storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates);
229 }
230}
231
232template uint_fast64_t estimateComplexity(double const& value);
233template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities,
234 storm::storage::FlexibleSparseMatrix<double> const& transitionMatrix,
235 storm::storage::FlexibleSparseMatrix<double> const& backwardTransitions,
236 std::vector<double> const& oneStepProbabilities, storm::storage::BitVector const& states);
237template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state,
238 storm::storage::FlexibleSparseMatrix<double> const& transitionMatrix,
239 storm::storage::FlexibleSparseMatrix<double> const& backwardTransitions,
240 std::vector<double> const& oneStepProbabilities);
241template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state,
242 storm::storage::FlexibleSparseMatrix<double> const& transitionMatrix,
243 storm::storage::FlexibleSparseMatrix<double> const& backwardTransitions,
244 std::vector<double> const& oneStepProbabilities);
245template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<double> const& transitionMatrix,
246 storm::storage::SparseMatrix<double> const& transitionMatrixTransposed,
247 storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities,
248 bool forward, bool reverse);
249template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<double> const& transitionMatrix,
250 storm::storage::SparseMatrix<double> const& transitionMatrixTransposed,
251 storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities,
252 bool forward);
253
254#ifdef STORM_HAVE_CARL
255template uint_fast64_t estimateComplexity(storm::RationalNumber const& value);
256template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities,
257 storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix,
258 storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions,
259 std::vector<storm::RationalNumber> const& oneStepProbabilities,
260 storm::storage::BitVector const& states);
261template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state,
262 storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix,
263 storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions,
264 std::vector<storm::RationalNumber> const& oneStepProbabilities);
265template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state,
266 storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix,
267 storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions,
268 std::vector<storm::RationalNumber> const& oneStepProbabilities);
269template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix,
270 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed,
271 storm::storage::BitVector const& initialStates,
272 std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward, bool reverse);
273template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix,
274 storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed,
275 storm::storage::BitVector const& initialStates,
276 std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward);
277
278template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities,
279 storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix,
280 storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions,
281 std::vector<storm::RationalFunction> const& oneStepProbabilities,
282 storm::storage::BitVector const& states);
283template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state,
284 storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix,
285 storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions,
286 std::vector<storm::RationalFunction> const& oneStepProbabilities);
287template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state,
288 storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix,
289 storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions,
290 std::vector<storm::RationalFunction> const& oneStepProbabilities);
291template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix,
292 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed,
293 storm::storage::BitVector const& initialStates,
294 std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward, bool reverse);
295template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix,
296 storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed,
297 storm::storage::BitVector const& initialStates,
298 std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward);
299#endif
300} // namespace stateelimination
301} // namespace utility
302} // namespace storm
storm::settings::modules::EliminationSettings::EliminationOrder
EliminationOrder
An enum that contains all available state elimination orders.
Definition EliminationSettings.h:18
storm::solver::stateelimination::DynamicStatePriorityQueue::PenaltyFunctionType
std::function< uint_fast64_t(storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &oneStepProbabilities)> PenaltyFunctionType
Definition DynamicStatePriorityQueue.h:32
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::storage::BitVector::end
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
Definition BitVector.cpp:747
storm::storage::BitVector::set
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
Definition BitVector.cpp:242
storm::storage::BitVector::begin
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
Definition BitVector.cpp:739
storm::storage::FlexibleSparseMatrix
The flexible sparse matrix is used during state elimination.
Definition FlexibleSparseMatrix.h:21
storm::storage::FlexibleSparseMatrix::getRow
row_type & getRow(index_type)
Returns an object representing the given row.
Definition FlexibleSparseMatrix.cpp:71
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:328
storm::storage::SparseMatrix::getRowCount
index_type getRowCount() const
Returns the number of rows of the matrix.
Definition SparseMatrix.cpp:661
STORM_LOG_TRACE
#define STORM_LOG_TRACE(message)
Definition logging.h:12
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
storm::utility::graph::getDistances
std::vector< uint_fast64_t > getDistances(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, boost::optional< storm::storage::BitVector > const &subsystem)
Performs a breadth-first search through the underlying graph structure to compute the distance from a...
Definition graph.cpp:287
storm::utility::stateelimination::createStatePriorityQueue
std::shared_ptr< StatePriorityQueue > createStatePriorityQueue(boost::optional< std::vector< uint_fast64_t > > const &distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &oneStepProbabilities, storm::storage::BitVector const &states)
Definition stateelimination.cpp:105
storm::utility::stateelimination::computeStatePenalty
uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &oneStepProbabilities)
Definition stateelimination.cpp:72
storm::utility::stateelimination::getStateDistances
std::vector< uint_fast64_t > getStateDistances(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &transitionMatrixTransposed, storm::storage::BitVector const &initialStates, std::vector< ValueType > const &oneStepProbabilities, bool forward)
Definition stateelimination.cpp:212
storm::utility::stateelimination::eliminationOrderIsStatic
bool eliminationOrderIsStatic(storm::settings::modules::EliminationSettings::EliminationOrder const &order)
Definition stateelimination.cpp:48
storm::utility::stateelimination::eliminationOrderNeedsForwardDistances
bool eliminationOrderNeedsForwardDistances(storm::settings::modules::EliminationSettings::EliminationOrder const &order)
Definition stateelimination.cpp:32
storm::utility::stateelimination::computeStatePenaltyRegularExpression
uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const &state, storm::storage::FlexibleSparseMatrix< ValueType > const &transitionMatrix, storm::storage::FlexibleSparseMatrix< ValueType > const &backwardTransitions, std::vector< ValueType > const &)
Definition stateelimination.cpp:98
storm::utility::stateelimination::estimateComplexity
uint_fast64_t estimateComplexity(ValueType const &)
Definition stateelimination.cpp:53
storm::utility::stateelimination::eliminationOrderNeedsDistances
bool eliminationOrderNeedsDistances(storm::settings::modules::EliminationSettings::EliminationOrder const &order)
Definition stateelimination.cpp:25
storm::utility::stateelimination::getDistanceBasedPriorities
std::vector< uint_fast64_t > getDistanceBasedPriorities(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &transitionMatrixTransposed, storm::storage::BitVector const &initialStates, std::vector< ValueType > const &oneStepProbabilities, bool forward, bool reverse)
Definition stateelimination.cpp:172
storm::utility::stateelimination::eliminationOrderNeedsReversedDistances
bool eliminationOrderNeedsReversedDistances(storm::settings::modules::EliminationSettings::EliminationOrder const &order)
Definition stateelimination.cpp:37
storm::utility::stateelimination::eliminationOrderIsPenaltyBased
bool eliminationOrderIsPenaltyBased(storm::settings::modules::EliminationSettings::EliminationOrder const &order)
Definition stateelimination.cpp:42
storm::utility::isConstant
bool isConstant(ValueType const &)
Definition constants.cpp:102