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

WIP computeBoundedUntilProbabilities in SparseSmgRpatlHelper

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
28252a3caf
commit
c2d2c38c28
2 changed files with 166 additions and 35 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. 199
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  2. 2
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h

199
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
View File

@ -1,3 +1,4 @@
#include <utility/graph.h>
#include "SparseSmgRpatlHelper.h"
#include "storm/environment/Environment.h"
@ -5,9 +6,8 @@
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h"
#include "storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h"
namespace storm {
namespace modelchecker {
@ -19,44 +19,56 @@ namespace storm {
auto solverEnv = env;
solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false);
// Initialize the solution vector.
std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
// Relevant states are those states which are phiStates and not PsiStates.
storm::storage::BitVector relevantStates = phiStates & ~psiStates;
// TODO: check if relevantStates should be used for the size of x
// Initialize the x vector and solution vector result.
//std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
STORM_LOG_DEBUG("statesOfCoalition: " << statesOfCoalition);
storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
clippedStatesOfCoalition.complement();
storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(transitionMatrix, clippedStatesOfCoalition);
STORM_LOG_DEBUG("clippedStatesOfCoalition" << clippedStatesOfCoalition);
//clippedStatesOfCoalition.complement();
//STORM_LOG_DEBUG("clippedStatesOfCoalition" << clippedStatesOfCoalition);
if(!relevantStates.empty()) {
// Reduce the matrix to relevant states.
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
// Update the GameViHelper.
viHelper = storm::modelchecker::helper::internal::GameViHelper<ValueType>(submatrix, clippedStatesOfCoalition);
// Create GameViHelper for computations.
storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
if (produceScheduler) {
viHelper.setProduceScheduler(true);
}
// Perform value iteration.
viHelper.performValueIteration(env, x, b, goal.direction());
if(goal.isShieldingTask()) {
viHelper.getChoiceValues(env, x, constrainedChoiceValues);
}
}
// Fill up the result x with 0s and 1s for not relevant states.
viHelper.fillResultVector(x, relevantStates, psiStates);
// Fill up the constrainedChoice Values to full size.
viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
// Fill up the constrainedChoice Values to full size.
viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
if (produceScheduler) {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
if (produceScheduler) {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
}
}
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
// Fill up the result vector with the values of x for the relevant states, with 1s for psi states (0 is default)
storm::utility::vector::setVectorValues(result, relevantStates, x);
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
STORM_LOG_DEBUG(result);
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
}
template<typename ValueType>
@ -85,6 +97,8 @@ namespace storm {
// The psiStates are flipped, then the true U part is calculated, at the end the result is flipped again.
storm::storage::BitVector notPsiStates = ~psiStates;
statesOfCoalition.complement();
STORM_LOG_DEBUG(statesOfCoalition);
auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint);
for (auto& element : result.values) {
element = storm::utility::one<ValueType>() - element;
@ -92,27 +106,31 @@ namespace storm {
for (auto& element : result.choiceValues) {
element = storm::utility::one<ValueType>() - element;
}
STORM_LOG_DEBUG(result.values);
return result;
}
template<typename ValueType>
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
// Create vector x for result, bitvector allStates with a true for each state and a vector b for the probability for each state to get to a psi state, choiceValues is to store choices for shielding.
std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
// Create vector result, bitvector allStates with a true for each state and a vector b for the probability for each state to get to a psi state, choiceValues is to store choices for shielding.
std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
storm::storage::BitVector allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates);
std::vector<ValueType> choiceValues = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
statesOfCoalition.complement();
STORM_LOG_DEBUG(statesOfCoalition);
if (produceScheduler) {
STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true.");
}
// Create a multiplier for reduction.
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), x, &statesOfCoalition);
multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition);
if (goal.isShieldingTask()) {
choiceValues = b;
}
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(allStates), nullptr, std::move(choiceValues));
STORM_LOG_DEBUG(result);
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(allStates), nullptr, std::move(choiceValues));
}
template<typename ValueType>
@ -123,35 +141,148 @@ namespace storm {
// Relevant states are safe states - the psiStates.
storm::storage::BitVector relevantStates = psiStates;
// Initialize the solution vector.
// Initializations.
std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::one<ValueType>());
std::vector<ValueType> b = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero<ValueType>());
std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero<ValueType>());
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
clippedStatesOfCoalition.complement();
//clippedStatesOfCoalition.complement();
STORM_LOG_DEBUG(clippedStatesOfCoalition);
// Use the bounded globally game vi helper.
storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(transitionMatrix, clippedStatesOfCoalition);
if(!relevantStates.empty() && upperBound > 0) {
// Reduce the matrix to relevant states.
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
// Update the BoundedGloballyViHelper.
// Create GameViHelper for computations.
storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
if (produceScheduler) {
viHelper.setProduceScheduler(true);
}
viHelper.performValueIterationUpperBound(env, x, goal.direction(), upperBound, constrainedChoiceValues);
viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues);
viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
if (produceScheduler) {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates));
}
}
viHelper.fillResultVector(x, relevantStates);
viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
// Fill up the result vector with the values of x for the relevant states (0 is default)
storm::utility::vector::setVectorValues(result, relevantStates, x);
STORM_LOG_DEBUG(result);
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
}
template<typename ValueType>
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint,uint64_t lowerBound, uint64_t upperBound) {
STORM_LOG_DEBUG("lowerBound = " << lowerBound);
STORM_LOG_DEBUG("upperBound = " << upperBound);
auto solverEnv = env;
solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false);
// relevantStates are default all set
// if the upper bound is 0 a psiState cannot be passed between 0 and the lower bound - we can reduce the relevant states and fill the psi states in the result with 1s.
//storm::storage::BitVector relevantStates(transitionMatrix.getRowGroupCount(), true);
storm::storage::BitVector relevantStates = phiStates & ~psiStates;
storm::storage::BitVector makeZeroColumns;
/* if (goal.minimize()) {
relevantStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, upperBound);
} else {
relevantStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, upperBound);
}*/
/* if(lowerBound == 0) {
STORM_LOG_DEBUG("LOWER BOUND = 0, relevant states are the not-psiStates");
relevantStates = phiStates & ~psiStates;
}*/ /*else {
STORM_LOG_DEBUG("LOWER BOUND !=0, relevant states are all states, makeZeroColumns = psiStates");
makeZeroColumns = psiStates;
}*/
STORM_LOG_DEBUG("relevantStates = " << relevantStates);
// Initializations.
std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero<ValueType>());
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
if (produceScheduler) {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates));
}
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
//clippedStatesOfCoalition.complement();
STORM_LOG_DEBUG(clippedStatesOfCoalition);
if(!relevantStates.empty() && upperBound > 0) {
// Reduce the matrix to relevant states. - relevant states are all states
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false, makeZeroColumns);
// Create GameViHelper for computations.
storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
if (produceScheduler) {
viHelper.setProduceScheduler(true);
}
if(lowerBound == 0) {
STORM_LOG_DEBUG("LOWER BOUND = 0 ...");
STORM_LOG_DEBUG("Just peform Value Iteration with an UPPER BOUND.");
viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues);
} else {
STORM_LOG_DEBUG("LOWER BOUND != 0 ...");
// TODO: change the computation: first the diff, then till the lowerBound
STORM_LOG_DEBUG("first multiplication ...");
viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound + 1, constrainedChoiceValues);
STORM_LOG_DEBUG("x = " << x);
STORM_LOG_DEBUG("b = " << b);
STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues);
STORM_LOG_DEBUG("Reduction for ~phiStates ...");
/* for(uint rowGroupIndex = 0; rowGroupIndex < submatrix.getRowGroupCount(); rowGroupIndex++) {
for(uint rowIndex = 0; rowIndex < submatrix.getRowGroupSize(rowGroupIndex); rowIndex++) {
if(!phiStates.get(rowGroupIndex)) {
constrainedChoiceValues.at(rowGroupIndex) = storm::utility::zero<ValueType>();
}
}
}*/
STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues);
//storm::storage::BitVector newRelevantStates(x.size(), false);
//storm::utility::vector::setNonzeroIndices(x, newRelevantStates);
//storm::utility::vector::setVectorValues(x, ~phiStates, storm::utility::zero<ValueType>());
STORM_LOG_DEBUG("reset x ...");
x = std::vector<ValueType>(x.size(), storm::utility::zero<ValueType>());
STORM_LOG_DEBUG("x = " << x);
STORM_LOG_DEBUG("second multiplication ...");
viHelper.performValueIterationUpperBound(env, x, constrainedChoiceValues, goal.direction(), lowerBound, constrainedChoiceValues);
STORM_LOG_DEBUG("x = " << x);
STORM_LOG_DEBUG("b = " << b);
STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues);
/*
viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound + 1, constrainedChoiceValues);
submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
viHelper.updateTransitionMatrix(submatrix);
b = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), lowerBound - 1, constrainedChoiceValues);
*/
}
viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
if (produceScheduler) {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates));
}
storm::utility::vector::setVectorValues(result, relevantStates, x);
}
if(lowerBound == 0) {
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
}
STORM_LOG_DEBUG(result);
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
}
template class SparseSmgRpatlHelper<double>;

2
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
View File

@ -38,10 +38,10 @@ namespace storm {
static SMGSparseModelCheckingHelperReturnType<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
static SMGSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound);
static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound);
private:
static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);
static void expandChoiceValues(std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector<ValueType> const& constrainedChoiceValues, std::vector<ValueType>& choiceValues);
};
}
}

Write Preview
Loading…
Cancel
Save