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

set up SparseSmgRpatlHelper for bounded globally

main
Lukas Posch 4 years ago
parent
ff8c520808
commit
4aee59a15a
2 changed files with 40 additions and 1 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. 40
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  2. 1
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h

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

@ -7,7 +7,7 @@
#include "storm/utility/vector.h"
#include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h"
#include "storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h"
namespace storm {
namespace modelchecker {
@ -106,6 +106,44 @@ namespace storm {
return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x));
}
template<typename ValueType>
MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<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) {
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 safe states - the psiStates.
storm::storage::BitVector relevantStates = psiStates;
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(psiStates, psiStates);
// Reduce the matrix to relevant states
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, psiStates, psiStates, false);
storm::storage::BitVector clippedStatesOfCoalition(psiStates.getNumberOfSetBits());
clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition);
clippedStatesOfCoalition.complement();
// here is the bounded globally game vi helper used
storm::modelchecker::helper::internal::BoundedGloballyGameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
if (produceScheduler) {
viHelper.setProduceScheduler(true);
}
viHelper.performValueIteration(env, x, b, goal.direction());
viHelper.fillResultVector(x, psiStates);
// TODO: i am not sure about that ~psiStates are correct - but I think (~psiStates are unsafe like the ~phiStates before)
// maybe I should create another method for this case
if (produceScheduler) {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~psiStates));
}
return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
}
template class SparseSmgRpatlHelper<double>;
#ifdef STORM_HAVE_CARL
template class SparseSmgRpatlHelper<storm::RationalNumber>;

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

@ -39,6 +39,7 @@ namespace storm {
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(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 = ModelCheckerHint());
static MDPSparseModelCheckingHelperReturnType<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 MDPSparseModelCheckingHelperReturnType<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 MDPSparseModelCheckingHelperReturnType<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);
private:
static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);

Write Preview
Loading…
Cancel
Save