From aece3020f6996591cb408e90396cd51e41fe7246 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 22 Jun 2018 15:04:07 +0200 Subject: [PATCH] improved functionality of the scheduler evaluator --- .../MultiObjectiveSchedulerEvaluator.cpp | 152 +++++++++++++++++- .../MultiObjectiveSchedulerEvaluator.h | 34 +++- 2 files changed, 178 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp index 5a25557ef..f1c78f98d 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp @@ -1,32 +1,172 @@ #include "storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h" + +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "storm/storage/BitVector.h" +#include "storm/utility/graph.h" +#include "storm/utility/vector.h" + +#include "storm/utility/constants.h" +#include "storm/storage/Scheduler.h" + +#include "storm/exceptions/NotSupportedException.h" + + namespace storm { namespace modelchecker { namespace multiobjective { template - MultiObjectiveSchedulerEvaluator::MultiObjectiveSchedulerEvaluator(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) { - // TODO + MultiObjectiveSchedulerEvaluator::MultiObjectiveSchedulerEvaluator(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : model(*preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives), currSchedHasBeenChecked(false) { + results.resize(this->objectives.size()); + currSched.resize(this->getModel().getNumberOfStates(), 0); + initializeSchedulerIndependentStates(); + } + + template + void MultiObjectiveSchedulerEvaluator::initializeSchedulerIndependentStates() { + storm::modelchecker::SparsePropositionalModelChecker mc(getModel()); + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + auto const& formula = *this->objectives[objIndex].formula; + if (formula.isProbabilityOperatorFormula() && formula.getSubformula().isUntilFormula()) { + storm::storage::BitVector phiStates = mc.check(formula.getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector psiStates = mc.check(formula.getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto backwardTransitions = getModel().getBackwardTransitions(); + storm::storage::BitVector prob1States = storm::utility::graph::performProb1A(getModel().getTransitionMatrix(), getModel().getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); + storm::storage::BitVector prob0States = storm::utility::graph::performProb0A(backwardTransitions, phiStates, psiStates); + storm::utility::vector::setVectorValues(results[objIndex], prob0States, storm::utility::zero()); + storm::utility::vector::setVectorValues(results[objIndex], prob1States, storm::utility::one()); + schedulerIndependentStates.push_back(prob1States | prob0States); + } else if (formula.getSubformula().isEventuallyFormula() && (formula.isRewardOperatorFormula() || formula.isTimeOperatorFormula())) { + storm::storage::BitVector rew0States = mc.check(formula.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + if (formula.isRewardOperatorFormula()) { + auto const& rewModel = formula.asRewardOperatorFormula().hasRewardModelName() ? getModel().getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()) : getModel().getUniqueRewardModel(); + storm::storage::BitVector statesWithoutReward = rewModel.getStatesWithZeroReward(getModel().getTransitionMatrix()); + rew0States = storm::utility::graph::performProb1A(getModel().getTransitionMatrix(), getModel().getNondeterministicChoiceIndices(), getModel().getBackwardTransitions(), statesWithoutReward, rew0States); + } + storm::utility::vector::setVectorValues(results[objIndex], rew0States, storm::utility::zero()); + schedulerIndependentStates.push_back(std::move(rew0States)); + } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isTotalRewardFormula()) { + auto const& rewModel = formula.asRewardOperatorFormula().hasRewardModelName() ? getModel().getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()) : getModel().getUniqueRewardModel(); + storm::storage::BitVector statesWithoutReward = rewModel.getStatesWithZeroReward(getModel().getTransitionMatrix()); + storm::storage::BitVector rew0States = storm::utility::graph::performProbGreater0E(getModel().getBackwardTransitions(), statesWithoutReward, ~statesWithoutReward); + rew0States.complement(); + storm::utility::vector::setVectorValues(results[objIndex], rew0States, storm::utility::zero()); + schedulerIndependentStates.push_back(std::move(rew0States)); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The given formula " << formula << " is not supported."); + } + } + } + + template + std::unique_ptr invokeModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + if (model->getType() == storm::models::ModelType::Dtmc) { + return storm::modelchecker::SparseDtmcPrctlModelChecker>(*model->template as>()).check(env, task); + } else if(model->getType() == storm::models::ModelType::Ctmc) { + return storm::modelchecker::SparseCtmcCslModelChecker>(*model->template as>()).check(env, task); + } else { + STORM_LOG_ASSERT(false, "invalid model type"); + } + } + + template + void MultiObjectiveSchedulerEvaluator::check(Environment const& env) { + if (!currSchedHasBeenChecked) { + storm::storage::Scheduler scheduler(model.getNumberOfStates()); + for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) { + scheduler.setChoice(currSched[state], state); + } + + auto detModel = model.applyScheduler(scheduler, false); + + for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + storm::modelchecker::CheckTask task(*this->objectives[objIndex].formula, false); + auto res = invokeModelChecker(env, detModel, task); + results[objIndex] = std::move(res->template asExplicitQuantitativeCheckResult().getValueVector()); + } + currSchedHasBeenChecked = true; + } + } + + template + ModelType const& MultiObjectiveSchedulerEvaluator::getModel() const { + return model; + } + + template + std::vector::ValueType>> const& MultiObjectiveSchedulerEvaluator::getObjectives() const { + return objectives; + } + + template + std::vector const& MultiObjectiveSchedulerEvaluator::getScheduler() const { + return currSched; } template - void MultiObjectiveSchedulerEvaluator::check(std::vector const& scheduler) { - // TODO + bool MultiObjectiveSchedulerEvaluator::hasCurrentSchedulerBeenChecked() const { + return currSchedHasBeenChecked; + } + + template + uint64_t const& MultiObjectiveSchedulerEvaluator::getChoiceAtState(uint64_t state) const { + return currSched[state]; + } + + template + void MultiObjectiveSchedulerEvaluator::setChoiceAtState(uint64_t state, uint64_t choice) { + if (currSched[state] != choice) { + STORM_LOG_ASSERT(choice < this->getModel().getTransitionMatrix().getRowGroupSize(state), "Invalid choice index."); + currSched[state] = choice; + currSchedHasBeenChecked = false; + } } template std::vector::ValueType> const& MultiObjectiveSchedulerEvaluator::getResultForObjective(uint64_t objIndex) const { + STORM_LOG_ASSERT(currSchedHasBeenChecked, "Tried to get results for a scheduler that has not yet been analyzed."); return results[objIndex]; } template - std::vector MultiObjectiveSchedulerEvaluator::getInitialStateResults() const { + std::vector::ValueType>> const& MultiObjectiveSchedulerEvaluator::getResults() const { + STORM_LOG_ASSERT(currSchedHasBeenChecked, "Tried to get results for a scheduler that has not yet been analyzed."); + return results; + } + + template + storm::storage::BitVector const& MultiObjectiveSchedulerEvaluator::getSchedulerIndependentStates(uint64_t objIndex) const { + return schedulerIndependentStates[objIndex]; + } + + template + std::vector::ValueType> MultiObjectiveSchedulerEvaluator::getInitialStateResults() const { + STORM_LOG_ASSERT(currSchedHasBeenChecked, "Tried to get results for a scheduler that has not yet been analyzed."); + STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Getting initial state result ist only supported for models with a single initial state."); std::vector res; for (auto objResult : results) { - res.push_back(objResult[initialState]); + res.push_back(objResult[*model.getInitialStates().begin()]); } return res; } + + + + template class MultiObjectiveSchedulerEvaluator>; + template class MultiObjectiveSchedulerEvaluator>; + template class MultiObjectiveSchedulerEvaluator>; + template class MultiObjectiveSchedulerEvaluator>; + } } } \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h index 0a4ef3c0d..edb68b705 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h @@ -5,6 +5,12 @@ #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" namespace storm { + + class Environment; + namespace storage { + class BitVector; + } + namespace modelchecker { namespace multiobjective { @@ -16,14 +22,38 @@ namespace storm { MultiObjectiveSchedulerEvaluator(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); - void check(std::vector const& scheduler); + /*! + * Instantiates the given model with the provided scheduler and checks the objectives individually under that scheduler. + */ + void check(Environment const& env); + // Retrieve the results after calling check. + std::vector> const& getResults() const; std::vector const& getResultForObjective(uint64_t objIndex) const; + storm::storage::BitVector const& getSchedulerIndependentStates(uint64_t objIndex) const; std::vector getInitialStateResults() const; + ModelType const& getModel() const; + std::vector> const& getObjectives() const; + bool hasCurrentSchedulerBeenChecked() const; + std::vector const& getScheduler() const; + uint64_t const& getChoiceAtState(uint64_t state) const; + void setChoiceAtState(uint64_t state, uint64_t choice); + private: + + void initializeSchedulerIndependentStates(); + + ModelType const& model; + std::vector> const& objectives; + + // Indicates for each objective the set of states for which the result is fix (i.e. independent of the scheduler). + std::vector schedulerIndependentStates; + + // Stores the results from the last call to check std::vector> results; - uint64_t initialState; + std::vector currSched; + bool currSchedHasBeenChecked; }; } }