sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added timing measurements to symbolic to sparse conversion in hybrid model checkers

tempestpy_adaptions
dehnert 7 years ago
parent
139752eb66
commit
51ebb47587
3 changed files with 155 additions and 31 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 75
      src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
  2. 56
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  3. 55
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

75
src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
View File

@ -18,6 +18,8 @@
#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/utility/Stopwatch.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidOperationException.h"
@ -79,12 +81,16 @@ namespace storm {
// Compute the vector that is to be added as a compensation for removing the absorbing states.
storm::dd::Add<DdType, ValueType> b = (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate);
storm::utility::Stopwatch conversionWatch(true);
// Create an ODD for the translation to an explicit representation.
storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd();
// Convert the symbolic parts to their explicit representation.
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitB = b.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Finally compute the transient probabilities.
std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
@ -106,12 +112,18 @@ namespace storm {
// Filter the unbounded result such that it only contains values for the relevant states.
unboundedResult->filter(SymbolicQualitativeCheckResult<DdType>(model.getReachableStates(), relevantStates));
storm::utility::Stopwatch conversionWatch;
// Build an ODD for the relevant states.
conversionWatch.start();
storm::dd::Odd odd = relevantStates.createOdd();
conversionWatch.stop();
std::vector<ValueType> result;
if (unboundedResult->isHybridQuantitativeCheckResult()) {
conversionWatch.start();
std::unique_ptr<CheckResult> explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult<DdType, ValueType>().toExplicitQuantitativeCheckResult();
conversionWatch.stop();
result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
} else {
STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException, "Expected check result of different type.");
@ -123,8 +135,11 @@ namespace storm {
// Compute the uniformized matrix.
storm::dd::Add<DdType, ValueType> uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate);
conversionWatch.start();
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Compute the transient probabilities.
result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result);
@ -146,10 +161,12 @@ namespace storm {
storm::dd::Add<DdType, ValueType> b = (statesWithProbabilityGreater0NonPsi.template toAdd<ValueType>() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate);
// Build an ODD for the relevant states and translate the symbolic parts to their explicit representation.
storm::utility::Stopwatch conversionWatch(true);
storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd();
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitB = b.toVector(odd);
conversionWatch.stop();
// Compute the transient probabilities.
std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> subResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values);
@ -164,13 +181,15 @@ namespace storm {
// Filter the unbounded result such that it only contains values for the relevant states.
hybridResult.filter(SymbolicQualitativeCheckResult<DdType>(model.getReachableStates(), relevantStates));
// Build an ODD for the relevant states.
conversionWatch.start();
odd = relevantStates.createOdd();
std::unique_ptr<CheckResult> explicitResult = hybridResult.toExplicitQuantitativeCheckResult();
conversionWatch.stop();
std::vector<ValueType> newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
// Then compute the transient probabilities of being in such a state after t time units. For this,
// we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
uniformizationRate = 1.02 * (relevantStates.template toAdd<ValueType>() * exitRateVector).getMax();
@ -185,19 +204,26 @@ namespace storm {
// Finally, we compute the second set of transient probabilities.
uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate);
conversionWatch.start();
explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero<ValueType>(), relevantStates, odd, newSubresult));
} else {
// In this case, the interval is of the form [t, t] with t != 0, t != inf.
storm::utility::Stopwatch conversionWatch;
// Build an ODD for the relevant states.
conversionWatch.start();
storm::dd::Odd odd = statesWithProbabilityGreater0.createOdd();
std::vector<ValueType> newSubresult = psiStates.template toAdd<ValueType>().toVector(odd);
conversionWatch.stop();
// Then compute the transient probabilities of being in such a state after t time units. For this,
// we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0.template toAdd<ValueType>() * exitRateVector).getMax();
@ -205,8 +231,11 @@ namespace storm {
// Finally, we compute the second set of transient probabilities.
storm::dd::Add<DdType, ValueType> uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate);
conversionWatch.start();
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(), model.getManager().template getAddZero<ValueType>(), statesWithProbabilityGreater0, odd, newSubresult));
@ -229,8 +258,12 @@ namespace storm {
// Only compute the result if the model has a state-based reward model.
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
storm::utility::Stopwatch conversionWatch;
// Create ODD for the translation.
conversionWatch.start();
storm::dd::Odd odd = model.getReachableStates().createOdd();
conversionWatch.stop();
// Initialize result to state rewards of the model.
std::vector<ValueType> result = rewardModel.getStateRewardVector().toVector(odd);
@ -242,7 +275,11 @@ namespace storm {
storm::dd::Add<DdType, ValueType> uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate);
conversionWatch.start();
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType>(env, explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, result);
}
@ -270,17 +307,25 @@ namespace storm {
ValueType uniformizationRate = 1.02 * exitRateVector.getMax();
STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
storm::utility::Stopwatch conversionWatch;
// Create ODD for the translation.
conversionWatch.start();
storm::dd::Odd odd = model.getReachableStates().createOdd();
conversionWatch.stop();
// Compute the uniformized matrix.
storm::dd::Add<DdType, ValueType> uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate);
conversionWatch.start();
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
conversionWatch.stop();
// Then compute the state reward vector to use in the computation.
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false);
std::vector<ValueType> explicitTotalRewardVector = totalRewardVector.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Finally, compute the transient probabilities.
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities<ValueType, true>(env, explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
@ -295,12 +340,16 @@ namespace storm {
std::unique_ptr<CheckResult> HybridCtmcCslHelper::computeLongRunAverageProbabilities(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& psiStates) {
storm::dd::Add<DdType, ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
storm::utility::Stopwatch conversionWatch(true);
// Create ODD for the translation.
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitExitRateVector = exitRateVector.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(env, storm::solver::SolveGoal<ValueType>(), explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
@ -312,12 +361,16 @@ namespace storm {
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
storm::dd::Add<DdType, ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
storm::utility::Stopwatch conversionWatch(true);
// Create ODD for the translation.
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitExitRateVector = exitRateVector.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal<ValueType>(), explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));

56
src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
View File

@ -20,11 +20,12 @@
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "storm/utility/Stopwatch.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm {
namespace modelchecker {
namespace helper {
@ -46,8 +47,12 @@ namespace storm {
} else {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
storm::utility::Stopwatch conversionWatch;
// Create the ODD for the translation between symbolic and explicit storage.
conversionWatch.start();
storm::dd::Odd odd = maybeStates.createOdd();
conversionWatch.stop();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@ -83,9 +88,12 @@ namespace storm {
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));
// Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
conversionWatch.start();
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
std::vector<ValueType> b = subvector.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitSubmatrix));
solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->solveEquations(env, x, b);
@ -122,8 +130,12 @@ namespace storm {
// If there are maybe states, we need to perform matrix-vector multiplications.
if (!maybeStates.isZero()) {
storm::utility::Stopwatch conversionWatch;
// Create the ODD for the translation between symbolic and explicit storage.
conversionWatch.start();
storm::dd::Odd odd = maybeStates.createOdd();
conversionWatch.stop();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@ -144,9 +156,12 @@ namespace storm {
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
// Translate the symbolic matrix/vector to their explicit representations.
conversionWatch.start();
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
std::vector<ValueType> b = subvector.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitSubmatrix);
multiplier->repeatedMultiply(env, x, &b, stepBound);
@ -162,6 +177,8 @@ namespace storm {
// Only compute the result if the model has at least one reward this->getModel().
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
storm::utility::Stopwatch conversionWatch(true);
// Create the ODD for the translation between symbolic and explicit storage.
storm::dd::Odd odd = model.getReachableStates().createOdd();
@ -170,7 +187,9 @@ namespace storm {
// Translate the symbolic matrix to its explicit representations.
storm::storage::SparseMatrix<ValueType> explicitMatrix = transitionMatrix.toMatrix(odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Perform the matrix-vector multiplication.
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitMatrix);
multiplier->repeatedMultiply(env, x, nullptr, stepBound);
@ -187,16 +206,20 @@ namespace storm {
// Compute the reward vector to add in each step based on the available reward models.
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables());
// Create the ODD for the translation between symbolic and explicit storage.
storm::dd::Odd odd = model.getReachableStates().createOdd();
// Create the solution vector.
std::vector<ValueType> x(model.getNumberOfStates(), storm::utility::zero<ValueType>());
storm::utility::Stopwatch conversionWatch(true);
// Create the ODD for the translation between symbolic and explicit storage.
storm::dd::Odd odd = model.getReachableStates().createOdd();
// Translate the symbolic matrix/vector to their explicit representations.
storm::storage::SparseMatrix<ValueType> explicitMatrix = transitionMatrix.toMatrix(odd, odd);
std::vector<ValueType> b = totalRewardVector.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Perform the matrix-vector multiplication.
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitMatrix);
multiplier->repeatedMultiply(env, x, &b, stepBound);
@ -239,8 +262,12 @@ namespace storm {
} else {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
storm::utility::Stopwatch conversionWatch;
// Create the ODD for the translation between symbolic and explicit storage.
conversionWatch.start();
storm::dd::Odd odd = maybeStates.createOdd();
conversionWatch.stop();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@ -281,9 +308,12 @@ namespace storm {
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));
// Translate the symbolic matrix/vector to their explicit representations.
conversionWatch.start();
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
std::vector<ValueType> b = subvector.toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Create the upper bounds vector if one was requested.
boost::optional<std::vector<ValueType>> upperBounds;
if (oneStepTargetProbs) {
@ -311,8 +341,11 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& targetStates) {
// Create ODD for the translation.
storm::utility::Stopwatch conversionWatch(true);
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageProbabilities(env, storm::solver::SolveGoal<ValueType>(), explicitProbabilityMatrix, targetStates.toVector(odd));
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
@ -321,9 +354,12 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel) {
// Create ODD for the translation.
storm::utility::Stopwatch conversionWatch(true);
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageRewards(env, storm::solver::SolveGoal<ValueType>(), explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd));
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}

55
src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
View File

@ -23,6 +23,8 @@
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/Multiplier.h"
#include "storm/utility/Stopwatch.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
@ -174,8 +176,12 @@ namespace storm {
extendedMaybeStates |= maybeStates.relationalProduct(transitionMatrixBdd.existsAbstract(model.getNondeterminismVariables()), model.getRowVariables(), model.getColumnVariables());
}
storm::utility::Stopwatch conversionWatch;
// Create the ODD for the translation between symbolic and explicit storage.
conversionWatch.start();
storm::dd::Odd odd = extendedMaybeStates.createOdd();
conversionWatch.stop();
// Convert the maybe states BDD to an ADD.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@ -191,20 +197,21 @@ namespace storm {
submatrix *= extendedMaybeStates.template toAdd<ValueType>().swapVariables(model.getRowColumnMetaVariablePairs());
// Only translate the matrix for now.
conversionWatch.start();
explicitRepresentation.first = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd);
// Get all original maybe states in the extended matrix.
solverRequirementsData.properMaybeStates = maybeStates.toVector(odd);
// Compute the target states within the set of extended maybe states.
storm::storage::BitVector targetStates = (extendedMaybeStates && statesWithProbability01.second).toVector(odd);
conversionWatch.stop();
// Eliminate the end components and remove the states that are not interesting (target or non-filter).
eliminateEndComponentsAndExtendedStatesUntilProbabilities(explicitRepresentation, solverRequirementsData, targetStates);
// The solution becomes unique after end components have been eliminated.
uniqueSolution = true;
} else {
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
// maybe states.
@ -217,13 +224,17 @@ namespace storm {
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
// Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
conversionWatch.start();
explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd);
conversionWatch.stop();
if (requirements.requiresValidInitialScheduler()) {
solverRequirementsData.initialScheduler = computeValidInitialSchedulerForUntilProbabilities<ValueType>(explicitRepresentation.first, explicitRepresentation.second);
}
}
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Create the solution vector.
std::vector<ValueType> x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero<ValueType>());
@ -287,8 +298,12 @@ namespace storm {
// If there are maybe states, we need to perform matrix-vector multiplications.
if (!maybeStates.isZero()) {
storm::utility::Stopwatch conversionWatch;
// Create the ODD for the translation between symbolic and explicit storage.
conversionWatch.start();
storm::dd::Odd odd = maybeStates.createOdd();
conversionWatch.stop();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@ -309,8 +324,11 @@ namespace storm {
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
// Translate the symbolic matrix/vector to their explicit representations.
conversionWatch.start();
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitRepresentation.first);
multiplier->repeatedMultiplyAndReduce(env, dir, x, &explicitRepresentation.second, stepBound);
@ -326,6 +344,8 @@ namespace storm {
// Only compute the result if the model has at least one reward this->getModel().
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
storm::utility::Stopwatch conversionWatch;
// Create the ODD for the translation between symbolic and explicit storage.
storm::dd::Odd odd = model.getReachableStates().createOdd();
@ -334,7 +354,9 @@ namespace storm {
// Create the solution vector (and initialize it to the state rewards of the model).
std::vector<ValueType> x = rewardModel.getStateRewardVector().toVector(odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Perform the matrix-vector multiplication.
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitMatrix);
multiplier->repeatedMultiplyAndReduce(env, dir, x, nullptr, stepBound);
@ -351,15 +373,19 @@ namespace storm {
// Compute the reward vector to add in each step based on the available reward models.
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables());
// Create the ODD for the translation between symbolic and explicit storage.
storm::dd::Odd odd = model.getReachableStates().createOdd();
// Create the solution vector.
std::vector<ValueType> x(model.getNumberOfStates(), storm::utility::zero<ValueType>());
storm::utility::Stopwatch conversionWatch(true);
// Create the ODD for the translation between symbolic and explicit storage.
storm::dd::Odd odd = model.getReachableStates().createOdd();
// Translate the symbolic matrix/vector to their explicit representations.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = transitionMatrix.toMatrixVector(totalRewardVector, model.getNondeterminismVariables(), odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Perform the matrix-vector multiplication.
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitRepresentation.first);
multiplier->repeatedMultiplyAndReduce(env, dir, x, &explicitRepresentation.second, stepBound);
@ -546,8 +572,12 @@ namespace storm {
// Compute the set of maybe states that we are required to keep in the translation to explicit.
storm::dd::Bdd<DdType> requiredMaybeStates = extendMaybeStates ? maybeStatesWithTargetStates : maybeStates;
storm::utility::Stopwatch conversionWatch;
// Create the ODD for the translation between symbolic and explicit storage.
conversionWatch.start();
storm::dd::Odd odd = requiredMaybeStates.createOdd();
conversionWatch.stop();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
@ -562,14 +592,19 @@ namespace storm {
// Then compute the reward vector to use in the computation.
storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, choiceFilterAdd, submatrix, model.getColumnVariables());
conversionWatch.start();
std::vector<uint_fast64_t> rowGroupSizes = (submatrix.notZero().existsAbstract(model.getColumnVariables()) || subvector.notZero()).template toAdd<uint_fast64_t>().sumAbstract(model.getNondeterminismVariables()).toVector(odd);
conversionWatch.stop();
// Finally cut away all columns targeting non-maybe states (or non-(maybe or target) states, respectively).
submatrix *= extendMaybeStates ? maybeStatesWithTargetStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>() : maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
// Translate the symbolic matrix/vector to their explicit representations.
conversionWatch.start();
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(std::move(rowGroupSizes), subvector, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), odd, odd);
conversionWatch.stop();
STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");
// Fulfill the solver's requirements.
SolverRequirementsData<ValueType> solverRequirementsData;
if (extendMaybeStates) {

Write Preview
Loading…
Cancel
Save