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

added and finalized methods for rpatlMC

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
f72f83f23e
commit
ea90c1ac7d
2 changed files with 47 additions and 32 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 65
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
  2. 14
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h

65
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
View File

@ -2,6 +2,8 @@
#include <vector> #include <vector>
#include <memory> #include <memory>
#include <algorithm>
#include <boost/variant/get.hpp>
#include "storm/utility/macros.h" #include "storm/utility/macros.h"
#include "storm/utility/FilteredRewardModel.h" #include "storm/utility/FilteredRewardModel.h"
@ -14,6 +16,10 @@
#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h"
#include "storm/logic/FragmentSpecification.h" #include "storm/logic/FragmentSpecification.h"
#include "storm/logic/Coalition.h"
#include "storm/storage/BitVector.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/StandardRewardModel.h"
@ -30,10 +36,11 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename SparseSmgModelType> template<typename SparseSmgModelType>
bool SparseSmgRpatlModelChecker<SparseSmgModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) { bool SparseSmgRpatlModelChecker<SparseSmgModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
if (formula.isInFragment(storm::logic::rpatl().setCoalitionOperatorsAllowed(true).setRewardOperatorsAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageOperatorsAllowed(true))) { if (formula.isInFragment(storm::logic::rpatl().setCoalitionOperatorsAllowed(true).setRewardOperatorsAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageOperatorsAllowed(true))) {
return true; return true;
} else { } else {
@ -51,21 +58,22 @@ namespace storm {
} }
} }
template<typename SparseSmgModelType> template<typename SparseSmgModelType>
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> 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
Environment solverEnv = env;
coalitionIndicator(solverEnv, checkTask);
storm::logic::GameFormula const& gameFormula = checkTask.getFormula(); storm::logic::GameFormula const& gameFormula = checkTask.getFormula();
storm::logic::Formula const& subFormula = gameFormula.getSubformula(); storm::logic::Formula const& subFormula = gameFormula.getSubformula();
STORM_LOG_DEBUG(gameFormula);
if (subFormula.isRewardOperatorFormula()) { if (subFormula.isRewardOperatorFormula()) {
return this->checkRewardOperatorFormula(env, checkTask.substituteFormula(subFormula.asRewardOperatorFormula()));
return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula()));
} else if (subFormula.isLongRunAverageOperatorFormula()) { } else if (subFormula.isLongRunAverageOperatorFormula()) {
return this->checkLongRunAverageOperatorFormula(env, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula()));
return this->checkLongRunAverageOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula()));
} }
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkGameFormula NYI");
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Cannot check this property (yet).");
} }
template<typename ModelType> template<typename ModelType>
@ -73,26 +81,26 @@ namespace storm {
storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula(); storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula();
std::unique_ptr<CheckResult> result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula())); std::unique_ptr<CheckResult> result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula()));
return nullptr;
return result;
} }
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> 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.");
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, ValueType> const& checkTask) {
storm::logic::LongRunAverageOperatorFormula const& formula = checkTask.getFormula();
std::unique_ptr<CheckResult> result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula()));
return result;
} }
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, ValueType> 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<CheckResult> result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula()));
return result; //TODO check bounds.
template<typename ModelType>
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> 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 << "' cannot (yet) be handled.");
} }
template<typename SparseSmgModelType> template<typename SparseSmgModelType>
@ -107,9 +115,15 @@ namespace storm {
storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());
//std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values));
//return result;
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI");
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values)));
if (checkTask.isProduceSchedulersSet()) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));
}
return result;
}
template<typename SparseSmgModelType> template<typename SparseSmgModelType>
void SparseSmgRpatlModelChecker<SparseSmgModelType>::coalitionIndicator(Environment& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) { void SparseSmgRpatlModelChecker<SparseSmgModelType>::coalitionIndicator(Environment& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) {
storm::storage::BitVector coalitionIndicators(this->getModel().getTransitionMatrix().getRowGroupCount()); storm::storage::BitVector coalitionIndicators(this->getModel().getTransitionMatrix().getRowGroupCount());
@ -143,7 +157,6 @@ namespace storm {
template class SparseSmgRpatlModelChecker<storm::models::sparse::Smg<double>>; template class SparseSmgRpatlModelChecker<storm::models::sparse::Smg<double>>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class SparseSmgRpatlModelChecker<storm::models::sparse::Smg<storm::RationalNumber>>; template class SparseSmgRpatlModelChecker<storm::models::sparse::Smg<storm::RationalNumber>>;
//template class SparseSmgRpatlModelChecker<storm::models::sparse::Smg<storm::RationalFunction>>; TODO are we going to need this?
#endif #endif
} }
} }

14
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h
View File

@ -25,12 +25,14 @@ namespace storm {
static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState = nullptr); static bool canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState = nullptr);
// The implemented methods of the AbstractModelChecker interface. // The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
virtual std::unique_ptr<CheckResult> checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(Environment const& env, CheckTask<storm::logic::RewardOperatorFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
std::unique_ptr<CheckResult> checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> checkRewardOperatorFormula(Environment const& env, CheckTask<storm::logic::RewardOperatorFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
void coalitionIndicator(Environment& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask); void coalitionIndicator(Environment& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask);
}; };

Write Preview
Loading…
Cancel
Save