Browse Source
init rpatl mc and helper
init rpatl mc and helper
This - adds a temporary GameViHelper, needs refactoring in the future - additional methods to rpatlMC and an - rpatl helper.tempestpy_adaptions
6 changed files with 466 additions and 38 deletions
-
81src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
-
4src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h
-
97src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
-
47src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
-
198src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
-
77src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h
@ -0,0 +1,97 @@ |
|||||
|
#include "SparseSmgRpatlHelper.h"
|
||||
|
|
||||
|
#include "storm/environment/Environment.h"
|
||||
|
#include "storm/environment/solver/MultiplierEnvironment.h"
|
||||
|
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
|
||||
|
#include "storm/solver/MinMaxLinearEquationSolver.h"
|
||||
|
#include "storm/utility/vector.h"
|
||||
|
|
||||
|
#include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h"
|
||||
|
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<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) { |
||||
|
// TODO add Kwiatkowska original reference
|
||||
|
// TODO FIX solver min max mess
|
||||
|
|
||||
|
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>()); |
||||
|
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); |
||||
|
|
||||
|
// Reduce matrix to ~Prob1 states-
|
||||
|
//STORM_LOG_DEBUG("\n" << transitionMatrix);
|
||||
|
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false); |
||||
|
//STORM_LOG_DEBUG("\n" << submatrix);
|
||||
|
|
||||
|
|
||||
|
//STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x));
|
||||
|
//STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b));
|
||||
|
|
||||
|
storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits()); |
||||
|
//STORM_LOG_DEBUG(psiStates);
|
||||
|
//STORM_LOG_DEBUG(statesOfCoalition);
|
||||
|
//STORM_LOG_DEBUG(clippedStatesOfCoalition);
|
||||
|
|
||||
|
// TODO move this to BitVector-class
|
||||
|
auto clippedStatesCounter = 0; |
||||
|
for(uint i = 0; i < psiStates.size(); i++) { |
||||
|
std::cout << i << " : " << psiStates.get(i) << " -> " << statesOfCoalition[i] << std::endl; |
||||
|
if(!psiStates.get(i)) { |
||||
|
clippedStatesOfCoalition.set(clippedStatesCounter, statesOfCoalition[i]); |
||||
|
clippedStatesCounter++; |
||||
|
} |
||||
|
} |
||||
|
//STORM_LOG_DEBUG(clippedStatesOfCoalition);
|
||||
|
clippedStatesOfCoalition.complement(); |
||||
|
//STORM_LOG_DEBUG(clippedStatesOfCoalition);
|
||||
|
|
||||
|
storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition); |
||||
|
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler; |
||||
|
if (produceScheduler) { |
||||
|
viHelper.setProduceScheduler(true); |
||||
|
} |
||||
|
|
||||
|
viHelper.performValueIteration(env, x, b, goal.direction()); |
||||
|
|
||||
|
STORM_LOG_DEBUG(storm::utility::vector::toString(x)); |
||||
|
if (produceScheduler) { |
||||
|
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates)); |
||||
|
STORM_LOG_DEBUG("IsPartial?" << scheduler->isPartialScheduler()); |
||||
|
} |
||||
|
return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler)); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates) { |
||||
|
//STORM_LOG_DEBUG(psiStates.size());
|
||||
|
for(uint i = 0; i < 2; i++) { |
||||
|
//STORM_LOG_DEBUG(scheduler.getChoice(i));
|
||||
|
} |
||||
|
storm::storage::Scheduler<ValueType> completeScheduler(psiStates.size()); |
||||
|
uint_fast64_t maybeStatesCounter = 0; |
||||
|
for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) { |
||||
|
//STORM_LOG_DEBUG(stateCounter << " : " << psiStates.get(stateCounter));
|
||||
|
if(psiStates.get(stateCounter)) { |
||||
|
completeScheduler.setChoice(0, stateCounter); |
||||
|
} else { |
||||
|
completeScheduler.setChoice(scheduler.getChoice(maybeStatesCounter), stateCounter); |
||||
|
maybeStatesCounter++; |
||||
|
} |
||||
|
} |
||||
|
return completeScheduler; |
||||
|
} |
||||
|
|
||||
|
template class SparseSmgRpatlHelper<double>; |
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template class SparseSmgRpatlHelper<storm::RationalNumber>; |
||||
|
#endif
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,47 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include <vector> |
||||
|
|
||||
|
#include "storm/modelchecker/hints/ModelCheckerHint.h" |
||||
|
#include "storm/modelchecker/prctl/helper/SolutionType.h" |
||||
|
#include "storm/storage/SparseMatrix.h" |
||||
|
|
||||
|
#include "storm/utility/solver.h" |
||||
|
#include "storm/solver/SolveGoal.h" |
||||
|
|
||||
|
#include "storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
|
||||
|
class Environment; |
||||
|
|
||||
|
namespace storage { |
||||
|
class BitVector; |
||||
|
} |
||||
|
|
||||
|
namespace models { |
||||
|
namespace sparse { |
||||
|
template <typename ValueType> |
||||
|
class StandardRewardModel; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
namespace modelchecker { |
||||
|
class CheckResult; |
||||
|
|
||||
|
namespace helper { |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
class SparseSmgRpatlHelper { |
||||
|
public: |
||||
|
// TODO should probably be renamed in the future: |
||||
|
|
||||
|
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()); |
||||
|
|
||||
|
private: |
||||
|
static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates); |
||||
|
|
||||
|
}; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,198 @@ |
|||||
|
#include "GameViHelper.h"
|
||||
|
|
||||
|
#include "storm/environment/Environment.h"
|
||||
|
#include "storm/environment/solver/SolverEnvironment.h"
|
||||
|
#include "storm/environment/solver/GameSolverEnvironment.h"
|
||||
|
|
||||
|
|
||||
|
#include "storm/utility/SignalHandler.h"
|
||||
|
#include "storm/utility/vector.h"
|
||||
|
|
||||
|
// TODO this will undergo major refactoring as soon as we implement model checking of further properties
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
namespace internal { |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
GameViHelper<ValueType>::GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void GameViHelper<ValueType>::prepareSolversAndMultipliersReachability(const Environment& env) { |
||||
|
// TODO we get whole transitionmatrix and psistates DONE IN smgrpatlhelper
|
||||
|
// -> clip statesofcoalition
|
||||
|
// -> compute b vector from psiStates
|
||||
|
// -> clip transitionmatrix and create multiplier
|
||||
|
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix); |
||||
|
_multiplier->setOptimizationDirectionOverride(_statesOfCoalition); |
||||
|
|
||||
|
_x1IsCurrent = false; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) { |
||||
|
prepareSolversAndMultipliersReachability(env); |
||||
|
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision()); |
||||
|
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); |
||||
|
_b = b; |
||||
|
|
||||
|
_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>()); |
||||
|
_x2 = _x1; |
||||
|
|
||||
|
if (this->isProduceSchedulerSet()) { |
||||
|
if (!this->_producedOptimalChoices.is_initialized()) { |
||||
|
this->_producedOptimalChoices.emplace(); |
||||
|
} |
||||
|
this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); |
||||
|
} |
||||
|
|
||||
|
uint64_t iter = 0; |
||||
|
std::vector<ValueType> result = x; |
||||
|
while (iter < maxIter) { |
||||
|
++iter; |
||||
|
performIterationStep(env, dir); |
||||
|
|
||||
|
if (checkConvergence(precision)) { |
||||
|
break; |
||||
|
} |
||||
|
if (storm::utility::resources::isTerminate()) { |
||||
|
break; |
||||
|
} |
||||
|
} |
||||
|
x = xNew(); |
||||
|
|
||||
|
if (isProduceSchedulerSet()) { |
||||
|
// We will be doing one more iteration step and track scheduler choices this time.
|
||||
|
performIterationStep(env, dir, &_producedOptimalChoices.get()); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void GameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) { |
||||
|
if (!_multiplier) { |
||||
|
prepareSolversAndMultipliersReachability(env); |
||||
|
} |
||||
|
_x1IsCurrent = !_x1IsCurrent; |
||||
|
|
||||
|
// multiplyandreducegaussseidel
|
||||
|
// Ax + b
|
||||
|
if (choices == nullptr) { |
||||
|
//STORM_LOG_DEBUG("\n" << _transitionMatrix);
|
||||
|
//STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld()));
|
||||
|
//STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b));
|
||||
|
//STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew()));
|
||||
|
_multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew()); |
||||
|
//std::cin.get();
|
||||
|
} else { |
||||
|
// Also keep track of the choices made.
|
||||
|
_multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices); |
||||
|
} |
||||
|
|
||||
|
// compare applyPointwise
|
||||
|
storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { |
||||
|
if(storm::solver::maximize(dir)) { |
||||
|
if(a > b) return a; |
||||
|
else return b; |
||||
|
} else { |
||||
|
if(a > b) return a; |
||||
|
else return b; |
||||
|
} |
||||
|
}); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
bool GameViHelper<ValueType>::checkConvergence(ValueType threshold) const { |
||||
|
STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); |
||||
|
|
||||
|
// Now check whether the currently produced results are precise enough
|
||||
|
STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold."); |
||||
|
auto x1It = xOld().begin(); |
||||
|
auto x1Ite = xOld().end(); |
||||
|
auto x2It = xNew().begin(); |
||||
|
ValueType maxDiff = (*x2It - *x1It); |
||||
|
ValueType minDiff = maxDiff; |
||||
|
// The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now.
|
||||
|
for (++x1It, ++x2It; x1It != x1Ite; ++x1It, ++x2It) { |
||||
|
ValueType diff = (*x2It - *x1It); |
||||
|
// Potentially update maxDiff or minDiff
|
||||
|
bool skipCheck = false; |
||||
|
if (maxDiff < diff) { |
||||
|
maxDiff = diff; |
||||
|
} else if (minDiff > diff) { |
||||
|
minDiff = diff; |
||||
|
} else { |
||||
|
skipCheck = true; |
||||
|
} |
||||
|
// Check convergence
|
||||
|
if (!skipCheck && (maxDiff - minDiff) > threshold) { |
||||
|
return false; |
||||
|
} |
||||
|
} |
||||
|
// TODO needs checking
|
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void GameViHelper<ValueType>::setProduceScheduler(bool value) { |
||||
|
_produceScheduler = value; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
bool GameViHelper<ValueType>::isProduceSchedulerSet() const { |
||||
|
return _produceScheduler; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
std::vector<uint64_t> const& GameViHelper<ValueType>::getProducedOptimalChoices() const { |
||||
|
STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); |
||||
|
STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); |
||||
|
return this->_producedOptimalChoices.get(); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
std::vector<uint64_t>& GameViHelper<ValueType>::getProducedOptimalChoices() { |
||||
|
STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); |
||||
|
STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); |
||||
|
return this->_producedOptimalChoices.get(); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
storm::storage::Scheduler<ValueType> GameViHelper<ValueType>::extractScheduler() const{ |
||||
|
auto const& optimalChoices = getProducedOptimalChoices(); |
||||
|
storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size()); |
||||
|
for (uint64_t state = 0; state < optimalChoices.size(); ++state) { |
||||
|
scheduler.setChoice(optimalChoices[state], state); |
||||
|
} |
||||
|
return scheduler; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
std::vector<ValueType>& GameViHelper<ValueType>::xNew() { |
||||
|
return _x1IsCurrent ? _x1 : _x2; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
std::vector<ValueType> const& GameViHelper<ValueType>::xNew() const { |
||||
|
return _x1IsCurrent ? _x1 : _x2; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
std::vector<ValueType>& GameViHelper<ValueType>::xOld() { |
||||
|
return _x1IsCurrent ? _x2 : _x1; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
std::vector<ValueType> const& GameViHelper<ValueType>::xOld() const { |
||||
|
return _x1IsCurrent ? _x2 : _x1; |
||||
|
} |
||||
|
|
||||
|
template class GameViHelper<double>; |
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template class GameViHelper<storm::RationalNumber>; |
||||
|
#endif
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,77 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "storm/storage/SparseMatrix.h" |
||||
|
#include "storm/solver/LinearEquationSolver.h" |
||||
|
#include "storm/solver/MinMaxLinearEquationSolver.h" |
||||
|
#include "storm/solver/Multiplier.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
class Environment; |
||||
|
|
||||
|
namespace storage { |
||||
|
template <typename VT> class Scheduler; |
||||
|
} |
||||
|
|
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
namespace internal { |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
class GameViHelper { |
||||
|
public: |
||||
|
GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition); |
||||
|
|
||||
|
void prepareSolversAndMultipliersReachability(const Environment& env); |
||||
|
|
||||
|
void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir); |
||||
|
|
||||
|
/*h |
||||
|
* Sets whether an optimal scheduler shall be constructed during the computation |
||||
|
*/ |
||||
|
void setProduceScheduler(bool value); |
||||
|
|
||||
|
/*! |
||||
|
* @return whether an optimal scheduler shall be constructed during the computation |
||||
|
*/ |
||||
|
bool isProduceSchedulerSet() const; |
||||
|
|
||||
|
storm::storage::Scheduler<ValueType> extractScheduler() const; |
||||
|
private: |
||||
|
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr); |
||||
|
|
||||
|
/*! |
||||
|
* Checks whether the curently computed value achieves the desired precision |
||||
|
*/ |
||||
|
bool checkConvergence(ValueType precision) const; |
||||
|
|
||||
|
std::vector<ValueType>& xNew(); |
||||
|
std::vector<ValueType> const& xNew() const; |
||||
|
|
||||
|
std::vector<ValueType>& xOld(); |
||||
|
std::vector<ValueType> const& xOld() const; |
||||
|
bool _x1IsCurrent; |
||||
|
|
||||
|
/*! |
||||
|
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled. |
||||
|
* @return the produced scheduler of the most recent call. |
||||
|
*/ |
||||
|
std::vector<uint64_t> const& getProducedOptimalChoices() const; |
||||
|
|
||||
|
/*! |
||||
|
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled. |
||||
|
* @return the produced scheduler of the most recent call. |
||||
|
*/ |
||||
|
std::vector<uint64_t>& getProducedOptimalChoices(); |
||||
|
|
||||
|
storm::storage::SparseMatrix<ValueType> _transitionMatrix; |
||||
|
storm::storage::BitVector _statesOfCoalition; |
||||
|
std::vector<ValueType> _x1, _x2, _b; |
||||
|
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier; |
||||
|
|
||||
|
bool _produceScheduler = false; |
||||
|
boost::optional<std::vector<uint64_t>> _producedOptimalChoices; |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue