48 changed files with 2173 additions and 265 deletions
-
67README.md
-
10resources/3rdparty/cudd-3.0.0/config.h.in
-
32resources/examples/testfiles/smg/example_smg.nm
-
26src/storm-cli-utilities/model-handling.h
-
8src/storm-parsers/parser/FormulaParserGrammar.cpp
-
2src/storm-parsers/parser/FormulaParserGrammar.h
-
14src/storm/api/export.h
-
2src/storm/api/verification.h
-
10src/storm/logic/ShieldExpression.cpp
-
7src/storm/logic/ShieldExpression.h
-
311src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp
-
108src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h
-
63src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
15src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
37src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
4src/storm/modelchecker/results/CheckResult.cpp
-
1src/storm/modelchecker/results/CheckResult.h
-
22src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
-
13src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h
-
69src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
-
99src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
-
3src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
-
371src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
-
136src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
-
10src/storm/settings/modules/IOSettings.cpp
-
11src/storm/settings/modules/IOSettings.h
-
55src/storm/shields/AbstractShield.cpp
-
45src/storm/shields/AbstractShield.h
-
31src/storm/shields/OptimalShield.cpp
-
8src/storm/shields/OptimalShield.h
-
32src/storm/shields/PostShield.cpp
-
8src/storm/shields/PostShield.h
-
34src/storm/shields/PreShield.cpp
-
11src/storm/shields/PreShield.h
-
38src/storm/shields/ShieldHandling.cpp
-
9src/storm/shields/ShieldHandling.h
-
16src/storm/storage/MaximalEndComponent.cpp
-
11src/storm/storage/MaximalEndComponent.h
-
68src/storm/storage/PostScheduler.cpp
-
18src/storm/storage/PostScheduler.h
-
92src/storm/storage/PreScheduler.cpp
-
17src/storm/storage/PreScheduler.h
-
12src/test/storm/logic/FragmentCheckerTest.cpp
-
57src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp
-
117src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp
-
286src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp
-
12src/test/storm/parser/GameShieldingParserTest.cpp
-
10src/test/storm/parser/MdpShieldingParserTest.cpp
@ -1,68 +1,3 @@ |
|||
Storm - A Modern Probabilistic Model Checker |
|||
Tempest - A Shield Synthesis Tool |
|||
============================================ |
|||
|
|||
[](https://github.com/moves-rwth/storm/actions) |
|||
[](https://github.com/moves-rwth/storm/releases/) |
|||
[](https://doi.org/10.5281/zenodo.1181896) |
|||
|
|||
|
|||
For more instructions, check out the documentation found in [Getting Started](http://www.stormchecker.org/getting-started.html). |
|||
|
|||
|
|||
Benchmarks |
|||
---------------------------- |
|||
|
|||
Example input files for Storm can be obtained from |
|||
https://github.com/moves-rwth/storm-examples. |
|||
|
|||
Various Benchmarks together with example invocations of Storm can be found at the [Quantitative Verification Benchmark Set (QVBS)](http://qcomp.org/benchmarks). |
|||
|
|||
Further examples and benchmarks can be found in the following repositories: |
|||
|
|||
* **Prism files** (DTMC, MDP, CTMC): |
|||
http://www.prismmodelchecker.org/benchmarks |
|||
* **Jani files** (DTMC, MDP, CTMC, MA): |
|||
http://jani-spec.org |
|||
* **GSPN**s: |
|||
(private, contact: sebastian.junges@cs.rwth-aachen.de) |
|||
* **DFT**s: |
|||
https://github.com/moves-rwth/dft-examples |
|||
* **PGCL**: |
|||
(private, contact: sebastian.junges@cs.rwth-aachen.de) |
|||
|
|||
|
|||
Authors |
|||
----------------------------- |
|||
Storm has been developed at RWTH Aachen University. |
|||
|
|||
###### Principal developers |
|||
* Christian Hensel |
|||
* Sebastian Junges |
|||
* Joost-Pieter Katoen |
|||
* Tim Quatmann |
|||
* Matthias Volk |
|||
|
|||
###### Developers (lexicographical order) |
|||
* Jana Berger |
|||
* Alexander Bork |
|||
* David Korzeniewski |
|||
* Jip Spel |
|||
|
|||
###### Contributors (lexicographical order) |
|||
* Daniel Basgöze |
|||
* Dimitri Bohlender |
|||
* Harold Bruintjes |
|||
* Michael Deutschen |
|||
* Linus Heck |
|||
* Thomas Heinemann |
|||
* Thomas Henn |
|||
* Tom Janson |
|||
* Jan Karuc |
|||
* Joachim Klein |
|||
* Gereon Kremer |
|||
* Sascha Vincent Kurowski |
|||
* Hannah Mertens |
|||
* Stefan Pranger |
|||
* Svenja Stein |
|||
* Manuel Sascha Weiand |
|||
* Lukas Westhofen |
|||
@ -0,0 +1,32 @@ |
|||
// taken from Julia Eisentraut "Value iteration for simple stochastic games: Stopping criterion |
|||
// and learning algorithm" - Fig. 1 |
|||
|
|||
|
|||
smg |
|||
|
|||
const double p = 2/3; |
|||
|
|||
player maxP |
|||
[q_action1], [q_action2] |
|||
endplayer |
|||
|
|||
player minP |
|||
[p_action1] |
|||
endplayer |
|||
|
|||
player sinkstates |
|||
state_space |
|||
endplayer |
|||
|
|||
|
|||
module state_space |
|||
s : [0..3]; |
|||
|
|||
[p_action1] s=0 -> (s'=1); |
|||
|
|||
[q_action1] s=1 -> (s'=0); |
|||
[q_action2] s=1 -> (1-p) : (s'=1) + (p/2) : (s'=2) + (p/2) : (s'=3); |
|||
|
|||
[] s=2 -> true; |
|||
[] s=3 -> true; |
|||
endmodule |
|||
@ -0,0 +1,311 @@ |
|||
#include "SparseSmgLraHelper.h"
|
|||
|
|||
#include "storm/storage/MaximalEndComponent.h"
|
|||
#include "storm/storage/StronglyConnectedComponent.h"
|
|||
|
|||
#include "storm/utility/graph.h"
|
|||
#include "storm/utility/vector.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/utility/SignalHandler.h"
|
|||
|
|||
#include "storm/environment/solver/SolverEnvironment.h"
|
|||
#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
|
|||
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
|
|||
#include "storm/environment/solver/MultiplierEnvironment.h"
|
|||
#include "storm/environment/solver/GameSolverEnvironment.h"
|
|||
|
|||
#include "modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h"
|
|||
#include "storm/exceptions/UnmetRequirementException.h"
|
|||
|
|||
#define SOLVE_MDP 50
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
namespace internal { |
|||
|
|||
template <typename ValueType> |
|||
SparseSmgLraHelper<ValueType>::SparseSmgLraHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { |
|||
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> SparseSmgLraHelper<ValueType>::computeLongRunAverageRewardsSound(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel) { |
|||
std::vector<ValueType> result; |
|||
std::vector<ValueType> stateRewardsGetter = std::vector<ValueType>(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>()); |
|||
if (rewardModel.hasStateRewards()) { |
|||
stateRewardsGetter = rewardModel.getStateRewardVector(); |
|||
} |
|||
ValueGetter actionRewardsGetter; |
|||
if (rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) { |
|||
if (rewardModel.hasTransitionRewards()) { |
|||
actionRewardsGetter = [&] (uint64_t globalChoiceIndex) { return rewardModel.getStateActionAndTransitionReward(globalChoiceIndex, this->_transitionMatrix); }; |
|||
} else { |
|||
actionRewardsGetter = [&] (uint64_t globalChoiceIndex) { return rewardModel.getStateActionReward(globalChoiceIndex); }; |
|||
} |
|||
} else { |
|||
actionRewardsGetter = [] (uint64_t) { return storm::utility::zero<ValueType>(); }; |
|||
} |
|||
_b = getBVector(stateRewardsGetter, actionRewardsGetter); |
|||
|
|||
// If requested, allocate memory for the choices made
|
|||
if (this->_produceScheduler) { |
|||
if (!this->_producedOptimalChoices.is_initialized()) { |
|||
_producedOptimalChoices.emplace(); |
|||
} |
|||
_producedOptimalChoices->resize(_transitionMatrix.getRowGroupCount()); |
|||
} |
|||
|
|||
prepareMultiplier(env, rewardModel); |
|||
performValueIteration(env, rewardModel, _b, result); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> SparseSmgLraHelper<ValueType>::getBVector(std::vector<ValueType> const& stateRewardsGetter, ValueGetter const& actionRewardsGetter) { |
|||
std::vector<ValueType> b = std::vector<ValueType>(_transitionMatrix.getRowCount()); |
|||
size_t globalChoiceCount = 0; |
|||
auto rowGroupIndices = _transitionMatrix.getRowGroupIndices(); |
|||
for (size_t state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { |
|||
size_t rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; |
|||
for (size_t choice = 0; choice < rowGroupSize; choice++, globalChoiceCount++) |
|||
{ |
|||
b[globalChoiceCount] = stateRewardsGetter[state] + actionRewardsGetter(globalChoiceCount); |
|||
} |
|||
} |
|||
return b; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SparseSmgLraHelper<ValueType>::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel, std::vector<ValueType> const& b, std::vector<ValueType>& result) |
|||
{ |
|||
std::vector<uint64_t> choicesForStrategies = std::vector<uint64_t>(_transitionMatrix.getRowGroupCount(), 0); |
|||
auto precision = storm::utility::convertNumber<ValueType>(env.solver().lra().getPrecision()); |
|||
|
|||
Environment envMinMax = env; |
|||
envMinMax.solver().lra().setPrecision(precision / storm::utility::convertNumber<storm::RationalNumber>(2)); |
|||
do |
|||
{ |
|||
size_t iteration_count = 0; |
|||
// Convergent recommender procedure
|
|||
|
|||
_multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &choicesForStrategies, &_statesOfCoalition); |
|||
|
|||
if (iteration_count % SOLVE_MDP == 0) { // only every 50th iteration
|
|||
storm::storage::BitVector fixedMaxStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MaxStrategy); |
|||
storm::storage::BitVector fixedMinStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MinStrategy); |
|||
|
|||
// compute bounds
|
|||
if (fixedMaxStrat != _fixedMaxStrat) { |
|||
storm::storage::SparseMatrix<ValueType> restrictedMaxMatrix = _transitionMatrix.restrictRows(fixedMaxStrat); |
|||
|
|||
storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> MaxSolver(restrictedMaxMatrix); |
|||
|
|||
MaxSolver.setOptimizationDirection(OptimizationDirection::Minimize); |
|||
MaxSolver.setProduceChoiceValues(false); |
|||
_resultForMax = MaxSolver.computeLongRunAverageRewards(envMinMax, rewardModel); |
|||
_fixedMaxStrat = fixedMaxStrat; |
|||
|
|||
for (size_t i = 0; i < xNewL().size(); i++) { |
|||
xNewL()[i] = std::max(xNewL()[i], _resultForMax[i]); |
|||
} |
|||
} |
|||
|
|||
if (fixedMinStrat != _fixedMinStrat) { |
|||
storm::storage::SparseMatrix<ValueType> restrictedMinMatrix = _transitionMatrix.restrictRows(fixedMinStrat); |
|||
|
|||
storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> MinSolver(restrictedMinMatrix); |
|||
MinSolver.setOptimizationDirection(OptimizationDirection::Maximize); |
|||
MinSolver.setProduceChoiceValues(false); |
|||
_resultForMin = MinSolver.computeLongRunAverageRewards(envMinMax, rewardModel); |
|||
_fixedMinStrat = fixedMinStrat; |
|||
|
|||
for (size_t i = 0; i < xNewU().size(); i++) { |
|||
xNewU()[i] = std::min(xNewU()[i], _resultForMin[i]); |
|||
} |
|||
} |
|||
} |
|||
|
|||
} while (!checkConvergence(precision)); |
|||
|
|||
if (_produceScheduler) { |
|||
_multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &_producedOptimalChoices.get(), &_statesOfCoalition); |
|||
} |
|||
|
|||
if (_produceChoiceValues) { |
|||
if (!this->_choiceValues.is_initialized()) { |
|||
this->_choiceValues.emplace(); |
|||
} |
|||
this->_choiceValues->resize(this->_transitionMatrix.getRowCount()); |
|||
_choiceValues = calcChoiceValues(env, rewardModel); |
|||
} |
|||
result = xNewL(); |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
storm::storage::BitVector SparseSmgLraHelper<ValueType>::getStrategyFixedBitVec(std::vector<uint64_t> const& choices, MinMaxStrategy strategy) { |
|||
storm::storage::BitVector restrictBy(_transitionMatrix.getRowCount(), true); |
|||
auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); |
|||
|
|||
for(uint state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { |
|||
if ((_minimizerStates[state] && strategy == MinMaxStrategy::MaxStrategy) || (!_minimizerStates[state] && strategy == MinMaxStrategy::MinStrategy)) |
|||
continue; |
|||
|
|||
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; |
|||
for(uint rowGroupIndex = 0; rowGroupIndex < rowGroupSize; rowGroupIndex++) { |
|||
if ((rowGroupIndex) != choices[state]) { |
|||
restrictBy.set(rowGroupIndex + rowGroupIndices[state], false); |
|||
} |
|||
} |
|||
} |
|||
return restrictBy; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> SparseSmgLraHelper<ValueType>::calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel) { |
|||
std::vector<ValueType> choiceValues(_transitionMatrix.getRowCount()); |
|||
_multiplier->multiply(env, xNewL(), nullptr, choiceValues); |
|||
|
|||
return choiceValues; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> SparseSmgLraHelper<ValueType>::getChoiceValues() const { |
|||
STORM_LOG_ASSERT(_produceChoiceValues, "Trying to get the computed choice values although this was not requested."); |
|||
STORM_LOG_ASSERT(this->_choiceValues.is_initialized(), "Trying to get the computed choice values but none were available. Was there a computation call before?"); |
|||
return this->_choiceValues.get(); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
storm::storage::Scheduler<ValueType> SparseSmgLraHelper<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<uint64_t> const& SparseSmgLraHelper<ValueType>::getProducedOptimalChoices() const { |
|||
STORM_LOG_ASSERT(_produceScheduler, "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> |
|||
void SparseSmgLraHelper<ValueType>::prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel) |
|||
{ |
|||
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix); |
|||
if (_statesOfCoalition.size()) { |
|||
_minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; |
|||
} |
|||
else { |
|||
_minimizerStates = storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), _optimizationDirection == OptimizationDirection::Minimize); |
|||
} |
|||
|
|||
_xL = std::vector<ValueType>(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>()); |
|||
_x = _xL; |
|||
|
|||
_fixedMaxStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); |
|||
_fixedMinStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); |
|||
|
|||
_resultForMin = std::vector<ValueType>(_transitionMatrix.getRowGroupCount()); |
|||
_resultForMax = std::vector<ValueType>(_transitionMatrix.getRowGroupCount()); |
|||
|
|||
_xU = std::vector<ValueType>(_transitionMatrix.getRowGroupCount(), std::numeric_limits<ValueType>::infinity()); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool SparseSmgLraHelper<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 = xNewL().begin(); |
|||
auto x1Ite = xNewL().end(); |
|||
auto x2It = xNewU().begin(); |
|||
for (; x1It != x1Ite; x1It++, x2It++) { |
|||
ValueType diff = (*x2It - *x1It); |
|||
if (diff > threshold) { |
|||
return false; |
|||
} |
|||
} |
|||
return true; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType>& SparseSmgLraHelper<ValueType>::xNewL() { |
|||
return _xL; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> const& SparseSmgLraHelper<ValueType>::xNewL() const { |
|||
return _xL; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType>& SparseSmgLraHelper<ValueType>::xNewU() { |
|||
return _xU; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> const& SparseSmgLraHelper<ValueType>::xNewU() const { |
|||
return _xU; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType>& SparseSmgLraHelper<ValueType>::xNew() { |
|||
return _x; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> const& SparseSmgLraHelper<ValueType>::xNew() const { |
|||
return _x; |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
void SparseSmgLraHelper<ValueType>::setRelevantStates(storm::storage::BitVector relevantStates){ |
|||
_relevantStates = relevantStates; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SparseSmgLraHelper<ValueType>::setValueThreshold(storm::logic::ComparisonType const& comparisonType, const ValueType &thresholdValue) { |
|||
_valueThreshold = std::make_pair(comparisonType, thresholdValue); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SparseSmgLraHelper<ValueType>::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) { |
|||
_optimizationDirection = direction; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SparseSmgLraHelper<ValueType>::setProduceScheduler(bool value) { |
|||
_produceScheduler = value; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SparseSmgLraHelper<ValueType>::setProduceChoiceValues(bool value) { |
|||
_produceChoiceValues = value; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SparseSmgLraHelper<ValueType>::setQualitative(bool value) { |
|||
_isQualitativeSet = value; |
|||
} |
|||
|
|||
template class SparseSmgLraHelper<double>; |
|||
#ifdef STORM_HAVE_CARL
|
|||
template class SparseSmgLraHelper<storm::RationalNumber>; |
|||
#endif
|
|||
|
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,108 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/storage/SparseMatrix.h" |
|||
#include "storm/storage/BitVector.h" |
|||
#include "storm/solver/LinearEquationSolver.h" |
|||
#include "storm/solver/MinMaxLinearEquationSolver.h" |
|||
#include "storm/solver/Multiplier.h" |
|||
#include "storm/logic/ComparisonType.h" |
|||
|
|||
|
|||
namespace storm { |
|||
class Environment; |
|||
|
|||
|
|||
namespace modelchecker { |
|||
namespace helper { |
|||
namespace internal { |
|||
|
|||
enum class MinMaxStrategy { |
|||
MaxStrategy, |
|||
MinStrategy |
|||
}; |
|||
|
|||
template <typename ValueType> |
|||
class SparseSmgLraHelper { |
|||
public: |
|||
// Function mapping from indices to values |
|||
typedef std::function<ValueType(uint64_t)> ValueGetter; |
|||
|
|||
SparseSmgLraHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const statesOfCoalition); |
|||
|
|||
void performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel, std::vector<ValueType> const& b, std::vector<ValueType>& result); |
|||
|
|||
std::vector<ValueType> getChoiceValues() const; |
|||
|
|||
storm::storage::Scheduler<ValueType> extractScheduler() const; |
|||
|
|||
std::vector<uint64_t> const& getProducedOptimalChoices() const; |
|||
|
|||
void prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel); |
|||
|
|||
std::vector<ValueType> computeLongRunAverageRewardsSound(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel); |
|||
|
|||
void setRelevantStates(storm::storage::BitVector relevantStates); |
|||
|
|||
void setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& thresholdValue); |
|||
|
|||
void setOptimizationDirection(storm::solver::OptimizationDirection const& direction); |
|||
|
|||
void setProduceScheduler(bool value); |
|||
|
|||
void setProduceChoiceValues(bool value); |
|||
|
|||
void setQualitative(bool value); |
|||
|
|||
private: |
|||
|
|||
bool checkConvergence(ValueType threshold) const; |
|||
|
|||
storm::storage::BitVector getStrategyFixedBitVec(std::vector<uint64_t> const& choices, MinMaxStrategy strategy); |
|||
|
|||
std::vector<ValueType> getBVector(std::vector<ValueType> const& stateRewardsGetter, ValueGetter const& actionRewardsGetter); |
|||
|
|||
std::vector<ValueType> calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel); |
|||
|
|||
std::vector<ValueType>& xNew(); |
|||
std::vector<ValueType> const& xNew() const; |
|||
|
|||
std::vector<ValueType>& xNewL(); |
|||
std::vector<ValueType> const& xNewL() const; |
|||
|
|||
std::vector<ValueType>& xNewU(); |
|||
std::vector<ValueType> const& xNewU() const; |
|||
|
|||
storm::storage::SparseMatrix<ValueType> const& _transitionMatrix; |
|||
storm::storage::BitVector const _statesOfCoalition; |
|||
|
|||
storm::storage::BitVector _relevantStates; |
|||
storm::storage::BitVector _minimizerStates; |
|||
|
|||
storm::storage::BitVector _fixedMinStrat; |
|||
storm::storage::BitVector _fixedMaxStrat; |
|||
std::vector<ValueType> _resultForMax; |
|||
std::vector<ValueType> _resultForMin; |
|||
|
|||
std::vector<ValueType> _b; |
|||
|
|||
boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> _valueThreshold; |
|||
storm::solver::OptimizationDirection _optimizationDirection; |
|||
bool _produceScheduler; |
|||
bool _produceChoiceValues; |
|||
bool _isQualitativeSet; |
|||
|
|||
std::vector<ValueType> _x, _xL, _xU; |
|||
std::vector<ValueType> _Tsx1, _Tsx2, _TsChoiceValues; |
|||
std::vector<ValueType> _Isx, _Isb, _IsChoiceValues; |
|||
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier; |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> _Solver; |
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> _DetIsSolver; |
|||
std::unique_ptr<storm::Environment> _IsSolverEnv; |
|||
|
|||
boost::optional<std::vector<uint64_t>> _producedOptimalChoices; |
|||
boost::optional<std::vector<ValueType>> _choiceValues; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,371 @@ |
|||
#include "SoundGameViHelper.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"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
namespace internal { |
|||
|
|||
template <typename ValueType> |
|||
SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection), _b(b) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) { |
|||
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix); |
|||
_x1IsCurrent = false; |
|||
if (_statesOfCoalition.size()) { |
|||
_minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; |
|||
} |
|||
else { |
|||
_minimizerStates = storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), _optimizationDirection == OptimizationDirection::Minimize); |
|||
} |
|||
_oldPolicy = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); |
|||
_timing = std::vector<double>(5, 0); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& xL, std::vector<ValueType>& xU, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues) { |
|||
|
|||
prepareSolversAndMultipliers(env); |
|||
// Get precision for convergence check.
|
|||
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision()); |
|||
|
|||
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); |
|||
_x1L = xL; |
|||
_x2L = _x1L; |
|||
|
|||
_x1U = xU; |
|||
_x2U = _x1U; |
|||
|
|||
if (this->isProduceSchedulerSet()) { |
|||
if (!this->_producedOptimalChoices.is_initialized()) { |
|||
this->_producedOptimalChoices.emplace(); |
|||
} |
|||
this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); |
|||
} |
|||
|
|||
uint64_t iter = 0; |
|||
constrainedChoiceValues = std::vector<ValueType>(_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); |
|||
|
|||
while (iter < maxIter) { |
|||
performIterationStep(env, dir); |
|||
if (checkConvergence(precision)) { |
|||
// one last iteration for shield
|
|||
_multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); |
|||
storm::storage::BitVector psiStates = _psiStates; |
|||
auto xL_begin = xNewL().begin(); |
|||
std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it){ |
|||
if (psiStates[&it - &(*xL_begin)]) |
|||
it = 1; |
|||
}); |
|||
break; |
|||
} |
|||
if (storm::utility::resources::isTerminate()) { |
|||
break; |
|||
} |
|||
++iter; |
|||
} |
|||
xL = xNewL(); |
|||
xU = xNewU(); |
|||
|
|||
if (isProduceSchedulerSet()) { |
|||
// We will be doing one more iteration step and track scheduler choices this time.
|
|||
_x1IsCurrent = !_x1IsCurrent; |
|||
_multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), &_producedOptimalChoices.get(), &_statesOfCoalition); |
|||
storm::storage::BitVector psiStates = _psiStates; |
|||
auto xL_begin = xNewL().begin(); |
|||
std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it) |
|||
{ |
|||
if (psiStates[&it - &(*xL_begin)]) |
|||
it = 1; |
|||
}); |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) { |
|||
storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; |
|||
|
|||
// under approximation
|
|||
if (!_multiplier) { |
|||
prepareSolversAndMultipliers(env); |
|||
} |
|||
_x1IsCurrent = !_x1IsCurrent; |
|||
std::vector<ValueType> choiceValuesL = std::vector<ValueType>(this->_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); |
|||
|
|||
_multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); |
|||
reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); |
|||
storm::storage::BitVector psiStates = _psiStates; |
|||
auto xL_begin = xNewL().begin(); |
|||
std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it) |
|||
{ |
|||
if (psiStates[&it - &(*xL_begin)]) |
|||
it = 1; |
|||
}); |
|||
|
|||
// over_approximation
|
|||
std::vector<ValueType> choiceValuesU = std::vector<ValueType>(this->_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); |
|||
|
|||
_multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); |
|||
reduceChoiceValues(choiceValuesU, nullptr, xNewU()); |
|||
auto xU_begin = xNewU().begin(); |
|||
std::for_each(xNewU().begin(), xNewU().end(), [&psiStates, &xU_begin](ValueType &it) |
|||
{ |
|||
if (psiStates[&it - &(*xU_begin)]) |
|||
it = 1; |
|||
}); |
|||
|
|||
if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed
|
|||
// restricting the none optimal minimizer choices
|
|||
_restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); |
|||
|
|||
// find_MSECs()
|
|||
_MSECs = storm::storage::MaximalEndComponentDecomposition<ValueType>(_restrictedTransitions, _restrictedTransitions.transpose(true)); |
|||
} |
|||
|
|||
// reducing the choiceValuesU
|
|||
size_t i = 0; |
|||
auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { |
|||
bool ret = !(reducedMinimizerActions[i]); |
|||
i++; |
|||
return ret; |
|||
}); |
|||
choiceValuesU.erase(new_end, choiceValuesU.end()); |
|||
|
|||
_oldPolicy = reducedMinimizerActions; |
|||
|
|||
// deflating the MSECs
|
|||
deflate(_MSECs, _restrictedTransitions, xNewU(), choiceValuesU); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MSEC, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU, std::vector<ValueType> choiceValues) { |
|||
|
|||
auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); |
|||
auto choice_begin = choiceValues.begin(); |
|||
// iterating over all MSECs
|
|||
for (auto smec_it : MSEC) { |
|||
ValueType bestExit = 0; |
|||
auto stateSet = smec_it.getStateSet(); |
|||
for (uint state : stateSet) { |
|||
if (_psiStates[state]) { |
|||
bestExit = 1; |
|||
break; |
|||
} |
|||
if (_minimizerStates[state]) continue; |
|||
uint rowGroupIndex = rowGroupIndices[state]; |
|||
auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs) |
|||
{ |
|||
bool lhsExiting = !smec_it.containsChoice(state, (&lhs - &(*choice_begin))); |
|||
bool rhsExiting = !smec_it.containsChoice(state, (&rhs - &(*choice_begin))); |
|||
if( lhsExiting && !rhsExiting) return false; |
|||
if(!lhsExiting && rhsExiting) return true; |
|||
if(!lhsExiting && !rhsExiting) return false; |
|||
return lhs < rhs; |
|||
}; |
|||
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex; |
|||
|
|||
auto choice_it = choice_begin + rowGroupIndex; |
|||
auto it = std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare); |
|||
ValueType newBestExit = 0; |
|||
if (!smec_it.containsChoice(state, it - choice_begin)) { |
|||
newBestExit = *it; |
|||
} |
|||
if (newBestExit > bestExit) |
|||
bestExit = newBestExit; |
|||
} |
|||
// deflating the states of the current MSEC
|
|||
for (uint state : stateSet) { |
|||
xU[state] = std::min(xU[state], bestExit); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result, std::vector<ValueType>& x) |
|||
{ |
|||
// result BitVec should be initialized with 1s outside the method
|
|||
|
|||
auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); |
|||
auto choice_it = choiceValues.begin(); |
|||
|
|||
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { |
|||
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; |
|||
ValueType optChoice; |
|||
if (_minimizerStates[state]) { // check if current state is minimizer state
|
|||
// getting the optimal minimizer choice for the given state
|
|||
optChoice = *std::min_element(choice_it, choice_it + rowGroupSize); |
|||
|
|||
if (result != nullptr) { |
|||
for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { |
|||
if (*choice_it > optChoice) { |
|||
result->set(rowGroupIndices[state] + choice, 0); |
|||
} |
|||
} |
|||
} |
|||
else { |
|||
choice_it += rowGroupSize; |
|||
} |
|||
// reducing the xNew() vector for minimizer states
|
|||
x[state] = optChoice; |
|||
} |
|||
else |
|||
{ |
|||
optChoice = *std::max_element(choice_it, choice_it + rowGroupSize); |
|||
// reducing the xNew() vector for maximizer states
|
|||
x[state] = optChoice; |
|||
choice_it += rowGroupSize; |
|||
} |
|||
} |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
bool SoundGameViHelper<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 = xNewL().begin(); |
|||
auto x1Ite = xNewL().end(); |
|||
auto x2It = xNewU().begin(); |
|||
for (; x1It != x1Ite; x1It++, x2It++) { |
|||
ValueType diff = (*x2It - *x1It); |
|||
if (diff > threshold) { |
|||
return false; |
|||
} |
|||
} |
|||
return true; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::setProduceScheduler(bool value) { |
|||
_produceScheduler = value; |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
bool SoundGameViHelper<ValueType>::isProduceSchedulerSet() const { |
|||
return _produceScheduler; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::setShieldingTask(bool value) { |
|||
_shieldingTask = value; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool SoundGameViHelper<ValueType>::isShieldingTask() const { |
|||
return _shieldingTask; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix) { |
|||
_transitionMatrix = newTransitionMatrix; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) { |
|||
_statesOfCoalition = newStatesOfCoalition; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<uint64_t> const& SoundGameViHelper<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>& SoundGameViHelper<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> SoundGameViHelper<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> |
|||
void SoundGameViHelper<ValueType>::getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues) { |
|||
_multiplier->multiply(env, x, nullptr, choiceValues); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
void SoundGameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) { |
|||
std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>()); |
|||
auto choice_it = choiceValues.begin(); |
|||
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { |
|||
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; |
|||
if (psiStates.get(state)) { |
|||
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { |
|||
allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; |
|||
} |
|||
} |
|||
} |
|||
choiceValues = allChoices; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType>& SoundGameViHelper<ValueType>::xNewL() { |
|||
return _x1IsCurrent ? _x1L : _x2L; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> const& SoundGameViHelper<ValueType>::xNewL() const { |
|||
return _x1IsCurrent ? _x1L : _x2L; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType>& SoundGameViHelper<ValueType>::xOldL() { |
|||
return _x1IsCurrent ? _x2L : _x1L; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> const& SoundGameViHelper<ValueType>::xOldL() const { |
|||
return _x1IsCurrent ? _x2L : _x1L; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType>& SoundGameViHelper<ValueType>::xNewU() { |
|||
return _x1IsCurrent ? _x1U : _x2U; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> const& SoundGameViHelper<ValueType>::xNewU() const { |
|||
return _x1IsCurrent ? _x1U : _x2U; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType>& SoundGameViHelper<ValueType>::xOldU() { |
|||
return _x1IsCurrent ? _x2U : _x1U; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> const& SoundGameViHelper<ValueType>::xOldU() const { |
|||
return _x1IsCurrent ? _x2U : _x1U; |
|||
} |
|||
|
|||
template class SoundGameViHelper<double>; |
|||
#ifdef STORM_HAVE_CARL
|
|||
template class SoundGameViHelper<storm::RationalNumber>; |
|||
#endif
|
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,136 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/storage/SparseMatrix.h" |
|||
#include "storm/solver/LinearEquationSolver.h" |
|||
#include "storm/solver/MinMaxLinearEquationSolver.h" |
|||
#include "storm/solver/Multiplier.h" |
|||
#include "storm/storage/MaximalEndComponentDecomposition.h" |
|||
|
|||
namespace storm { |
|||
class Environment; |
|||
|
|||
namespace storage { |
|||
template <typename VT> class Scheduler; |
|||
} |
|||
|
|||
namespace modelchecker { |
|||
namespace helper { |
|||
namespace internal { |
|||
|
|||
template <typename ValueType> |
|||
class SoundGameViHelper { |
|||
public: |
|||
SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); |
|||
|
|||
void prepareSolversAndMultipliers(const Environment& env); |
|||
|
|||
/*! |
|||
* Perform value iteration until convergence |
|||
*/ |
|||
void performValueIteration(Environment const& env, std::vector<ValueType>& xL, std::vector<ValueType>& xU, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues); |
|||
|
|||
/*! |
|||
* 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; |
|||
|
|||
/*! |
|||
* Sets whether an optimal scheduler shall be constructed during the computation |
|||
*/ |
|||
void setShieldingTask(bool value); |
|||
|
|||
/*! |
|||
* @return whether an optimal scheduler shall be constructed during the computation |
|||
*/ |
|||
bool isShieldingTask() const; |
|||
|
|||
/*! |
|||
* Changes the transitionMatrix to the given one. |
|||
*/ |
|||
void updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix); |
|||
|
|||
/*! |
|||
* Changes the statesOfCoalition to the given one. |
|||
*/ |
|||
void updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition); |
|||
|
|||
storm::storage::Scheduler<ValueType> extractScheduler() const; |
|||
|
|||
void getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues); |
|||
|
|||
/*! |
|||
* Fills the choice values vector to the original size with zeros for ~psiState choices. |
|||
*/ |
|||
void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices); |
|||
|
|||
void deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU, std::vector<ValueType> choiceValues); |
|||
|
|||
void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result, std::vector<ValueType>& x); |
|||
|
|||
private: |
|||
/*! |
|||
* Performs one iteration step for value iteration |
|||
*/ |
|||
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>& xNewL(); |
|||
std::vector<ValueType> const& xNewL() const; |
|||
|
|||
std::vector<ValueType>& xOldL(); |
|||
std::vector<ValueType> const& xOldL() const; |
|||
|
|||
std::vector<ValueType>& xNewU(); |
|||
std::vector<ValueType> const& xNewU() const; |
|||
|
|||
std::vector<ValueType>& xOldU(); |
|||
std::vector<ValueType> const& xOldU() const; |
|||
|
|||
bool _x1IsCurrent; |
|||
|
|||
storm::storage::BitVector _minimizerStates; |
|||
|
|||
/*! |
|||
* @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(); |
|||
|
|||
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier; |
|||
|
|||
storm::storage::SparseMatrix<ValueType> _transitionMatrix; |
|||
storm::storage::SparseMatrix<ValueType> _backwardTransitions; |
|||
storm::storage::SparseMatrix<ValueType> _restrictedTransitions; |
|||
storm::storage::BitVector _oldPolicy; |
|||
storm::storage::BitVector _statesOfCoalition; |
|||
storm::storage::BitVector _psiStates; |
|||
std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U, _b; |
|||
OptimizationDirection _optimizationDirection; |
|||
|
|||
storm::storage::MaximalEndComponentDecomposition<ValueType> _MSECs; |
|||
|
|||
bool _produceScheduler = false; |
|||
bool _shieldingTask = false; |
|||
boost::optional<std::vector<uint64_t>> _producedOptimalChoices; |
|||
|
|||
std::vector<double> _timing; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue