Browse Source
Merge pull request 'Merge simple reachability for SMG' (#5) from smg_reachability into main
Merge pull request 'Merge simple reachability for SMG' (#5) from smg_reachability into main
Reviewed-on: http://git.pranger.xyz/TEMPEST/tempest-devel/pulls/5 Going to receive a major cleanup just as #4main
14 changed files with 633 additions and 142 deletions
-
2src/storm/api/verification.h
-
3src/storm/logic/FragmentSpecification.cpp
-
10src/storm/logic/PlayerCoalition.cpp
-
2src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
-
65src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
-
23src/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
-
1src/storm/models/sparse/Smg.cpp
-
2src/storm/solver/GmmxxMultiplier.cpp
-
6src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@ -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