From 51ebb47587a284c8528e05de6f9619453b415e96 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 5 Mar 2018 12:08:44 +0100 Subject: [PATCH] added timing measurements to symbolic to sparse conversion in hybrid model checkers --- .../csl/helper/HybridCtmcCslHelper.cpp | 75 ++++++++++++++++--- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 56 +++++++++++--- .../prctl/helper/HybridMdpPrctlHelper.cpp | 55 +++++++++++--- 3 files changed, 155 insertions(+), 31 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index dcd589378..841088ac2 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -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 b = (statesWithProbabilityGreater0NonPsi.template toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd()).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 explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); std::vector 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 values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); @@ -106,12 +112,18 @@ namespace storm { // Filter the unbounded result such that it only contains values for the relevant states. unboundedResult->filter(SymbolicQualitativeCheckResult(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 result; if (unboundedResult->isHybridQuantitativeCheckResult()) { + conversionWatch.start(); std::unique_ptr explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult().toExplicitQuantitativeCheckResult(); + conversionWatch.stop(); result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult().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 uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); + conversionWatch.start(); storm::storage::SparseMatrix 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(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result); @@ -146,10 +161,12 @@ namespace storm { storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.template toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd()).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 explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); std::vector explicitB = b.toVector(odd); - + conversionWatch.stop(); + // Compute the transient probabilities. std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); std::vector 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(model.getReachableStates(), relevantStates)); - + // Build an ODD for the relevant states. + conversionWatch.start(); odd = relevantStates.createOdd(); std::unique_ptr explicitResult = hybridResult.toExplicitQuantitativeCheckResult(); + conversionWatch.stop(); std::vector newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult().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() * 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(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero(), 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 newSubresult = psiStates.template toAdd().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() * exitRateVector).getMax(); @@ -205,8 +231,11 @@ namespace storm { // Finally, we compute the second set of transient probabilities. storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate); + conversionWatch.start(); storm::storage::SparseMatrix 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(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(), model.getManager().template getAddZero(), 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 result = rewardModel.getStateRewardVector().toVector(odd); @@ -242,7 +275,11 @@ namespace storm { storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); + conversionWatch.start(); storm::storage::SparseMatrix 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(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 uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); + conversionWatch.start(); storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + conversionWatch.stop(); // Then compute the state reward vector to use in the computation. storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false); std::vector 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 result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); @@ -295,12 +340,16 @@ namespace storm { std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates) { storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + storm::utility::Stopwatch conversionWatch(true); + // Create ODD for the translation. storm::dd::Odd odd = model.getReachableStates().createOdd(); storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(env, storm::solver::SolveGoal(), explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), 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 probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + storm::utility::Stopwatch conversionWatch(true); + // Create ODD for the translation. storm::dd::Odd odd = model.getReachableStates().createOdd(); storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(), explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index e5a7df87b..b90aa25be 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -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 maybeStatesAdd = maybeStates.template toAdd(); @@ -83,9 +88,12 @@ namespace storm { std::vector x(maybeStates.getNonZeroCount(), storm::utility::convertNumber(0.5)); // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. + conversionWatch.start(); storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector b = subvector.toVector(odd); - + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitSubmatrix)); solver->setBounds(storm::utility::zero(), storm::utility::one()); 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 maybeStatesAdd = maybeStates.template toAdd(); @@ -144,9 +156,12 @@ namespace storm { std::vector x(maybeStates.getNonZeroCount(), storm::utility::zero()); // Translate the symbolic matrix/vector to their explicit representations. + conversionWatch.start(); storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector 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().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 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().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 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 x(model.getNumberOfStates(), storm::utility::zero()); + + 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 explicitMatrix = transitionMatrix.toMatrix(odd, odd); std::vector 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().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 maybeStatesAdd = maybeStates.template toAdd(); @@ -281,9 +308,12 @@ namespace storm { std::vector x(maybeStates.getNonZeroCount(), storm::utility::convertNumber(0.5)); // Translate the symbolic matrix/vector to their explicit representations. + conversionWatch.start(); storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector 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> upperBounds; if (oneStepTargetProbs) { @@ -311,8 +341,11 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates) { // Create ODD for the translation. + storm::utility::Stopwatch conversionWatch(true); storm::dd::Odd odd = model.getReachableStates().createOdd(); storm::storage::SparseMatrix 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 result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(env, storm::solver::SolveGoal(), explicitProbabilityMatrix, targetStates.toVector(odd)); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); @@ -321,9 +354,12 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::Model const& model, storm::dd::Add 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 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 result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(), explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd)); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 47ea6c1b4..90fbd61d0 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -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 maybeStatesAdd = maybeStates.template toAdd(); @@ -191,20 +197,21 @@ namespace storm { submatrix *= extendedMaybeStates.template toAdd().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(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 x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero()); @@ -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 maybeStatesAdd = maybeStates.template toAdd(); @@ -309,8 +324,11 @@ namespace storm { std::vector x(maybeStates.getNonZeroCount(), storm::utility::zero()); // Translate the symbolic matrix/vector to their explicit representations. + conversionWatch.start(); std::pair, std::vector> 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().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 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().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 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 x(model.getNumberOfStates(), storm::utility::zero()); + + 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, std::vector> 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().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 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 maybeStatesAdd = maybeStates.template toAdd(); @@ -562,14 +592,19 @@ namespace storm { // Then compute the reward vector to use in the computation. storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, choiceFilterAdd, submatrix, model.getColumnVariables()); + conversionWatch.start(); std::vector rowGroupSizes = (submatrix.notZero().existsAbstract(model.getColumnVariables()) || subvector.notZero()).template toAdd().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() : maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); // Translate the symbolic matrix/vector to their explicit representations. + conversionWatch.start(); std::pair, std::vector> 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 solverRequirementsData; if (extendMaybeStates) {