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

added and finalized NondetGamehelper methods 

This still needs some better documentation for the introduced class
methods.

Also removed some debug printing.
tempestpy_adaptions
Stefan Pranger 4 years ago
parent
ea90c1ac7d
commit
4c7968b4cf
3 changed files with 96 additions and 15 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. 1
      src/storm-parsers/parser/PrismParser.cpp
  2. 89
      src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
  3. 21
      src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h

1
src/storm-parsers/parser/PrismParser.cpp
View File

@ -816,7 +816,6 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present.");
}
}
STORM_LOG_DEBUG("PLAYER created:" << playerName);
return storm::prism::Player(playerName, controlledModuleIndices, controlledActionIndices);
} else {
return storm::prism::Player();

89
src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
View File

@ -3,6 +3,7 @@
#include "storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/Scheduler.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
@ -26,25 +27,99 @@ namespace storm {
// Intentionally left empty.
}
template <typename ValueType>
std::vector<uint64_t> const& SparseNondeterministicGameInfiniteHorizonHelper<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>& SparseNondeterministicGameInfiniteHorizonHelper<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> SparseNondeterministicGameInfiniteHorizonHelper<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 SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::createDecomposition() {
STORM_LOG_THROW(false, storm::exceptions::InternalException, "Creating Decompositions of SMGs is currently not possible.");
// TODO This needs to be changed to return the whole model as one component as long as there is no overwritten version of MaximalEndComponentDecomposition for SMGs.
if (this->_longRunComponentDecomposition == nullptr) {
// The decomposition has not been provided or computed, yet.
if (this->_backwardTransitions == nullptr) {
this->_computedBackwardTransitions = std::make_unique<storm::storage::SparseMatrix<ValueType>>(this->_transitionMatrix.transpose(true));
this->_backwardTransitions = this->_computedBackwardTransitions.get();
}
this->_computedLongRunComponentDecomposition = std::make_unique<storm::storage::MaximalEndComponentDecomposition<ValueType>>(this->_transitionMatrix, *this->_backwardTransitions);
this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get();
}
}
template <typename ValueType>
ValueType SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) {
std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter) {
auto underlyingSolverEnvironment = env;
std::vector<ValueType> componentLraValues;
createDecomposition();
componentLraValues.reserve(this->_longRunComponentDecomposition->size());
for (auto const& c : *(this->_longRunComponentDecomposition)) {
componentLraValues.push_back(computeLraForComponent(underlyingSolverEnvironment, stateValuesGetter, actionValuesGetter, c));
}
return componentLraValues;
}
STORM_LOG_THROW(false, storm::exceptions::InternalException, "Computing values for LRA for SMGs components is currently not possible.");
template <typename ValueType>
ValueType SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) {
// Allocate memory for the nondeterministic choices.
if (this->isProduceSchedulerSet()) {
if (!this->_producedOptimalChoices.is_initialized()) {
this->_producedOptimalChoices.emplace();
}
this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
}
storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod();
if (method == storm::solver::LraMethod::LinearProgramming) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
} else if (method == storm::solver::LraMethod::ValueIteration) {
return computeLraVi(env, stateRewardsGetter, actionRewardsGetter, component);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
}
template <typename ValueType>
std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& componentLraValues) {
STORM_LOG_THROW(false, storm::exceptions::InternalException, "buildAndSolveSsp not available for SMGs");
ValueType SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLraVi(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& mec) {
// Collect some parameters of the computation
ValueType aperiodicFactor = storm::utility::convertNumber<ValueType>(env.solver().lra().getAperiodicFactor());
std::vector<uint64_t>* optimalChoices = nullptr;
if (this->isProduceSchedulerSet()) {
optimalChoices = &this->_producedOptimalChoices.get();
}
// Now create a helper and perform the algorithm
if (this->isContinuousTime()) {
STORM_LOG_THROW(false, storm::exceptions::InternalException, "We cannot handle continuous time games.");
} else {
storm::modelchecker::helper::internal::LraViHelper<ValueType, storm::storage::MaximalEndComponent, storm::modelchecker::helper::internal::LraViTransitionsType::GameNondetTsNoIs> viHelper(mec, this->_transitionMatrix, aperiodicFactor);
return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices);
}
}
template <typename ValueType>
std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLongRunAverageValues(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter) {
STORM_LOG_THROW(false, storm::exceptions::InternalException, "computeLongRunAverageValues not possible yet.");
std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& componentLraValues) {
STORM_LOG_THROW(false, storm::exceptions::InternalException, "We do not create compositions for LRA for SMGs, solving a stochastic shortest path problem is not available.");
}

21
src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h
View File

@ -1,4 +1,5 @@
#pragma once
#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h"
namespace storm {
@ -29,31 +30,37 @@ namespace storm {
*/
SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player);
/*!
* TODO
/*! TODO
* Computes the long run average value given the provided state and action based rewards
* @param stateValuesGetter a function returning a value for a given state index
* @param actionValuesGetter a function returning a value for a given (global) choice index
* @return a value for each state
*/
std::vector<ValueType> computeLongRunAverageValues(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter);
std::vector<ValueType> computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter) override;
/*!
* @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;
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::vector<uint64_t>& getProducedOptimalChoices();
/*!
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
* @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call.
*/
//storm::storage::Scheduler<ValueType> extractScheduler() const;
storm::storage::Scheduler<ValueType> extractScheduler() const;
void createDecomposition();
ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component);
ValueType computeLraVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec);
void createDecomposition();
std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues);
private:

Write Preview
Loading…
Cancel
Save