Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
HybridCtmcCslHelper.cpp
Go to the documentation of this file.
1#include "storm/modelchecker/csl/helper/HybridCtmcCslHelper.h"
2
3#include "storm/adapters/RationalFunctionAdapter.h"
4#include "storm/environment/solver/TimeBoundedSolverEnvironment.h"
5#include "storm/exceptions/InvalidPropertyException.h"
6#include "storm/exceptions/InvalidStateException.h"
7#include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
8#include "storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h"
9#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
10#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
11#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
12#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
13#include "storm/models/symbolic/StandardRewardModel.h"
14#include "storm/storage/dd/Add.h"
15#include "storm/storage/dd/Bdd.h"
16#include "storm/storage/dd/DdManager.h"
17#include "storm/utility/Stopwatch.h"
18#include "storm/utility/constants.h"
19#include "storm/utility/graph.h"
20#include "storm/utility/macros.h"
21
22namespace storm {
23namespace modelchecker {
24namespace helper {
25
26template<storm::dd::DdType DdType, class ValueType>
27std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
28 Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix,
29 storm::dd::Add<DdType, ValueType> const& exitRateVector, typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel,
30 storm::dd::Bdd<DdType> const& targetStates, bool qualitative) {
31 return HybridDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(env, model, computeProbabilityMatrix(rateMatrix, exitRateVector),
32 rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative);
33}
34
35template<storm::dd::DdType DdType, class ValueType>
36std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(Environment const& env,
37 storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
38 storm::dd::Add<DdType, ValueType> const& rateMatrix,
39 storm::dd::Add<DdType, ValueType> const& exitRateVector,
40 storm::dd::Bdd<DdType> const& nextStates) {
41 return HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(env, model, computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates);
42}
43
44template<storm::dd::DdType DdType, class ValueType>
45std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeUntilProbabilities(Environment const& env,
46 storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
47 storm::dd::Add<DdType, ValueType> const& rateMatrix,
48 storm::dd::Add<DdType, ValueType> const& exitRateVector,
49 storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates,
50 bool qualitative) {
51 return HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(env, model, computeProbabilityMatrix(rateMatrix, exitRateVector), phiStates,
52 psiStates, qualitative);
53}
54
55template<storm::dd::DdType DdType, typename ValueType>
56 requires storm::NumberTraits<ValueType>::SupportsExponential
57std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeBoundedUntilProbabilities(
58 Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, bool onlyInitialStatesRelevant,
59 storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, storm::dd::Bdd<DdType> const& phiStates,
60 storm::dd::Bdd<DdType> const& psiStates, bool qualitative, ValueType lowerBound, std::optional<ValueType> const& upperBound) {
61 // If the time bounds are [0, inf], we rather call untimed reachability.
62 if (storm::utility::isZero(lowerBound) && !upperBound) {
63 return computeUntilProbabilities(env, model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative);
64 }
65
66 if (env.solver().isForceSoundness() && env.solver().timeBounded().getRelativeTerminationCriterion()) {
67 // Forward this query to the sparse engine
68 storm::utility::Stopwatch conversionWatch(true);
69 storm::dd::Odd odd = model.getReachableStates().createOdd();
70 storm::storage::SparseMatrix<ValueType> explicitRateMatrix = rateMatrix.toMatrix(odd, odd);
71 std::vector<ValueType> explicitExitRateVector = exitRateVector.toVector(odd);
72 storm::solver::SolveGoal<ValueType> goal;
73 if (onlyInitialStatesRelevant) {
74 goal.setRelevantValues(model.getInitialStates().toVector(odd));
75 }
76 conversionWatch.stop();
77 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
78
79 std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities<ValueType>(
80 env, std::move(goal), explicitRateMatrix, explicitRateMatrix.transpose(true), phiStates.toVector(odd), psiStates.toVector(odd),
81 explicitExitRateVector, qualitative, lowerBound, upperBound);
82
83 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(
84 model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(),
85 std::move(odd), std::move(result)));
86 }
87
88 // Set the possible (absolute) error allowed for truncation (epsilon for fox-glynn)
89 ValueType epsilon = storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getPrecision()) / 8.0;
90
91 // From this point on, we know that we have to solve a more complicated problem [t, t'] with either t != 0
92 // or t' != inf.
93
94 // If we identify the states that have probability 0 of reaching the target states, we can exclude them from the
95 // further computations.
96 storm::dd::Bdd<DdType> statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, rateMatrix.notZero(), phiStates, psiStates);
97 STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNonZeroCount() << " states with probability greater 0.");
98 storm::dd::Bdd<DdType> statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 && !psiStates;
99 STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNonZeroCount() << " 'maybe' states.");
100
101 if (!statesWithProbabilityGreater0NonPsi.isZero()) {
102 if (upperBound && storm::utility::isZero(*upperBound)) {
103 // In this case, the interval is of the form [0, 0].
104 return std::unique_ptr<CheckResult>(
105 new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), psiStates.template toAdd<ValueType>()));
106 } else {
107 if (storm::utility::isZero(lowerBound)) {
108 // In this case, the interval is of the form [0, t].
109 // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier.
110
111 // Find the maximal rate of all 'maybe' states to take it as the uniformization rate.
112 ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * exitRateVector).getMax();
113 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
114
115 // Compute the uniformized matrix.
116 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
117 computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate);
118
119 // Compute the vector that is to be added as a compensation for removing the absorbing states.
120 storm::dd::Add<DdType, ValueType> b = (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * rateMatrix *
121 psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>())
122 .sumAbstract(model.getColumnVariables()) /
123 model.getManager().getConstant(uniformizationRate);
124
125 storm::utility::Stopwatch conversionWatch(true);
126
127 // Create an ODD for the translation to an explicit representation.
128 storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd();
129
130 // Convert the symbolic parts to their explicit representation.
131 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
132 std::vector<ValueType> explicitB = b.toVector(odd);
133 conversionWatch.stop();
134 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
135
136 // Finally compute the transient probabilities.
137 std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
138 std::vector<ValueType> subresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(
139 env, explicitUniformizedMatrix, &explicitB, *upperBound, uniformizationRate, values, epsilon);
140
141 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(
142 model.getReachableStates(), (psiStates || !statesWithProbabilityGreater0) && model.getReachableStates(),
143 psiStates.template toAdd<ValueType>(), statesWithProbabilityGreater0NonPsi, odd, subresult));
144 } else if (!upperBound) {
145 // In this case, the interval is of the form [t, inf] with t != 0.
146
147 // Start by computing the (unbounded) reachability probabilities of reaching psi states while
148 // staying in phi states.
149 std::unique_ptr<CheckResult> unboundedResult =
150 computeUntilProbabilities(env, model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative);
151
152 // Compute the set of relevant states.
153 storm::dd::Bdd<DdType> relevantStates = statesWithProbabilityGreater0 && phiStates;
154
155 // Filter the unbounded result such that it only contains values for the relevant states.
156 unboundedResult->filter(SymbolicQualitativeCheckResult<DdType>(model.getReachableStates(), relevantStates));
157
158 storm::utility::Stopwatch conversionWatch;
159
160 // Build an ODD for the relevant states.
161 conversionWatch.start();
162 storm::dd::Odd odd = relevantStates.createOdd();
163 conversionWatch.stop();
164
165 std::vector<ValueType> result;
166 if (unboundedResult->isHybridQuantitativeCheckResult()) {
167 conversionWatch.start();
168 std::unique_ptr<CheckResult> explicitUnboundedResult =
169 unboundedResult->asHybridQuantitativeCheckResult<DdType, ValueType>().toExplicitQuantitativeCheckResult();
170 conversionWatch.stop();
171 // getValueVector() hands out ExtendedValueType<ValueType>, which is ValueType only because bounded until is instantiated for
172 // double alone: RationalNumber has no SupportsExponential.
173 result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
174 } else {
175 STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException,
176 "Expected check result of different type.");
177 result = unboundedResult->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().toVector(odd);
178 }
179
180 // Determine the uniformization rate for the transient probability computation.
181 ValueType uniformizationRate = 1.02 * (relevantStates.template toAdd<ValueType>() * exitRateVector).getMax();
182
183 // Compute the uniformized matrix.
184 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
185 computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate);
186 conversionWatch.start();
187 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
188 conversionWatch.stop();
189 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
190
191 // Compute the transient probabilities.
192 result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(
193 env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result, epsilon);
194
195 return std::unique_ptr<CheckResult>(
196 new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), !relevantStates && model.getReachableStates(),
197 model.getManager().template getAddZero<ValueType>(), relevantStates, odd, result));
198 } else {
199 // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf.
200
201 if (lowerBound != *upperBound) {
202 // In this case, the interval is of the form [t, t'] with t != 0, t' != inf and t != t'.
203
204 // Find the maximal rate of all 'maybe' states to take it as the uniformization rate.
205 ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * exitRateVector).getMax();
206 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
207
208 // Compute the (first) uniformized matrix.
209 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
210 computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate);
211
212 // Create the one-step vector.
213 storm::dd::Add<DdType, ValueType> b = (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * rateMatrix *
214 psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>())
215 .sumAbstract(model.getColumnVariables()) /
216 model.getManager().getConstant(uniformizationRate);
217
218 // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation.
219 storm::utility::Stopwatch conversionWatch(true);
220 storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd();
221 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
222 std::vector<ValueType> explicitB = b.toVector(odd);
223 conversionWatch.stop();
224
225 // Compute the transient probabilities.
226 std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
227 std::vector<ValueType> subResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(
228 env, explicitUniformizedMatrix, &explicitB, *upperBound - lowerBound, uniformizationRate, values, epsilon);
229
230 // Transform the explicit result to a hybrid check result, so we can easily convert it to
231 // a symbolic qualitative format.
232 HybridQuantitativeCheckResult<DdType> hybridResult(
233 model.getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && model.getReachableStates()),
234 psiStates.template toAdd<ValueType>(), statesWithProbabilityGreater0NonPsi, odd, subResult);
235
236 // Compute the set of relevant states.
237 storm::dd::Bdd<DdType> relevantStates = statesWithProbabilityGreater0 && phiStates;
238
239 // Filter the unbounded result such that it only contains values for the relevant states.
240 hybridResult.filter(SymbolicQualitativeCheckResult<DdType>(model.getReachableStates(), relevantStates));
241
242 // Build an ODD for the relevant states.
243 conversionWatch.start();
244 odd = relevantStates.createOdd();
245
246 std::unique_ptr<CheckResult> explicitResult = hybridResult.toExplicitQuantitativeCheckResult();
247 conversionWatch.stop();
248 // getValueVector() hands out ExtendedValueType<ValueType>, which is ValueType only because bounded until is instantiated for
249 // double alone: RationalNumber has no SupportsExponential.
250 std::vector<ValueType> newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
251
252 // Then compute the transient probabilities of being in such a state after t time units. For this,
253 // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
254 uniformizationRate = 1.02 * (relevantStates.template toAdd<ValueType>() * exitRateVector).getMax();
255 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
256
257 // If the lower and upper bounds coincide, we have only determined the relevant states at this
258 // point, but we still need to construct the starting vector.
259 if (lowerBound == *upperBound) {
260 odd = relevantStates.createOdd();
261 newSubresult = psiStates.template toAdd<ValueType>().toVector(odd);
262 }
263
264 // Finally, we compute the second set of transient probabilities.
265 uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate);
266 conversionWatch.start();
267 explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
268 conversionWatch.stop();
269 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
270
271 newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(
272 env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, epsilon);
273
274 return std::unique_ptr<CheckResult>(
275 new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), !relevantStates && model.getReachableStates(),
276 model.getManager().template getAddZero<ValueType>(), relevantStates, odd, newSubresult));
277 } else {
278 // In this case, the interval is of the form [t, t] with t != 0, t != inf.
279
280 storm::utility::Stopwatch conversionWatch;
281
282 // Build an ODD for the relevant states.
283 conversionWatch.start();
284 storm::dd::Odd odd = statesWithProbabilityGreater0.createOdd();
285
286 std::vector<ValueType> newSubresult = psiStates.template toAdd<ValueType>().toVector(odd);
287 conversionWatch.stop();
288
289 // Then compute the transient probabilities of being in such a state after t time units. For this,
290 // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
291 ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0.template toAdd<ValueType>() * exitRateVector).getMax();
292 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
293
294 // Finally, we compute the second set of transient probabilities.
295 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
296 computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate);
297 conversionWatch.start();
298 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
299 conversionWatch.stop();
300 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
301
302 newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(
303 env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, epsilon);
304
305 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(
306 model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(),
307 model.getManager().template getAddZero<ValueType>(), statesWithProbabilityGreater0, odd, newSubresult));
308 }
309 }
310 }
311 } else {
312 return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), psiStates.template toAdd<ValueType>()));
313 }
314}
315
316template<storm::dd::DdType DdType, typename ValueType>
317 requires storm::NumberTraits<ValueType>::SupportsExponential
318std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeInstantaneousRewards(
319 Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, bool onlyInitialStatesRelevant,
320 storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector,
321 typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel, ValueType timeBound) {
322 // Only compute the result if the model has a state-based reward model.
323 STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException,
324 "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0.");
325
326 storm::utility::Stopwatch conversionWatch;
327
328 // Create ODD for the translation.
329 conversionWatch.start();
330 storm::dd::Odd odd = model.getReachableStates().createOdd();
331 conversionWatch.stop();
332
333 // Initialize result to state rewards of the model.
334 auto rewardsAdd = rewardModel.getStateRewardVector();
335 std::vector<ValueType> result = rewardsAdd.toVector(odd);
336 ValueType maxValue = std::max(rewardsAdd.getMax(), -rewardsAdd.getMin());
337
338 // If the rewards are not zero and the time-bound is not zero, we need to perform a transient analysis.
339 if (!storm::utility::isZero(maxValue) && timeBound > 0) {
340 ValueType uniformizationRate = 1.02 * exitRateVector.getMax();
341 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
342
343 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
344 computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate);
345
346 conversionWatch.start();
347 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
348 conversionWatch.stop();
349 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
350
351 // Set the possible error allowed for truncation (epsilon for fox-glynn)
352 ValueType epsilon = storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getPrecision());
353 if (env.solver().timeBounded().getRelativeTerminationCriterion()) {
354 // Be more precise, if the maximum value is very small (This still gives no sound guarantee!)
355 epsilon *= std::min(storm::utility::one<ValueType>(), maxValue);
356 } else {
357 // Be more precise, if the maximal possible value is very large
358 epsilon /= std::max(storm::utility::one<ValueType>(), maxValue);
359 }
360
361 storm::storage::BitVector relevantValues;
362 if (onlyInitialStatesRelevant) {
363 relevantValues = model.getInitialStates().toVector(odd);
364 } else {
365 relevantValues = storm::storage::BitVector(result.size(), true);
366 }
367
368 // Loop until the desired precision is reached.
369 do {
370 result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(env, explicitUniformizedMatrix, nullptr,
371 timeBound, uniformizationRate, result, epsilon);
372 } while (storm::modelchecker::helper::SparseCtmcCslHelper::checkAndUpdateTransientProbabilityEpsilon(env, epsilon, result, relevantValues));
373 }
374
375 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(),
376 model.getManager().template getAddZero<ValueType>(),
377 model.getReachableStates(), odd, result));
378}
379
380template<storm::dd::DdType DdType, typename ValueType>
381 requires storm::NumberTraits<ValueType>::SupportsExponential
382std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeCumulativeRewards(
383 Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, bool onlyInitialStatesRelevant,
384 storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector,
385 typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel, ValueType timeBound) {
386 // Only compute the result if the model has a state-based reward model.
387 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
388
389 // If the time bound is zero, the result is the constant zero vector.
390 if (timeBound == 0) {
391 return std::unique_ptr<CheckResult>(
392 new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().template getAddZero<ValueType>()));
393 }
394
395 // Otherwise, we need to perform some computations.
396
397 // Start with the uniformization.
398 ValueType uniformizationRate = 1.02 * exitRateVector.getMax();
399 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
400
401 storm::utility::Stopwatch conversionWatch;
402
403 // Create ODD for the translation.
404 conversionWatch.start();
405 storm::dd::Odd odd = model.getReachableStates().createOdd();
406 conversionWatch.stop();
407
408 // Compute the uniformized matrix.
409 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
410 computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate);
411 conversionWatch.start();
412 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
413 conversionWatch.stop();
414
415 // Then compute the state reward vector to use in the computation.
416 storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false);
417 conversionWatch.start();
418 std::vector<ValueType> explicitTotalRewardVector = totalRewardVector.toVector(odd);
419 conversionWatch.stop();
420 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
421
422 ValueType maxReward = std::max(totalRewardVector.getMax(), -totalRewardVector.getMin());
423
424 // If all rewards are zero, the result is the constant zero vector.
425 if (storm::utility::isZero(maxReward)) {
426 return std::unique_ptr<CheckResult>(
427 new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().template getAddZero<ValueType>()));
428 }
429
430 // Set the possible (absolute) error allowed for truncation (epsilon for fox-glynn)
431 ValueType epsilon = storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getPrecision());
432 if (env.solver().timeBounded().getRelativeTerminationCriterion()) {
433 // Be more precise, if the value is very small (this still gives no sound guarantee)
434 epsilon *= std::min(storm::utility::one<ValueType>(), maxReward);
435 } else {
436 // Be more precise, if the maximal possible value is very large
437 epsilon /= std::max(storm::utility::one<ValueType>(), maxReward * timeBound);
438 }
439
440 storm::storage::BitVector relevantValues;
441 if (onlyInitialStatesRelevant) {
442 relevantValues = model.getInitialStates().toVector(odd);
443 } else {
444 relevantValues = storm::storage::BitVector(explicitTotalRewardVector.size(), true);
445 }
446
447 std::vector<ValueType> result;
448 // Finally, compute the transient probabilities.
449 // Loop until the desired precision is reached.
450 do {
451 result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType, true>(
452 env, explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, epsilon);
453 } while (storm::modelchecker::helper::SparseCtmcCslHelper::checkAndUpdateTransientProbabilityEpsilon(env, epsilon, result, relevantValues));
454
455 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(),
456 model.getManager().template getAddZero<ValueType>(),
457 model.getReachableStates(), std::move(odd), std::move(result)));
458}
459
460template<storm::dd::DdType DdType, class ValueType>
461storm::dd::Add<DdType, ValueType> HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
462 storm::dd::Add<DdType, ValueType> const& transitionMatrix,
463 storm::dd::Add<DdType, ValueType> const& exitRateVector,
464 storm::dd::Bdd<DdType> const& maybeStates, ValueType uniformizationRate) {
465 STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << ".");
466 STORM_LOG_DEBUG("Keeping " << maybeStates.getNonZeroCount() << " rows.");
467
468 // Cut all non-maybe rows/columns from the transition matrix.
469 storm::dd::Add<DdType, ValueType> uniformizedMatrix = transitionMatrix * maybeStates.template toAdd<ValueType>() *
470 maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>();
471
472 // Now perform the uniformization.
473 uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate);
474 storm::dd::Add<DdType, ValueType> diagonal = model.getRowColumnIdentity() * maybeStates.template toAdd<ValueType>();
475 storm::dd::Add<DdType, ValueType> diagonalOffset = diagonal;
476 diagonalOffset -= diagonal * (exitRateVector / model.getManager().getConstant(uniformizationRate));
477 uniformizedMatrix += diagonalOffset;
478
479 return uniformizedMatrix;
480}
481
482template<storm::dd::DdType DdType, class ValueType>
487
488// Explicit instantiations.
489
490// Cudd, double.
491template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeBoundedUntilProbabilities(
492 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model, bool onlyInitialStatesRelevant,
493 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
494 storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, bool qualitative, double lowerBound,
495 std::optional<double> const& upperBound);
496template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeInstantaneousRewards(
497 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model, bool onlyInitialStatesRelevant,
498 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
499 typename storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>::RewardModelType const& rewardModel, double timeBound);
500template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeCumulativeRewards(
501 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model, bool onlyInitialStatesRelevant,
502 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
503 typename storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>::RewardModelType const& rewardModel, double timeBound);
504template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeUntilProbabilities(
505 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model,
506 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
507 storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, bool qualitative);
508template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
509 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model,
510 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
511 typename storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>::RewardModelType const& rewardModel,
512 storm::dd::Bdd<storm::dd::DdType::CUDD> const& targetStates, bool qualitative);
513template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(Environment const& env,
514 storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model,
515 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix,
516 storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
517 storm::dd::Bdd<storm::dd::DdType::CUDD> const& nextStates);
518template storm::dd::Add<storm::dd::DdType::CUDD, double> HybridCtmcCslHelper::computeProbabilityMatrix(
519 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector);
520template storm::dd::Add<storm::dd::DdType::CUDD, double> HybridCtmcCslHelper::computeUniformizedMatrix(
521 storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model, storm::dd::Add<storm::dd::DdType::CUDD, double> const& transitionMatrix,
522 storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::CUDD> const& maybeStates,
523 double uniformizationRate);
524
525// Sylvan, double.
526template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeBoundedUntilProbabilities(
527 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model, bool onlyInitialStatesRelevant,
528 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
529 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative, double lowerBound,
530 std::optional<double> const& upperBound);
531template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeInstantaneousRewards(
532 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model, bool onlyInitialStatesRelevant,
533 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
534 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>::RewardModelType const& rewardModel, double timeBound);
535template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeCumulativeRewards(
536 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model, bool onlyInitialStatesRelevant,
537 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
538 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>::RewardModelType const& rewardModel, double timeBound);
539template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeUntilProbabilities(
540 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model,
541 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
542 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative);
543template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
544 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model,
545 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
546 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>::RewardModelType const& rewardModel,
547 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& targetStates, bool qualitative);
548template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(
549 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model,
550 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
551 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nextStates);
552template storm::dd::Add<storm::dd::DdType::Sylvan, double> HybridCtmcCslHelper::computeProbabilityMatrix(
553 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector);
554template storm::dd::Add<storm::dd::DdType::Sylvan, double> HybridCtmcCslHelper::computeUniformizedMatrix(
555 storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& transitionMatrix,
556 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& maybeStates,
557 double uniformizationRate);
558
559// Sylvan, rational number.
560template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeUntilProbabilities(
561 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
562 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
563 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates,
564 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative);
565template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
566 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
567 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
568 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector,
569 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::RewardModelType const& rewardModel,
570 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& targetStates, bool qualitative);
571template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(
572 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
573 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
574 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nextStates);
575template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> HybridCtmcCslHelper::computeProbabilityMatrix(
576 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
577 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector);
578template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> HybridCtmcCslHelper::computeUniformizedMatrix(
579 storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
580 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& transitionMatrix,
581 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& maybeStates,
582 storm::RationalNumber uniformizationRate);
583
584// Sylvan, rational function.
585template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeUntilProbabilities(
586 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
587 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
588 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates,
589 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative);
590template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
591 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
592 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
593 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector,
594 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::RewardModelType const& rewardModel,
595 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& targetStates, bool qualitative);
596template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(
597 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
598 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
599 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nextStates);
600template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> HybridCtmcCslHelper::computeProbabilityMatrix(
601 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
602 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector);
603template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> HybridCtmcCslHelper::computeUniformizedMatrix(
604 storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
605 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& transitionMatrix,
606 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& maybeStates,
607 storm::RationalFunction uniformizationRate);
608
609} // namespace helper
610} // namespace modelchecker
611} // namespace storm
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:52
storm::SolverEnvironment::timeBounded
TimeBoundedSolverEnvironment & timeBounded()
Definition SolverEnvironment.cpp:132
storm::TimeBoundedSolverEnvironment::getPrecision
storm::RationalNumber const & getPrecision() const
Definition TimeBoundedSolverEnvironment.cpp:34
storm::dd::Add::getMax
ValueType getMax() const
Retrieves the highest function value of any encoding.
Definition Add.cpp:468
storm::dd::Add::toMatrix
storm::storage::SparseMatrix< ValueType > toMatrix() const
Converts the ADD to a (sparse) matrix.
Definition Add.cpp:627
storm::dd::Add::getMin
ValueType getMin() const
Retrieves the lowest function value of any encoding.
Definition Add.cpp:463
storm::dd::Add::notZero
Bdd< LibraryType > notZero() const
Computes a BDD that represents the function in which all assignments with a function value unequal to...
Definition Add.cpp:424
storm::dd::Add::toVector
std::vector< ValueType > toVector() const
Converts the ADD to a vector.
Definition Add.cpp:545
storm::dd::Bdd::isZero
bool isZero() const
Retrieves whether this DD represents the constant zero function.
Definition Bdd.cpp:541
storm::dd::Bdd::getNonZeroCount
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
Definition Bdd.cpp:507
storm::dd::Bdd::swapVariables
Bdd< LibraryType > swapVariables(std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
Swaps the given pairs of meta variables in the BDD.
Definition Bdd.cpp:296
storm::dd::Bdd::createOdd
Odd createOdd() const
Creates an ODD based on the current BDD.
Definition Bdd.cpp:565
storm::dd::Bdd::toVector
storm::storage::BitVector toVector(storm::dd::Odd const &rowOdd) const
Converts the BDD to a bit vector.
Definition Bdd.cpp:491
storm::modelchecker::HybridQuantitativeCheckResult::toExplicitQuantitativeCheckResult
std::unique_ptr< CheckResult > toExplicitQuantitativeCheckResult() const
Definition HybridQuantitativeCheckResult.cpp:60
storm::modelchecker::HybridQuantitativeCheckResult::filter
virtual void filter(QualitativeCheckResult const &filter) override
Filters the current result wrt.
Definition HybridQuantitativeCheckResult.cpp:201
storm::modelchecker::helper::HybridCtmcCslHelper::computeProbabilityMatrix
static storm::dd::Add< DdType, ValueType > computeProbabilityMatrix(storm::dd::Add< DdType, ValueType > const &rateMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector)
Converts the given rate-matrix into a time-abstract probability matrix.
Definition HybridCtmcCslHelper.cpp:483
storm::modelchecker::helper::HybridCtmcCslHelper::computeNextProbabilities
static std::unique_ptr< CheckResult > computeNextProbabilities(Environment const &env, storm::models::symbolic::Ctmc< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &rateMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector, storm::dd::Bdd< DdType > const &nextStates)
Definition HybridCtmcCslHelper.cpp:36
storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards
static std::unique_ptr< CheckResult > computeInstantaneousRewards(Environment const &env, storm::models::symbolic::Ctmc< DdType, ValueType > const &model, bool onlyInitialStatesRelevant, storm::dd::Add< DdType, ValueType > const &rateMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector, typename storm::models::symbolic::Model< DdType, ValueType >::RewardModelType const &rewardModel, ValueType timeBound)
Definition HybridCtmcCslHelper.cpp:318
storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards
static std::unique_ptr< CheckResult > computeCumulativeRewards(Environment const &env, storm::models::symbolic::Ctmc< DdType, ValueType > const &model, bool onlyInitialStatesRelevant, storm::dd::Add< DdType, ValueType > const &rateMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector, typename storm::models::symbolic::Model< DdType, ValueType >::RewardModelType const &rewardModel, ValueType timeBound)
Definition HybridCtmcCslHelper.cpp:382
storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities
static std::unique_ptr< CheckResult > computeBoundedUntilProbabilities(Environment const &env, storm::models::symbolic::Ctmc< DdType, ValueType > const &model, bool onlyInitialStatesRelevant, storm::dd::Add< DdType, ValueType > const &rateMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector, storm::dd::Bdd< DdType > const &phiStates, storm::dd::Bdd< DdType > const &psiStates, bool qualitative, ValueType lowerBound, std::optional< ValueType > const &upperBound)
Definition HybridCtmcCslHelper.cpp:57
storm::modelchecker::helper::HybridCtmcCslHelper::computeUniformizedMatrix
static storm::dd::Add< DdType, ValueType > computeUniformizedMatrix(storm::models::symbolic::Ctmc< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector, storm::dd::Bdd< DdType > const &maybeStates, ValueType uniformizationRate)
Computes the matrix representing the transitions of the uniformized CTMC.
Definition HybridCtmcCslHelper.cpp:461
storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards
static std::unique_ptr< CheckResult > computeReachabilityRewards(Environment const &env, storm::models::symbolic::Ctmc< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &rateMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector, typename storm::models::symbolic::Model< DdType, ValueType >::RewardModelType const &rewardModel, storm::dd::Bdd< DdType > const &targetStates, bool qualitative)
Definition HybridCtmcCslHelper.cpp:27
storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities
static std::unique_ptr< CheckResult > computeUntilProbabilities(Environment const &env, storm::models::symbolic::Ctmc< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &rateMatrix, storm::dd::Add< DdType, ValueType > const &exitRateVector, storm::dd::Bdd< DdType > const &phiStates, storm::dd::Bdd< DdType > const &psiStates, bool qualitative)
Definition HybridCtmcCslHelper.cpp:45
storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards
static std::unique_ptr< CheckResult > computeReachabilityRewards(Environment const &env, storm::models::symbolic::Model< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, RewardModelType const &rewardModel, storm::dd::Bdd< DdType > const &targetStates, bool qualitative)
Definition HybridDtmcPrctlHelper.cpp:277
storm::modelchecker::helper::HybridDtmcPrctlHelper::computeNextProbabilities
static std::unique_ptr< CheckResult > computeNextProbabilities(Environment const &env, storm::models::symbolic::Model< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, storm::dd::Bdd< DdType > const &nextStates)
Definition HybridDtmcPrctlHelper.cpp:129
storm::modelchecker::helper::HybridDtmcPrctlHelper::computeUntilProbabilities
static std::unique_ptr< CheckResult > computeUntilProbabilities(Environment const &env, storm::models::symbolic::Model< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, storm::dd::Bdd< DdType > const &phiStates, storm::dd::Bdd< DdType > const &psiStates, bool qualitative)
Definition HybridDtmcPrctlHelper.cpp:28
storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities
static std::vector< ValueType > computeTransientProbabilities(Environment const &env, storm::storage::SparseMatrix< ValueType > const &uniformizedMatrix, std::vector< ValueType > const *addVector, ValueType timeBound, ValueType uniformizationRate, std::vector< ValueType > values, ValueType epsilon)
Computes the transient probabilities for lambda time steps.
Definition SparseCtmcCslHelper.cpp:619
storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities
static std::vector< ValueType > computeBoundedUntilProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &rateMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, std::vector< ValueType > const &exitRates, bool qualitative, ValueType lowerBound, std::optional< ValueType > const &upperBound)
Definition SparseCtmcCslHelper.cpp:57
storm::modelchecker::helper::SparseCtmcCslHelper::checkAndUpdateTransientProbabilityEpsilon
static bool checkAndUpdateTransientProbabilityEpsilon(storm::Environment const &env, ValueType &epsilon, std::vector< ValueType > const &resultVector, storm::storage::BitVector const &relevantPositions)
Checks whether the given result vector is sufficiently precise, according to the provided epsilon and...
Definition SparseCtmcCslHelper.cpp:22
storm::models::symbolic::Ctmc
This class represents a continuous-time Markov chain.
Definition Ctmc.h:13
storm::models::symbolic::Model::getManager
storm::dd::DdManager< Type > & getManager() const
Retrieves the manager responsible for the DDs that represent this model.
Definition Model.cpp:89
storm::models::symbolic::Model::getColumnVariables
std::set< storm::expressions::Variable > const & getColumnVariables() const
Retrieves the meta variables used to encode the columns of the transition matrix and the vector indic...
Definition Model.cpp:194
storm::models::symbolic::Model::getRowColumnIdentity
storm::dd::Add< Type, ValueType > getRowColumnIdentity() const
Retrieves an ADD that represents the diagonal of the transition matrix.
Definition Model.cpp:235
storm::models::symbolic::Model::getInitialStates
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:104
storm::models::symbolic::Model::getRowColumnMetaVariablePairs
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & getRowColumnMetaVariablePairs() const
Retrieves the pairs of row and column meta variables.
Definition Model.cpp:220
storm::models::symbolic::Model::RewardModelType
StandardRewardModel< Type, ValueType > RewardModelType
Definition Model.h:47
storm::models::symbolic::Model::getReachableStates
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:99
storm::models::symbolic::StandardRewardModel::hasStateRewards
bool hasStateRewards() const
Retrieves whether the reward model has state rewards.
Definition StandardRewardModel.cpp:28
storm::models::symbolic::StandardRewardModel::getTotalRewardVector
storm::dd::Add< Type, ValueType > getTotalRewardVector(storm::dd::Add< Type, ValueType > const &transitionMatrix, std::set< storm::expressions::Variable > const &columnVariables) const
Creates a vector representing the complete reward vector based on the state-, state-action- and trans...
Definition StandardRewardModel.cpp:127
storm::models::symbolic::StandardRewardModel::empty
bool empty() const
Retrieves whether the reward model is empty.
Definition StandardRewardModel.cpp:23
storm::models::symbolic::StandardRewardModel::getStateRewardVector
storm::dd::Add< Type, ValueType > const & getStateRewardVector() const
Retrieves the state rewards of the reward model.
Definition StandardRewardModel.cpp:38
storm::models::symbolic::StandardRewardModel::divideStateRewardVector
StandardRewardModel< Type, ValueType > divideStateRewardVector(storm::dd::Add< Type, ValueType > const &divisor) const
Divides the state reward vector of the reward model by the given divisor.
Definition StandardRewardModel.cpp:180
storm::solver::SolveGoal::setRelevantValues
void setRelevantValues(storm::storage::BitVector &&values)
Definition SolveGoal.cpp:147
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:362
storm::storage::SparseMatrix::transpose
storm::storage::SparseMatrix< value_type > transpose(bool joinGroups=false, bool keepZeros=false) const
Transposes the matrix.
Definition SparseMatrix.cpp:1405
storm::utility::Stopwatch
A class that provides convenience operations to display run times.
Definition Stopwatch.h:13
storm::utility::Stopwatch::getTimeInMilliseconds
MilisecondType getTimeInMilliseconds() const
Gets the measured time in milliseconds.
Definition Stopwatch.cpp:21
storm::utility::Stopwatch::start
void start()
Start stopwatch (again) and start measuring time.
Definition Stopwatch.cpp:48
storm::utility::Stopwatch::stop
void stop()
Stop stopwatch and add measured time to total time.
Definition Stopwatch.cpp:42
STORM_LOG_INFO
#define STORM_LOG_INFO(message)
Definition logging.h:34
STORM_LOG_DEBUG
#define STORM_LOG_DEBUG(message)
Definition logging.h:28
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:39
storm::utility::graph::performProbGreater0
storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Performs a backward depth-first search trough the underlying graph structure of the given model to de...
Definition graph.cpp:316
storm::utility::isZero
bool isZero(ValueType const &a)
Definition constants.cpp:44
storm::utility::zero
ValueType zero()
Definition constants.cpp:26
storm::utility::one
ValueType one()
Definition constants.cpp:21
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:145
storm::RationalFunction
carl::RationalFunction< Polynomial, true > RationalFunction
Definition RationalFunctionForward.h:47
storm::NumberTraits::SupportsExponential
static const bool SupportsExponential
Definition NumberTraits.h:12