From 9e875adea9722c1cf02f452e3fbb531f6b110f5d Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 27 Feb 2018 12:55:27 +0100 Subject: [PATCH] Using Multiplier in CTMC and DTMC model checkers --- .../csl/helper/SparseCtmcCslHelper.cpp | 11 ++++---- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 17 ++++++------ .../prctl/helper/SparseDtmcPrctlHelper.cpp | 26 +++++++++---------- 3 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 90d556133..5bf12da1f 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -9,6 +9,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/Multiplier.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" @@ -671,18 +672,16 @@ namespace storm { } } - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(uniformizedMatrix), storm::solver::LinearEquationSolverTask::Multiply); - solver->setCachingEnabled(true); - + auto multiplier = storm::solver::MultiplierFactory().create(env, uniformizedMatrix); if (!useMixedPoissonProbabilities && foxGlynnResult.left > 1) { // Perform the matrix-vector multiplications (without adding). - solver->repeatedMultiply(values, addVector, foxGlynnResult.left - 1); + multiplier->repeatedMultiply(env, values, addVector, foxGlynnResult.left - 1); } else if (useMixedPoissonProbabilities) { std::function addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; }; // For the iterations below the left truncation point, we need to add and scale the result with the uniformization rate. for (uint_fast64_t index = 1; index < startingIteration; ++index) { - solver->repeatedMultiply(values, nullptr, 1); + multiplier->multiply(env, values, nullptr, values); storm::utility::vector::applyPointwise(result, values, result, addAndScale); } } @@ -692,7 +691,7 @@ namespace storm { ValueType weight = 0; std::function addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; }; for (uint_fast64_t index = startingIteration; index <= foxGlynnResult.right; ++index) { - solver->repeatedMultiply(values, addVector, 1); + multiplier->multiply(env, values, addVector, values); weight = foxGlynnResult.weights[index - foxGlynnResult.left]; storm::utility::vector::applyPointwise(result, values, result, addAndScale); diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 280c5aaff..ca8f7e439 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -3,6 +3,7 @@ #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/Multiplier.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" @@ -145,9 +146,9 @@ namespace storm { storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector b = subvector.toVector(odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitSubmatrix), storm::solver::LinearEquationSolverTask::Multiply); - solver->repeatedMultiply(x, &b, stepBound); - + auto multiplier = storm::solver::MultiplierFactory().create(env, explicitSubmatrix); + multiplier->repeatedMultiply(env, x, &b, stepBound); + // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd(), maybeStates, odd, x)); } else { @@ -170,9 +171,9 @@ namespace storm { storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(odd, odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix), storm::solver::LinearEquationSolverTask::Multiply); - solver->repeatedMultiply(x, nullptr, stepBound); - + auto multiplier = storm::solver::MultiplierFactory().create(env, explicitMatrix); + multiplier->repeatedMultiply(env, x, nullptr, stepBound); + // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); } @@ -196,8 +197,8 @@ namespace storm { std::vector b = totalRewardVector.toVector(odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix), storm::solver::LinearEquationSolverTask::Multiply); - solver->repeatedMultiply(x, &b, stepBound); + auto multiplier = storm::solver::MultiplierFactory().create(env, explicitMatrix); + multiplier->repeatedMultiply(env, x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index f10e1155e..1fe8ca527 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -11,6 +11,7 @@ #include "storm/storage/ConsecutiveUint64DynamicPriorityQueue.h" #include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/Multiplier.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" @@ -69,10 +70,9 @@ namespace storm { // Create the vector with which to multiply. std::vector subresult(maybeStates.getNumberOfSetBits()); - // Perform the matrix vector multiplication as often as required by the formula bound. - goal.restrictRelevantValues(maybeStates); - std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix), storm::solver::LinearEquationSolverTask::Multiply); - solver->repeatedMultiply(subresult, &b, stepBound); + // Perform the matrix vector multiplication + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + multiplier->repeatedMultiply(env, subresult, &b, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); @@ -116,9 +116,9 @@ namespace storm { // Update some data for the case that the Matrix has changed if (epochModel.epochMatrixChanged) { x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); - linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix, storm::solver::LinearEquationSolverTask::SolveEquations); + linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix); linEqSolver->setCachingEnabled(true); - auto req = linEqSolver->getRequirements(env, storm::solver::LinearEquationSolverTask::SolveEquations); + auto req = linEqSolver->getRequirements(env); if (lowerBound) { linEqSolver->setLowerBound(lowerBound.get()); req.clearLowerBounds(); @@ -345,8 +345,8 @@ namespace storm { storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); // Perform one single matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, transitionMatrix, storm::solver::LinearEquationSolverTask::Multiply); - solver->repeatedMultiply(result, nullptr, 1); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->multiply(env, result, nullptr, result); return result; } @@ -359,8 +359,8 @@ namespace storm { std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); // Perform the matrix vector multiplication as often as required by the formula bound. - std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, transitionMatrix, storm::solver::LinearEquationSolverTask::Multiply); - solver->repeatedMultiply(result, &totalRewardVector, stepBound); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->repeatedMultiply(env, result, &totalRewardVector, stepBound); return result; } @@ -374,9 +374,9 @@ namespace storm { std::vector result = rewardModel.getStateRewardVector(); // Perform the matrix vector multiplication as often as required by the formula bound. - std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, transitionMatrix); - solver->repeatedMultiply(result, nullptr, stepCount); - + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->repeatedMultiply(env, result, nullptr, stepCount); + return result; }