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

Using Multiplier in CTMC and DTMC model checkers

tempestpy_adaptions
TimQu 7 years ago
parent
541810f3b2
commit
9e875adea9
3 changed files with 27 additions and 27 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. 11
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  2. 17
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  3. 26
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

11
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -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<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(uniformizedMatrix), storm::solver::LinearEquationSolverTask::Multiply);
solver->setCachingEnabled(true);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().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<ValueType(ValueType const&, ValueType const&)> 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<ValueType(ValueType const&, ValueType const&)> 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);

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

@ -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<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
std::vector<ValueType> b = subvector.toVector(odd);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitSubmatrix), storm::solver::LinearEquationSolverTask::Multiply);
solver->repeatedMultiply(x, &b, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitSubmatrix);
multiplier->repeatedMultiply(env, x, &b, stepBound);
// Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd<ValueType>(), maybeStates, odd, x));
} else {
@ -170,9 +171,9 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitMatrix = transitionMatrix.toMatrix(odd, odd);
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix), storm::solver::LinearEquationSolverTask::Multiply);
solver->repeatedMultiply(x, nullptr, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitMatrix);
multiplier->repeatedMultiply(env, x, nullptr, stepBound);
// Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
}
@ -196,8 +197,8 @@ namespace storm {
std::vector<ValueType> b = totalRewardVector.toVector(odd);
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix), storm::solver::LinearEquationSolverTask::Multiply);
solver->repeatedMultiply(x, &b, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitMatrix);
multiplier->repeatedMultiply(env, x, &b, stepBound);
// Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));

26
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -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<ValueType> subresult(maybeStates.getNumberOfSetBits());
// Perform the matrix vector multiplication as often as required by the formula bound.
goal.restrictRelevantValues(maybeStates);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> 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<ValueType>().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<ValueType>());
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<ValueType>());
// Perform one single matrix-vector multiplication.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, transitionMatrix, storm::solver::LinearEquationSolverTask::Multiply);
solver->repeatedMultiply(result, nullptr, 1);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->multiply(env, result, nullptr, result);
return result;
}
@ -359,8 +359,8 @@ namespace storm {
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
// Perform the matrix vector multiplication as often as required by the formula bound.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, transitionMatrix, storm::solver::LinearEquationSolverTask::Multiply);
solver->repeatedMultiply(result, &totalRewardVector, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->repeatedMultiply(env, result, &totalRewardVector, stepBound);
return result;
}
@ -374,9 +374,9 @@ namespace storm {
std::vector<ValueType> result = rewardModel.getStateRewardVector();
// Perform the matrix vector multiplication as often as required by the formula bound.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, transitionMatrix);
solver->repeatedMultiply(result, nullptr, stepCount);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->repeatedMultiply(env, result, nullptr, stepCount);
return result;
}

Write Preview
Loading…
Cancel
Save