From ace401f120fbb1f117018bd811d4d046e781e99c Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 16 Dec 2020 11:25:05 +0100 Subject: [PATCH] added smg rpatl model checker --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 121 ++++++++++++++++++ .../rpatl/SparseSmgRpatlModelChecker.h | 38 ++++++ 2 files changed, 159 insertions(+) create mode 100644 src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp create mode 100644 src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp new file mode 100644 index 000000000..f6161fac2 --- /dev/null +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -0,0 +1,121 @@ +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" + +#include +#include + +#include "storm/utility/macros.h" +#include "storm/utility/FilteredRewardModel.h" + +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" + +#include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" + +#include "storm/logic/FragmentSpecification.h" + +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace modelchecker { + template + SparseSmgRpatlModelChecker::SparseSmgRpatlModelChecker(SparseSmgModelType const& model) : SparsePropositionalModelChecker(model) { + // Intentionally left empty. + } + + template + bool SparseSmgRpatlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { + storm::logic::Formula const& formula = checkTask.getFormula(); + + if (formula.isInFragment(storm::logic::rpatl().setCoalitionOperatorsAllowed(true).setRewardOperatorsAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageOperatorsAllowed(true))) { + return true; + } else { + return false; + } + } + + template + bool SparseSmgRpatlModelChecker::canHandle(CheckTask const& checkTask) const { + bool requiresSingleInitialState = false; + if (canHandleStatic(checkTask, &requiresSingleInitialState)) { + return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1; + } else { + return false; + } + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_DEBUG("checkGameFormula matrix: " << this->getModel().getTransitionMatrix().getDimensionsAsString()); + STORM_LOG_DEBUG("checkGameFormula playerindices:"); + STORM_LOG_DEBUG("checkGameFormula matrix: \n" << this->getModel().getTransitionMatrix()); + // TODO set min max row groups w.r.t. coalition + storm::logic::GameFormula const& gameFormula = checkTask.getFormula(); + storm::logic::Formula const& subFormula = gameFormula.getSubformula(); + STORM_LOG_DEBUG(gameFormula); + if (subFormula.isRewardOperatorFormula()) { + return this->checkRewardOperatorFormula(env, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); + } else if (subFormula.isLongRunAverageOperatorFormula()) { + return this->checkLongRunAverageOperatorFormula(env, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula())); + } + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkGameFormula NYI"); + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) { + storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula(); + std::unique_ptr result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula())); + + return nullptr; + } + + template + std::unique_ptr AbstractModelChecker::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + storm::logic::Formula const& rewardFormula = checkTask.getFormula(); + if (rewardFormula.isLongRunAverageRewardFormula()) { + return this->computeLongRunAverageRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula())); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid."); + } + + template + std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask const& checkTask) { + storm::logic::LongRunAverageOperatorFormula const& formula = checkTask.getFormula(); + //STORM_LOG_THROW(formula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + + std::unique_ptr result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula())); + + return result; //TODO check bounds. + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), this->getModel().getPlayerActionIndices()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + + //std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values)); + //return result; + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); + } + + template class SparseSmgRpatlModelChecker>; +#ifdef STORM_HAVE_CARL + template class SparseSmgRpatlModelChecker>; + //template class SparseSmgRpatlModelChecker>; TODO are we going to need this? +#endif + } +} diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h new file mode 100644 index 000000000..91bb09206 --- /dev/null +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -0,0 +1,38 @@ +#ifndef STORM_MODELCHECKER_SPARSESMGRPATLMODELCHECKER_H_ +#define STORM_MODELCHECKER_SPARSESMGRPATLMODELCHECKER_H_ + +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/models/sparse/Smg.h" +#include "storm/utility/solver.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/storage/StronglyConnectedComponent.h" + +namespace storm { + namespace modelchecker { + + template + class SparseSmgRpatlModelChecker : public SparsePropositionalModelChecker { + public: + typedef typename SparseSmgModelType::ValueType ValueType; + typedef typename SparseSmgModelType::RewardModelType RewardModelType; + + explicit SparseSmgRpatlModelChecker(SparseSmgModelType const& model); + + /*! + * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state + */ + static bool canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState = nullptr); + + // The implemented methods of the AbstractModelChecker interface. + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr checkGameFormula(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) override; + + virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + }; + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_SPARSESMGRPATLMODELCHECKER_H_ */