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