diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 774ef0014..6dff7e419 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -24,6 +24,8 @@ #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/shields/shield-handling.h" + #include "storm/settings/modules/GeneralSettings.h" #include "storm/exceptions/InvalidStateException.h" @@ -64,6 +66,10 @@ namespace storm { storm::logic::GameFormula const& gameFormula = checkTask.getFormula(); storm::logic::Formula const& subFormula = gameFormula.getSubformula(); + if(checkTask.isShieldingTask()) { + std::cout << "Creating Shield for " << checkTask.getShieldingExpression() << std::endl; + } + statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition()); if (subFormula.isRewardOperatorFormula()) { @@ -142,8 +148,13 @@ namespace storm { ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + for(auto const& x : ret.values) { + STORM_LOG_DEBUG("v: " << x); + } std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); - if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + if(checkTask.isShieldingTask()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(tempest::shields::createShield(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), statesOfCoalition))); + } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -203,9 +214,12 @@ namespace storm { auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); - if (checkTask.isProduceSchedulersSet()) { + if(checkTask.isShieldingTask()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(tempest::shields::createShield(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), coalitionStates))); + } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } + return result; }