Storm 1.11.1.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, ValueType upperBound) {
61 // If the time bounds are [0, inf], we rather call untimed reachability.
62 if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity<ValueType>()) {
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 (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 == storm::utility::infinity<ValueType>()) {
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 result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
172 } else {
173 STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException,
174 "Expected check result of different type.");
175 result = unboundedResult->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().toVector(odd);
176 }
177
178 // Determine the uniformization rate for the transient probability computation.
179 ValueType uniformizationRate = 1.02 * (relevantStates.template toAdd<ValueType>() * exitRateVector).getMax();
180
181 // Compute the uniformized matrix.
182 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
183 computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate);
184 conversionWatch.start();
185 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
186 conversionWatch.stop();
187 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
188
189 // Compute the transient probabilities.
190 result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(
191 env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result, epsilon);
192
193 return std::unique_ptr<CheckResult>(
194 new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), !relevantStates && model.getReachableStates(),
195 model.getManager().template getAddZero<ValueType>(), relevantStates, odd, result));
196 } else {
197 // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf.
198
199 if (lowerBound != upperBound) {
200 // In this case, the interval is of the form [t, t'] with t != 0, t' != inf and t != t'.
201
202 // Find the maximal rate of all 'maybe' states to take it as the uniformization rate.
203 ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * exitRateVector).getMax();
204 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
205
206 // Compute the (first) uniformized matrix.
207 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
208 computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate);
209
210 // Create the one-step vector.
211 storm::dd::Add<DdType, ValueType> b = (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * rateMatrix *
212 psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>())
213 .sumAbstract(model.getColumnVariables()) /
214 model.getManager().getConstant(uniformizationRate);
215
216 // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation.
217 storm::utility::Stopwatch conversionWatch(true);
218 storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd();
219 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
220 std::vector<ValueType> explicitB = b.toVector(odd);
221 conversionWatch.stop();
222
223 // Compute the transient probabilities.
224 std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
225 std::vector<ValueType> subResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(
226 env, explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values, epsilon);
227
228 // Transform the explicit result to a hybrid check result, so we can easily convert it to
229 // a symbolic qualitative format.
230 HybridQuantitativeCheckResult<DdType> hybridResult(
231 model.getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && model.getReachableStates()),
232 psiStates.template toAdd<ValueType>(), statesWithProbabilityGreater0NonPsi, odd, subResult);
233
234 // Compute the set of relevant states.
235 storm::dd::Bdd<DdType> relevantStates = statesWithProbabilityGreater0 && phiStates;
236
237 // Filter the unbounded result such that it only contains values for the relevant states.
238 hybridResult.filter(SymbolicQualitativeCheckResult<DdType>(model.getReachableStates(), relevantStates));
239
240 // Build an ODD for the relevant states.
241 conversionWatch.start();
242 odd = relevantStates.createOdd();
243
244 std::unique_ptr<CheckResult> explicitResult = hybridResult.toExplicitQuantitativeCheckResult();
245 conversionWatch.stop();
246 std::vector<ValueType> newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
247
248 // Then compute the transient probabilities of being in such a state after t time units. For this,
249 // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
250 uniformizationRate = 1.02 * (relevantStates.template toAdd<ValueType>() * exitRateVector).getMax();
251 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
252
253 // If the lower and upper bounds coincide, we have only determined the relevant states at this
254 // point, but we still need to construct the starting vector.
255 if (lowerBound == upperBound) {
256 odd = relevantStates.createOdd();
257 newSubresult = psiStates.template toAdd<ValueType>().toVector(odd);
258 }
259
260 // Finally, we compute the second set of transient probabilities.
261 uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate);
262 conversionWatch.start();
263 explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
264 conversionWatch.stop();
265 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
266
267 newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(
268 env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, epsilon);
269
270 return std::unique_ptr<CheckResult>(
271 new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), !relevantStates && model.getReachableStates(),
272 model.getManager().template getAddZero<ValueType>(), relevantStates, odd, newSubresult));
273 } else {
274 // In this case, the interval is of the form [t, t] with t != 0, t != inf.
275
276 storm::utility::Stopwatch conversionWatch;
277
278 // Build an ODD for the relevant states.
279 conversionWatch.start();
280 storm::dd::Odd odd = statesWithProbabilityGreater0.createOdd();
281
282 std::vector<ValueType> newSubresult = psiStates.template toAdd<ValueType>().toVector(odd);
283 conversionWatch.stop();
284
285 // Then compute the transient probabilities of being in such a state after t time units. For this,
286 // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
287 ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0.template toAdd<ValueType>() * exitRateVector).getMax();
288 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
289
290 // Finally, we compute the second set of transient probabilities.
291 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
292 computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate);
293 conversionWatch.start();
294 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
295 conversionWatch.stop();
296 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
297
298 newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(
299 env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, epsilon);
300
301 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(
302 model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(),
303 model.getManager().template getAddZero<ValueType>(), statesWithProbabilityGreater0, odd, newSubresult));
304 }
305 }
306 }
307 } else {
308 return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), psiStates.template toAdd<ValueType>()));
309 }
310}
311
312template<storm::dd::DdType DdType, typename ValueType>
313 requires storm::NumberTraits<ValueType>::SupportsExponential
314std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeInstantaneousRewards(
315 Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, bool onlyInitialStatesRelevant,
316 storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector,
317 typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel, ValueType timeBound) {
318 // Only compute the result if the model has a state-based reward model.
319 STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException,
320 "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0.");
321
322 storm::utility::Stopwatch conversionWatch;
323
324 // Create ODD for the translation.
325 conversionWatch.start();
326 storm::dd::Odd odd = model.getReachableStates().createOdd();
327 conversionWatch.stop();
328
329 // Initialize result to state rewards of the model.
330 auto rewardsAdd = rewardModel.getStateRewardVector();
331 std::vector<ValueType> result = rewardsAdd.toVector(odd);
332 ValueType maxValue = std::max(rewardsAdd.getMax(), -rewardsAdd.getMin());
333
334 // If the rewards are not zero and the time-bound is not zero, we need to perform a transient analysis.
335 if (!storm::utility::isZero(maxValue) && timeBound > 0) {
336 ValueType uniformizationRate = 1.02 * exitRateVector.getMax();
337 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
338
339 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
340 computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate);
341
342 conversionWatch.start();
343 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
344 conversionWatch.stop();
345 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
346
347 // Set the possible error allowed for truncation (epsilon for fox-glynn)
348 ValueType epsilon = storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getPrecision());
349 if (env.solver().timeBounded().getRelativeTerminationCriterion()) {
350 // Be more precise, if the maximum value is very small (This still gives no sound guarantee!)
351 epsilon *= std::min(storm::utility::one<ValueType>(), maxValue);
352 } else {
353 // Be more precise, if the maximal possible value is very large
354 epsilon /= std::max(storm::utility::one<ValueType>(), maxValue);
355 }
356
357 storm::storage::BitVector relevantValues;
358 if (onlyInitialStatesRelevant) {
359 relevantValues = model.getInitialStates().toVector(odd);
360 } else {
361 relevantValues = storm::storage::BitVector(result.size(), true);
362 }
363
364 // Loop until the desired precision is reached.
365 do {
366 result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(env, explicitUniformizedMatrix, nullptr,
367 timeBound, uniformizationRate, result, epsilon);
368 } while (storm::modelchecker::helper::SparseCtmcCslHelper::checkAndUpdateTransientProbabilityEpsilon(env, epsilon, result, relevantValues));
369 }
370
371 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(),
372 model.getManager().template getAddZero<ValueType>(),
373 model.getReachableStates(), odd, result));
374}
375
376template<storm::dd::DdType DdType, typename ValueType>
377 requires storm::NumberTraits<ValueType>::SupportsExponential
378std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeCumulativeRewards(
379 Environment const& env, storm::models::symbolic::Ctmc<DdType, ValueType> const& model, bool onlyInitialStatesRelevant,
380 storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector,
381 typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType const& rewardModel, ValueType timeBound) {
382 // Only compute the result if the model has a state-based reward model.
383 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
384
385 // If the time bound is zero, the result is the constant zero vector.
386 if (timeBound == 0) {
387 return std::unique_ptr<CheckResult>(
388 new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().template getAddZero<ValueType>()));
389 }
390
391 // Otherwise, we need to perform some computations.
392
393 // Start with the uniformization.
394 ValueType uniformizationRate = 1.02 * exitRateVector.getMax();
395 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
396
397 storm::utility::Stopwatch conversionWatch;
398
399 // Create ODD for the translation.
400 conversionWatch.start();
401 storm::dd::Odd odd = model.getReachableStates().createOdd();
402 conversionWatch.stop();
403
404 // Compute the uniformized matrix.
405 storm::dd::Add<DdType, ValueType> uniformizedMatrix =
406 computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate);
407 conversionWatch.start();
408 storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
409 conversionWatch.stop();
410
411 // Then compute the state reward vector to use in the computation.
412 storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false);
413 conversionWatch.start();
414 std::vector<ValueType> explicitTotalRewardVector = totalRewardVector.toVector(odd);
415 conversionWatch.stop();
416 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
417
418 ValueType maxReward = std::max(totalRewardVector.getMax(), -totalRewardVector.getMin());
419
420 // If all rewards are zero, the result is the constant zero vector.
421 if (storm::utility::isZero(maxReward)) {
422 return std::unique_ptr<CheckResult>(
423 new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().template getAddZero<ValueType>()));
424 }
425
426 // Set the possible (absolute) error allowed for truncation (epsilon for fox-glynn)
427 ValueType epsilon = storm::utility::convertNumber<ValueType>(env.solver().timeBounded().getPrecision());
428 if (env.solver().timeBounded().getRelativeTerminationCriterion()) {
429 // Be more precise, if the value is very small (this still gives no sound guarantee)
430 epsilon *= std::min(storm::utility::one<ValueType>(), maxReward);
431 } else {
432 // Be more precise, if the maximal possible value is very large
433 epsilon /= std::max(storm::utility::one<ValueType>(), maxReward * timeBound);
434 }
435
436 storm::storage::BitVector relevantValues;
437 if (onlyInitialStatesRelevant) {
438 relevantValues = model.getInitialStates().toVector(odd);
439 } else {
440 relevantValues = storm::storage::BitVector(explicitTotalRewardVector.size(), true);
441 }
442
443 std::vector<ValueType> result;
444 // Finally, compute the transient probabilities.
445 // Loop until the desired precision is reached.
446 do {
447 result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType, true>(
448 env, explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, epsilon);
449 } while (storm::modelchecker::helper::SparseCtmcCslHelper::checkAndUpdateTransientProbabilityEpsilon(env, epsilon, result, relevantValues));
450
451 return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(),
452 model.getManager().template getAddZero<ValueType>(),
453 model.getReachableStates(), std::move(odd), std::move(result)));
454}
455
456template<storm::dd::DdType DdType, class ValueType>
457storm::dd::Add<DdType, ValueType> HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc<DdType, ValueType> const& model,
458 storm::dd::Add<DdType, ValueType> const& transitionMatrix,
459 storm::dd::Add<DdType, ValueType> const& exitRateVector,
460 storm::dd::Bdd<DdType> const& maybeStates, ValueType uniformizationRate) {
461 STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << ".");
462 STORM_LOG_DEBUG("Keeping " << maybeStates.getNonZeroCount() << " rows.");
463
464 // Cut all non-maybe rows/columns from the transition matrix.
465 storm::dd::Add<DdType, ValueType> uniformizedMatrix = transitionMatrix * maybeStates.template toAdd<ValueType>() *
466 maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>();
467
468 // Now perform the uniformization.
469 uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate);
470 storm::dd::Add<DdType, ValueType> diagonal = model.getRowColumnIdentity() * maybeStates.template toAdd<ValueType>();
471 storm::dd::Add<DdType, ValueType> diagonalOffset = diagonal;
472 diagonalOffset -= diagonal * (exitRateVector / model.getManager().getConstant(uniformizationRate));
473 uniformizedMatrix += diagonalOffset;
474
475 return uniformizedMatrix;
476}
477
478template<storm::dd::DdType DdType, class ValueType>
483
484// Explicit instantiations.
485
486// Cudd, double.
487template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeBoundedUntilProbabilities(
488 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model, bool onlyInitialStatesRelevant,
489 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
490 storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, bool qualitative, double lowerBound,
491 double upperBound);
492template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeInstantaneousRewards(
493 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model, bool onlyInitialStatesRelevant,
494 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
495 typename storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>::RewardModelType const& rewardModel, double timeBound);
496template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeCumulativeRewards(
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::computeUntilProbabilities(
501 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model,
502 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
503 storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, bool qualitative);
504template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
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 typename storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>::RewardModelType const& rewardModel,
508 storm::dd::Bdd<storm::dd::DdType::CUDD> const& targetStates, bool qualitative);
509template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(Environment const& env,
510 storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model,
511 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix,
512 storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector,
513 storm::dd::Bdd<storm::dd::DdType::CUDD> const& nextStates);
514template storm::dd::Add<storm::dd::DdType::CUDD, double> HybridCtmcCslHelper::computeProbabilityMatrix(
515 storm::dd::Add<storm::dd::DdType::CUDD, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector);
516template storm::dd::Add<storm::dd::DdType::CUDD, double> HybridCtmcCslHelper::computeUniformizedMatrix(
517 storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& model, storm::dd::Add<storm::dd::DdType::CUDD, double> const& transitionMatrix,
518 storm::dd::Add<storm::dd::DdType::CUDD, double> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::CUDD> const& maybeStates,
519 double uniformizationRate);
520
521// Sylvan, double.
522template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeBoundedUntilProbabilities(
523 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model, bool onlyInitialStatesRelevant,
524 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
525 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative, double lowerBound,
526 double upperBound);
527template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeInstantaneousRewards(
528 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model, bool onlyInitialStatesRelevant,
529 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
530 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>::RewardModelType const& rewardModel, double timeBound);
531template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeCumulativeRewards(
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::computeUntilProbabilities(
536 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model,
537 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
538 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative);
539template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
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 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>::RewardModelType const& rewardModel,
543 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& targetStates, bool qualitative);
544template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(
545 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model,
546 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector,
547 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nextStates);
548template storm::dd::Add<storm::dd::DdType::Sylvan, double> HybridCtmcCslHelper::computeProbabilityMatrix(
549 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& rateMatrix, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector);
550template storm::dd::Add<storm::dd::DdType::Sylvan, double> HybridCtmcCslHelper::computeUniformizedMatrix(
551 storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Add<storm::dd::DdType::Sylvan, double> const& transitionMatrix,
552 storm::dd::Add<storm::dd::DdType::Sylvan, double> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& maybeStates,
553 double uniformizationRate);
554
555// Sylvan, rational number.
556template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeUntilProbabilities(
557 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
558 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
559 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates,
560 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative);
561template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
562 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
563 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
564 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector,
565 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::RewardModelType const& rewardModel,
566 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& targetStates, bool qualitative);
567template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(
568 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
569 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
570 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nextStates);
571template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> HybridCtmcCslHelper::computeProbabilityMatrix(
572 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& rateMatrix,
573 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector);
574template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> HybridCtmcCslHelper::computeUniformizedMatrix(
575 storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model,
576 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& transitionMatrix,
577 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& maybeStates,
578 storm::RationalNumber uniformizationRate);
579
580// Sylvan, rational function.
581template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeUntilProbabilities(
582 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
583 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
584 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates,
585 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, bool qualitative);
586template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeReachabilityRewards(
587 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
588 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
589 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector,
590 typename storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::RewardModelType const& rewardModel,
591 storm::dd::Bdd<storm::dd::DdType::Sylvan> const& targetStates, bool qualitative);
592template std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeNextProbabilities(
593 Environment const& env, storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
594 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
595 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nextStates);
596template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> HybridCtmcCslHelper::computeProbabilityMatrix(
597 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& rateMatrix,
598 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector);
599template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> HybridCtmcCslHelper::computeUniformizedMatrix(
600 storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model,
601 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& transitionMatrix,
602 storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& exitRateVector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& maybeStates,
603 storm::RationalFunction uniformizationRate);
604
605} // namespace helper
606} // namespace modelchecker
607} // namespace storm
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::SolverEnvironment::timeBounded
TimeBoundedSolverEnvironment & timeBounded()
Definition SolverEnvironment.cpp:35
storm::TimeBoundedSolverEnvironment::getPrecision
storm::RationalNumber const & getPrecision() const
Definition TimeBoundedSolverEnvironment.cpp:36
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:211
storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards
static ::SupportsExponential 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)
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:479
storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities
static ::SupportsExponential 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, ValueType upperBound)
storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards
static ::SupportsExponential 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)
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::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:457
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 ::SupportsExponential 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.
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:87
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:192
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:233
storm::models::symbolic::Model::getInitialStates
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:102
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:218
storm::models::symbolic::Model::getReachableStates
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:97
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:140
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:328
storm::storage::SparseMatrix::transpose
storm::storage::SparseMatrix< value_type > transpose(bool joinGroups=false, bool keepZeros=false) const
Transposes the matrix.
Definition SparseMatrix.cpp:1476
storm::utility::Stopwatch
A class that provides convenience operations to display run times.
Definition Stopwatch.h:14
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:24
STORM_LOG_DEBUG
#define STORM_LOG_DEBUG(message)
Definition logging.h:18
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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:315
storm::utility::isZero
bool isZero(ValueType const &a)
Definition constants.cpp:39