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