From e406b00c024e1aaa7bb953ceeb6b243e6c301cc6 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 28 Sep 2021 18:29:45 +0200 Subject: [PATCH] infinite horizon helper now store information about shielding tasks and whether to compute all choice values --- .../helper/SingleValueModelCheckerHelper.cpp | 50 ++++++----- .../helper/SingleValueModelCheckerHelper.h | 45 ++++++---- .../SparseInfiniteHorizonHelper.h | 45 +++++----- ...eNondeterministicInfiniteHorizonHelper.cpp | 88 +++++++++++-------- ...rseNondeterministicInfiniteHorizonHelper.h | 43 +++++---- .../utility/SetInformationFromCheckTask.h | 9 +- .../rpatl/helper/internal/GameViHelper.cpp | 12 ++- .../rpatl/helper/internal/GameViHelper.h | 11 +++ 8 files changed, 186 insertions(+), 117 deletions(-) diff --git a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp index 885411b01..196cb4353 100644 --- a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp +++ b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp @@ -4,85 +4,95 @@ namespace storm { namespace modelchecker { namespace helper { - + template SingleValueModelCheckerHelper::SingleValueModelCheckerHelper() : _produceScheduler(false) { // Intentionally left empty } - + template void SingleValueModelCheckerHelper::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) { _optimizationDirection = direction; } - + template void SingleValueModelCheckerHelper::clearOptimizationDirection() { _optimizationDirection = boost::none; } - + template bool SingleValueModelCheckerHelper::isOptimizationDirectionSet() const { return _optimizationDirection.is_initialized(); } - + template storm::solver::OptimizationDirection const& SingleValueModelCheckerHelper::getOptimizationDirection() const { STORM_LOG_ASSERT(isOptimizationDirectionSet(), "Requested optimization direction but none was set."); return _optimizationDirection.get(); } - + template bool SingleValueModelCheckerHelper::minimize() const { return storm::solver::minimize(getOptimizationDirection()); } - + template bool SingleValueModelCheckerHelper::maximize() const { return storm::solver::maximize(getOptimizationDirection()); } - + template boost::optional SingleValueModelCheckerHelper::getOptionalOptimizationDirection() const { return _optimizationDirection; } - + template void SingleValueModelCheckerHelper::setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& threshold) { _valueThreshold = std::make_pair(comparisonType, threshold); } - + template void SingleValueModelCheckerHelper::clearValueThreshold() { _valueThreshold = boost::none; } - + template bool SingleValueModelCheckerHelper::isValueThresholdSet() const { return _valueThreshold.is_initialized(); } - + template storm::logic::ComparisonType const& SingleValueModelCheckerHelper::getValueThresholdComparisonType() const { STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before."); return _valueThreshold->first; } - + template ValueType const& SingleValueModelCheckerHelper::getValueThresholdValue() const { STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before."); return _valueThreshold->second; } - + template void SingleValueModelCheckerHelper::setProduceScheduler(bool value) { _produceScheduler = value; } - + template bool SingleValueModelCheckerHelper::isProduceSchedulerSet() const { return _produceScheduler; } + template + void SingleValueModelCheckerHelper::setProduceChoiceValues(bool value) { + _produceChoiceValues = value; + } + + template + bool SingleValueModelCheckerHelper::isProduceChoiceValuesSet() const { + return _produceChoiceValues; + } + template void SingleValueModelCheckerHelper::setQualitative(bool value) { _isQualitativeSet = value; @@ -92,17 +102,17 @@ namespace storm { bool SingleValueModelCheckerHelper::isQualitativeSet() const { return _isQualitativeSet; } - + template class SingleValueModelCheckerHelper; template class SingleValueModelCheckerHelper; template class SingleValueModelCheckerHelper; - + template class SingleValueModelCheckerHelper; template class SingleValueModelCheckerHelper; template class SingleValueModelCheckerHelper; - + template class SingleValueModelCheckerHelper; - + } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h index f328d5a7f..2f1df6b94 100644 --- a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h +++ b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h @@ -8,7 +8,7 @@ namespace storm { namespace modelchecker { namespace helper { - + /*! * Helper for model checking queries where we are interested in (optimizing) a single value per state. * @tparam ValueType The type of a value @@ -19,47 +19,47 @@ namespace storm { public: SingleValueModelCheckerHelper(); - + /*! * Sets the optimization direction, i.e., whether we want to minimize or maximize the value for each state * Has no effect for models without nondeterminism. * Has to be set if there is nondeterminism in the model. */ void setOptimizationDirection(storm::solver::OptimizationDirection const& direction); - + /*! * Clears the optimization direction if it was set before. */ void clearOptimizationDirection(); - + /*! * @return true if there is an optimization direction set */ bool isOptimizationDirectionSet() const; - + /*! * @pre an optimization direction has to be set before calling this. * @return the optimization direction. */ storm::solver::OptimizationDirection const& getOptimizationDirection() const; - + /*! * @pre an optimization direction has to be set before calling this. * @return true iff the optimization goal is to minimize the value for each state */ bool minimize() const; - + /*! * @pre an optimization direction has to be set before calling this. * @return true iff the optimization goal is to maximize the value for each state */ bool maximize() const; - + /*! * @return The optimization direction (if it was set) */ boost::optional getOptionalOptimizationDirection() const; - + /*! * Sets a goal threshold for the value at each state. If such a threshold is set, it is assumed that we are only interested * in the satisfaction of the threshold. Setting this allows the helper to compute values only up to the precision @@ -68,39 +68,49 @@ namespace storm { * @param thresholdValue The value used on the right hand side of the comparison relation. */ void setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& thresholdValue); - + /*! * Clears the valueThreshold if it was set before. */ void clearValueThreshold(); - + /*! * @return true, if a value threshold has been set. */ bool isValueThresholdSet() const; - + /*! * @pre A value threshold has to be set before calling this. * @return The relation used when comparing computed values (left hand side) with the specified threshold value (right hand side). */ storm::logic::ComparisonType const& getValueThresholdComparisonType() const; - + /*! * @pre A value threshold has to be set before calling this. * @return The value used on the right hand side of the comparison relation. */ ValueType const& getValueThresholdValue() const; - + /*! * 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 all choice values shall be computed + */ + void setProduceChoiceValues(bool value); + + /*! + * @return whether all choice values shall be computed + */ + bool isProduceChoiceValuesSet() const; + /*! * Sets whether the property needs to be checked qualitatively */ @@ -110,13 +120,14 @@ namespace storm { * @return whether the property needs to be checked qualitatively */ bool isQualitativeSet() const; - + private: boost::optional _optimizationDirection; boost::optional> _valueThreshold; bool _produceScheduler; + bool _produceChoiceValues; bool _isQualitativeSet; }; } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h index 5b8ed6419..fa30b84d7 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h @@ -8,16 +8,16 @@ namespace storm { class Environment; - + namespace models { namespace sparse { template class StandardRewardModel; } } - + namespace modelchecker { namespace helper { - + /*! * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. * @tparam ValueType the type a value can have @@ -27,22 +27,22 @@ namespace storm { class SparseInfiniteHorizonHelper : public SingleValueModelCheckerHelper { public: - + /*! * The type of a component in which the system resides in the long run (BSCC for deterministic models, MEC for nondeterministic models) */ using LongRunComponentType = typename std::conditional::type; - + /*! * Function mapping from indices to values */ typedef std::function ValueGetter; - + /*! * Initializes the helper for a discrete time (i.e. DTMC, MDP) */ SparseInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix); - + /*! * Initializes the helper for continuous time (i.e. MA) */ @@ -52,33 +52,33 @@ namespace storm { * Initializes the helper for continuous time (i.e. CTMC) */ SparseInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates); - + /*! * Provides backward transitions that can be used during the computation. * Providing them is optional. If they are not provided, they will be computed internally * Be aware that this class does not take ownership, i.e. the caller has to make sure that the reference to the backwardstransitions remains valid. */ void provideBackwardTransitions(storm::storage::SparseMatrix const& backwardsTransitions); - + /*! * Provides the decomposition into long run components (BSCCs/MECs) that can be used during the computation. * Providing the decomposition is optional. If it is not provided, they will be computed internally. * Be aware that this class does not take ownership, i.e. the caller has to make sure that the reference to the decomposition remains valid. */ void provideLongRunComponentDecomposition(storm::storage::Decomposition const& decomposition); - + /*! * Computes the long run average probabilities, i.e., the fraction of the time we are in a psiState * @return a value for each state */ std::vector computeLongRunAverageProbabilities(Environment const& env, storm::storage::BitVector const& psiStates); - + /*! * Computes the long run average rewards, i.e., the average reward collected per time unit * @return a value for each state */ std::vector computeLongRunAverageRewards(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel); - + /*! * Computes the long run average value given the provided state and action-based rewards. * @param stateValues a vector containing a value for every state @@ -86,7 +86,7 @@ namespace storm { * @return a value for each state */ std::vector computeLongRunAverageValues(Environment const& env, std::vector const* stateValues = nullptr, std::vector const* actionValues = nullptr); - + /*! * 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 @@ -102,39 +102,40 @@ namespace storm { * @post if scheduler production is enabled and Nondeterministic is true, getProducedOptimalChoices() contains choices for the states of the given component which yield the returned LRA value. Choices for states outside of the component are not affected. */ virtual ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, LongRunComponentType const& component) = 0; - + protected: - + /*! * @return true iff this is a computation on a continuous time model (i.e. CTMC, MA) */ bool isContinuousTime() const; - + /*! * @post _longRunComponentDecomposition points to a decomposition of the long run components (MECs, BSCCs) */ virtual void createDecomposition() = 0; - + /*! * @pre if scheduler production is enabled and Nondeterministic is true, a choice for each state within a component must be set such that the choices yield optimal values w.r.t. the individual components. * @return Lra values for each state * @post if scheduler production is enabled and Nondeterministic is true, getProducedOptimalChoices() contains choices for all input model states which yield the returned LRA values. */ virtual std::vector buildAndSolveSsp(Environment const& env, std::vector const& mecLraValues) = 0; - + storm::storage::SparseMatrix const& _transitionMatrix; storm::storage::BitVector const* _markovianStates; std::vector const* _exitRates; - + storm::storage::SparseMatrix const* _backwardTransitions; storm::storage::Decomposition const* _longRunComponentDecomposition; std::unique_ptr> _computedBackwardTransitions; std::unique_ptr> _computedLongRunComponentDecomposition; - + boost::optional> _producedOptimalChoices; + boost::optional> _choiceValues; }; - + } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp index a6d4cb7dd..1fc6aa295 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp @@ -22,31 +22,31 @@ namespace storm { namespace modelchecker { namespace helper { - + template SparseNondeterministicInfiniteHorizonHelper::SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix) : SparseInfiniteHorizonHelper(transitionMatrix) { // Intentionally left empty. } - + template SparseNondeterministicInfiniteHorizonHelper::SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector const& exitRates) : SparseInfiniteHorizonHelper(transitionMatrix, markovianStates, exitRates) { // Intentionally left empty. } - + template std::vector const& SparseNondeterministicInfiniteHorizonHelper::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 std::vector& SparseNondeterministicInfiniteHorizonHelper::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 storm::storage::Scheduler SparseNondeterministicInfiniteHorizonHelper::extractScheduler() const { auto const& optimalChoices = getProducedOptimalChoices(); @@ -56,7 +56,14 @@ namespace storm { } return scheduler; } - + + template + std::vector SparseNondeterministicInfiniteHorizonHelper::getChoiceValues() const { + STORM_LOG_ASSERT(this->isProduceChoiceValuesSet(), "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 void SparseNondeterministicInfiniteHorizonHelper::createDecomposition() { if (this->_longRunComponentDecomposition == nullptr) { @@ -73,7 +80,7 @@ namespace storm { template ValueType SparseNondeterministicInfiniteHorizonHelper::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) { // For models with potential nondeterminisim, we compute the LRA for a maximal end component (MEC) - + // Allocate memory for the nondeterministic choices. if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { @@ -81,12 +88,19 @@ namespace storm { } this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); } - + // Allocate memory for the choice values. + if (this->isProduceSchedulerSet()) { + if (!this->_choiceValues.is_initialized()) { + this->_choiceValues.emplace(); + } + this->_choiceValues->resize(this->_transitionMatrix.getRowCount()); + } + auto trivialResult = this->computeLraForTrivialMec(env, stateRewardsGetter, actionRewardsGetter, component); if (trivialResult.first) { return trivialResult.second; } - + // Solve nontrivial MEC with the method specified in the settings storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod(); if ((storm::NumberTraits::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) { @@ -105,10 +119,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } } - + template std::pair SparseNondeterministicInfiniteHorizonHelper::computeLraForTrivialMec(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) { - + // If the component only consists of a single state, we compute the LRA value directly if (component.size() == 1) { auto const& element = *component.begin(); @@ -145,8 +159,8 @@ namespace storm { } return {false, storm::utility::zero()}; } - - + + template ValueType SparseNondeterministicInfiniteHorizonHelper::computeLraForMecVi(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& mec) { @@ -156,7 +170,11 @@ namespace storm { if (this->isProduceSchedulerSet()) { optimalChoices = &this->_producedOptimalChoices.get(); } - + std::vector* choiceValues = nullptr; + if (this->isProduceChoiceValuesSet()) { + choiceValues = &this->_choiceValues.get(); + } + // Now create a helper and perform the algorithm if (this->isContinuousTime()) { // We assume a Markov Automaton (with deterministic timed states and nondeterministic instant states) @@ -187,12 +205,12 @@ namespace storm { } storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", storm::utility::one()); solver->update(); - + // Add constraints. for (auto const& stateChoicesPair : mec) { uint_fast64_t state = stateChoicesPair.first; bool stateIsMarkovian = this->_markovianStates && this->_markovianStates->get(state); - + // Now create a suitable constraint for each choice // x_s {≤, ≥} -k/rate(s) + sum_s' P(s,act,s') * x_s' + (value(s)/rate(s) + value(s,act)) for (auto choice : stateChoicesPair.second) { @@ -231,12 +249,12 @@ namespace storm { solver->addConstraint("s" + std::to_string(state) + "," + std::to_string(choice), constraint); } } - + solver->optimize(); STORM_LOG_THROW(!this->isProduceSchedulerSet(), storm::exceptions::NotImplementedException, "Scheduler extraction is not yet implemented for LP based LRA method."); return solver->getContinuousValue(k); } - + /*! * Auxiliary function that adds the entries of the Ssp Matrix for a single choice (i.e., row) * Transitions that lead to a Component state will be redirected to a new auxiliary state (there is one aux. state for each component). @@ -244,10 +262,10 @@ namespace storm { */ template void addSspMatrixChoice(uint64_t const& inputMatrixChoice, storm::storage::SparseMatrix const& inputTransitionMatrix, std::vector const& inputToSspStateMap, uint64_t const& numberOfNonComponentStates, uint64_t const& currentSspChoice, storm::storage::SparseMatrixBuilder& sspMatrixBuilder) { - + // As there could be multiple transitions to the same MEC, we accumulate them in this map before adding them to the matrix builder. std::map auxiliaryStateToProbabilityMap; - + for (auto const& transition : inputTransitionMatrix.getRow(inputMatrixChoice)) { if (!storm::utility::isZero(transition.getValue())) { auto const& sspTransitionTarget = inputToSspStateMap[transition.getColumn()]; @@ -268,18 +286,18 @@ namespace storm { } } } - + // Now insert all (cumulative) probability values that target a component. for (auto const& componentToProbEntry : auxiliaryStateToProbabilityMap) { sspMatrixBuilder.addNextValue(currentSspChoice, componentToProbEntry.first, componentToProbEntry.second); } } - + template std::pair, std::vector> SparseNondeterministicInfiniteHorizonHelper::buildSspMatrixVector(std::vector const& mecLraValues, std::vector const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector>* sspComponentExitChoicesToOriginalMap) { - + auto const& choiceIndices = this->_transitionMatrix.getRowGroupIndices(); - + std::vector rhs; uint64_t numberOfSspStates = numberOfNonComponentStates + this->_longRunComponentDecomposition->size(); storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, numberOfSspStates , 0, true, true, numberOfSspStates); @@ -323,7 +341,7 @@ namespace storm { } return std::make_pair(sspMatrixBuilder.build(currentSspChoice, numberOfSspStates, numberOfSspStates), std::move(rhs)); } - + template void SparseNondeterministicInfiniteHorizonHelper::constructOptimalChoices(std::vector const& sspChoices, storm::storage::SparseMatrix const& sspMatrix, std::vector const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector> const& sspComponentExitChoicesToOriginalMap) { // We first take care of non-mec states @@ -398,11 +416,11 @@ namespace storm { template std::vector SparseNondeterministicInfiniteHorizonHelper::buildAndSolveSsp(Environment const& env, std::vector const& componentLraValues) { STORM_LOG_ASSERT(this->_longRunComponentDecomposition != nullptr, "Decomposition not computed, yet."); - + // For fast transition rewriting, we build a mapping from the input state indices to the state indices of a new transition matrix // which redirects all transitions leading to a former component state to a new auxiliary state. // There will be one auxiliary state for each component. These states will be appended to the end of the matrix. - + // First gather the states that are part of a component // and create a mapping from states that lie in a component to the corresponding component index. storm::storage::BitVector statesInComponents(this->_transitionMatrix.getRowGroupCount()); @@ -427,14 +445,14 @@ namespace storm { for (auto mecState : statesInComponents) { inputToSspStateMap[mecState] += numberOfNonComponentStates; } - + // For scheduler extraction, we will need to create a mapping between choices at the auxiliary states and the // corresponding choices in the original model. std::vector> sspComponentExitChoicesToOriginalMap; - + // The next step is to create the SSP matrix and the right-hand side of the SSP. auto sspMatrixVector = buildSspMatrixVector(componentLraValues, inputToSspStateMap, statesNotInComponent, numberOfNonComponentStates, this->isProduceSchedulerSet() ? &sspComponentExitChoicesToOriginalMap : nullptr); - + // Set-up a solver storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, this->getOptimizationDirection(), false, this->isProduceSchedulerSet()); @@ -448,7 +466,7 @@ namespace storm { solver->setLowerBound(*lowerUpperBounds.first); solver->setUpperBound(*lowerUpperBounds.second); solver->setRequirementsChecked(); - + // Solve the equation system std::vector x(sspMatrixVector.first.getRowGroupCount()); solver->solveEquations(env, this->getOptimizationDirection(), x, sspMatrixVector.second); @@ -460,7 +478,7 @@ namespace storm { } else { STORM_LOG_ERROR_COND(!this->isProduceSchedulerSet(), "Requested to produce a scheduler, but no scheduler was generated."); } - + // Prepare result vector. // For efficiency reasons, we re-use the memory of our rhs for this! std::vector result = std::move(sspMatrixVector.second); @@ -469,10 +487,10 @@ namespace storm { storm::utility::vector::selectVectorValues(result, inputToSspStateMap, x); return result; } - + template class SparseNondeterministicInfiniteHorizonHelper; template class SparseNondeterministicInfiniteHorizonHelper; - + } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h index 5286dfdfc..f5c0eea29 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h @@ -3,14 +3,14 @@ namespace storm { - + namespace storage { template class Scheduler; } - + namespace modelchecker { namespace helper { - + /*! * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. * @tparam ValueType the type a value can have @@ -23,35 +23,40 @@ namespace storm { * Function mapping from indices to values */ typedef typename SparseInfiniteHorizonHelper::ValueGetter ValueGetter; - + /*! * Initializes the helper for a discrete time model (i.e. MDP) */ SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix); - + /*! * Initializes the helper for a continuous time model (i.e. MA) */ SparseNondeterministicInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector const& exitRates); - + /*! * @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 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& 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 extractScheduler() const; + /*! + * @return the computed choice values for the states. + */ + std::vector getChoiceValues() const; + /*! * @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 @@ -59,43 +64,43 @@ namespace storm { * @post if scheduler production is enabled and Nondeterministic is true, getProducedOptimalChoices() contains choices for the states of the given component which yield the returned LRA value. Choices for states outside of the component are not affected. */ virtual ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component) override; - + protected: - + virtual void createDecomposition() override; - + std::pair computeLraForTrivialMec(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec); - + /*! * As computeLraForMec but uses value iteration as a solution method (independent of what is set in env) */ ValueType computeLraForMecVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec); - + /*! * As computeLraForMec but uses linear programming as a solution method (independent of what is set in env) * @see Guck et al.: Modelling and Analysis of Markov Reward Automata (ATVA'14), https://doi.org/10.1007/978-3-319-11936-6_13 */ ValueType computeLraForMecLp(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec); - + std::pair, std::vector> buildSspMatrixVector(std::vector const& mecLraValues, std::vector const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector>* sspComponentExitChoicesToOriginalMap); - + /*! * @pre a choice for each state within a component must be set such that the choices yield optimal values w.r.t. the individual components. * Translates optimal choices for MECS and SSP to the original model. * @post getProducedOptimalChoices() contains choices for all input model states which yield the returned LRA values. */ void constructOptimalChoices(std::vector const& sspChoices, storm::storage::SparseMatrix const& sspMatrix, std::vector const& inputToSspStateMap, storm::storage::BitVector const& statesNotInComponent, uint64_t numberOfNonComponentStates, std::vector> const& sspComponentExitChoicesToOriginalMap); - + /*! * @pre if scheduler production is enabled a choice for each state within a component must be set such that the choices yield optimal values w.r.t. the individual components. * @return Lra values for each state * @post if scheduler production is enabled getProducedOptimalChoices() contains choices for all input model states which yield the returned LRA values. */ virtual std::vector buildAndSolveSsp(Environment const& env, std::vector const& mecLraValues) override; - + }; - + } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h index df1df7362..c7f67060e 100644 --- a/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h +++ b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h @@ -5,7 +5,7 @@ namespace storm { namespace modelchecker { namespace helper { - + /*! * Forwards relevant information stored in the given CheckTask to the given helper */ @@ -26,10 +26,13 @@ namespace storm { // Scheduler Production helper.setProduceScheduler(checkTask.isProduceSchedulersSet()); + // Shield Synthesis + helper.setProduceChoiceValues(checkTask.isShieldingTask()); + // Qualitative flag helper.setQualitative(checkTask.isQualitativeSet()); } - + /*! * Forwards relevant information stored in the given CheckTask to the given helper */ @@ -50,4 +53,4 @@ namespace storm { } } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 54efd3c7c..55508edff 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -50,7 +50,7 @@ namespace storm { _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues); auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); rowGroupIndices.erase(rowGroupIndices.begin()); - _multiplier->reduce(env, dir, constrainedChoiceValues, rowGroupIndices, xNew()); + _multiplier->reduce(env, dir, rowGroupIndices, constrainedChoiceValues, xNew(), nullptr, &_statesOfCoalition); break; } performIterationStep(env, dir); @@ -125,6 +125,16 @@ namespace storm { return _produceScheduler; } + template + void GameViHelper::setShieldingTask(bool value) { + _shieldingTask = value; + } + + template + bool GameViHelper::isShieldingTask() const { + return _shieldingTask; + } + template void GameViHelper::updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix) { _transitionMatrix = newTransitionMatrix; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 507eb60b7..ae3d45647 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -38,6 +38,16 @@ namespace storm { */ 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. */ @@ -93,6 +103,7 @@ namespace storm { std::unique_ptr> _multiplier; bool _produceScheduler = false; + bool _shieldingTask = false; boost::optional> _producedOptimalChoices; }; }