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