From 8c09a4d4418485244746a4c01fc06868128f5cac Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 20 Sep 2021 18:36:56 +0200 Subject: [PATCH 01/13] refactored safety shield choices and scheduler --- src/storm/shields/PostSafetyShield.cpp | 14 ++--- src/storm/shields/PreSafetyShield.cpp | 13 ++-- src/storm/storage/PostScheduler.cpp | 74 +++++++++-------------- src/storm/storage/PostScheduler.h | 22 +++---- src/storm/storage/PostSchedulerChoice.cpp | 63 +++++++++++++++++++ src/storm/storage/PostSchedulerChoice.h | 46 ++++++++++++++ src/storm/storage/PreScheduler.cpp | 43 ++++++++++--- src/storm/storage/PreScheduler.h | 28 ++++++--- src/storm/storage/PreSchedulerChoice.cpp | 56 +++++++++++++++++ src/storm/storage/PreSchedulerChoice.h | 42 +++++++++++++ 10 files changed, 312 insertions(+), 89 deletions(-) create mode 100644 src/storm/storage/PostSchedulerChoice.cpp create mode 100644 src/storm/storage/PostSchedulerChoice.h create mode 100644 src/storm/storage/PreSchedulerChoice.cpp create mode 100644 src/storm/storage/PreSchedulerChoice.h diff --git a/src/storm/shields/PostSafetyShield.cpp b/src/storm/shields/PostSafetyShield.cpp index 9c639c010..311da2832 100644 --- a/src/storm/shields/PostSafetyShield.cpp +++ b/src/storm/shields/PostSafetyShield.cpp @@ -43,28 +43,28 @@ namespace tempest { ValueType maxProbability = *(choice_it + maxProbabilityIndex); if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); - shield.setChoice(0, storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); choice_it += rowGroupSize; continue; } + storm::storage::PostSchedulerChoice choiceMapping; for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - storm::storage::Distribution actionDistribution; if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { - actionDistribution.addProbability(choice, 1); + choiceMapping.addChoice(choice, choice); } else { - actionDistribution.addProbability(maxProbabilityIndex, 1); + choiceMapping.addChoice(choice, maxProbabilityIndex); } - shield.setChoice(choice, storm::storage::SchedulerChoice(actionDistribution), state); } + shield.setChoice(choiceMapping, state, 0); } else { - shield.setChoice(0, storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); choice_it += rowGroupSize; } } return shield; } - // Explicitly instantiate appropriate + // Explicitly instantiate appropriate classes template class PostSafetyShield::index_type>; #ifdef STORM_HAVE_CARL template class PostSafetyShield::index_type>; diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp index abbc50ae7..f4374b929 100644 --- a/src/storm/shields/PreSafetyShield.cpp +++ b/src/storm/shields/PreSafetyShield.cpp @@ -39,29 +39,30 @@ namespace tempest { for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; if(this->relevantStates.get(state)) { - storm::storage::Distribution actionDistribution; + storm::storage::PreSchedulerChoice enabledChoices; ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize); if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); - shield.setChoice(storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PreSchedulerChoice(), state, 0); choice_it += rowGroupSize; continue; } for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { - actionDistribution.addProbability(choice, *choice_it); + enabledChoices.addChoice(choice, *choice_it); } } - shield.setChoice(storm::storage::SchedulerChoice(actionDistribution), state); + shield.setChoice(enabledChoices, state, 0); } else { - shield.setChoice(storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PreSchedulerChoice(), state, 0); choice_it += rowGroupSize; } + } return shield; } - // Explicitly instantiate appropriate + // Explicitly instantiate appropriate classes template class PreSafetyShield::index_type>; #ifdef STORM_HAVE_CARL template class PreSafetyShield::index_type>; diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 92a81b434..11d0a7aed 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/src/storm/storage/PostScheduler.cpp @@ -9,14 +9,10 @@ namespace storm { namespace storage { template - PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { - STORM_LOG_DEBUG(numberOfChoicesPerState.size() << " " << numberOfModelStates); - STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); + PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { + //STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; - schedulerChoiceMapping = std::vector>>>(numOfMemoryStates, std::vector>>(numberOfModelStates)); - for(uint state = 0; state < numberOfModelStates; state++) { - schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]); - } + schedulerChoiceMapping = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); numberOfChoices = 0; for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) numberOfChoices += *it; @@ -25,13 +21,10 @@ namespace storm { } template - PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; - schedulerChoiceMapping = std::vector>>>(numOfMemoryStates, std::vector>>(numberOfModelStates)); - for(uint state = 0; state < numberOfModelStates; state++) { - schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]); - } + schedulerChoiceMapping = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); numberOfChoices = 0; for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) numberOfChoices += *it; @@ -40,21 +33,13 @@ namespace storm { } template - void PostScheduler::setChoice(OldChoice const& oldChoice, SchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState) { + void PostScheduler::setChoice(PostSchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { STORM_LOG_ASSERT(memoryState == 0, "Currently we do not support PostScheduler with memory"); STORM_LOG_ASSERT(modelState < schedulerChoiceMapping[memoryState].size(), "Illegal model state index"); - schedulerChoiceMapping[memoryState][modelState][oldChoice] = newChoice; - } - - template - SchedulerChoice const& PostScheduler::getChoice(uint_fast64_t modelState, OldChoice oldChoice, uint_fast64_t memoryState) { - STORM_LOG_ASSERT(memoryState < this->getNumberOfMemoryStates(), "Illegal memory state index"); - STORM_LOG_ASSERT(modelState < schedulerChoiceMapping[memoryState].size(), "Illegal model state index"); - return schedulerChoiceMapping[memoryState][modelState][oldChoice]; + schedulerChoiceMapping[memoryState][modelState] = choice; } - template bool PostScheduler::isDeterministicScheduler() const { return true; @@ -89,7 +74,11 @@ namespace storm { out << ":" << std::endl; uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; for (uint_fast64_t state = 0; state < schedulerChoiceMapping.front().size(); ++state) { + PostSchedulerChoice const& choices = schedulerChoiceMapping[0][state]; + if(choices.isEmpty() && !printUndefinedChoices) continue; + std::stringstream stateString; + // Print the state info if (stateValuationsGiven) { stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); @@ -98,42 +87,37 @@ namespace storm { } stateString << " "; + bool firstChoiceIndex = true; - for(uint choiceIndex = 0; choiceIndex < schedulerChoiceMapping[0][state].size(); choiceIndex++) { - SchedulerChoice const& choice = schedulerChoiceMapping[0][state][choiceIndex]; + for(auto const& choiceMap : choices.getChoiceMap()) { if(firstChoiceIndex) { firstChoiceIndex = false; } else { stateString << "; "; } - if (choice.isDefined()) { - auto choiceProbPair = *(choice.getChoiceAsDistribution().begin()); - if(choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceIndex); - stateString << std::to_string(choiceIndex) << " {" << boost::join(choiceLabels, ", ") << "}: "; - } else { - stateString << std::to_string(choiceIndex) << ": "; - } - //stateString << choiceProbPair.second << ": ("; - if (choiceOriginsGiven) { - stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - } else { - stateString << choiceProbPair.first; - } - if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - stateString << " {" << boost::join(choiceLabels, ", ") << "}"; - } + if(choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<0>(choiceMap)); + stateString << std::to_string(std::get<0>(choiceMap)) << " {" << boost::join(choiceLabels, ", ") << "}: "; + } else { + stateString << std::to_string(std::get<0>(choiceMap)) << ": "; + } + + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceMap)); } else { - if(!this->printUndefinedChoices) goto skipStatesWithUndefinedChoices; - stateString << "undefined."; + stateString << std::to_string(std::get<1>(choiceMap)); } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceMap)); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } + // Todo: print memory updates } out << stateString.str() << std::endl; // jump to label if we find one undefined choice. - skipStatesWithUndefinedChoices:; + //skipStatesWithUndefinedChoices:; } out << "___________________________________________________________________" << std::endl; } diff --git a/src/storm/storage/PostScheduler.h b/src/storm/storage/PostScheduler.h index 57c194fa6..99fc3c1b8 100644 --- a/src/storm/storage/PostScheduler.h +++ b/src/storm/storage/PostScheduler.h @@ -2,7 +2,7 @@ #include #include -#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/PostSchedulerChoice.h" #include "storm/storage/Scheduler.h" #include "storm/logic/ShieldExpression.h" @@ -16,7 +16,7 @@ namespace storm { * A Choice can be undefined, deterministic */ template - class PostScheduler : public Scheduler { + class PostScheduler { public: typedef uint_fast64_t OldChoice; /*! @@ -35,7 +35,7 @@ namespace storm { * @param modelState The state of the model for which to set the choice. * @param memoryState The state of the memoryStructure for which to set the choice. */ - void setChoice(OldChoice const& oldChoice, SchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState = 0); + void setChoice(PostSchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState = 0); /*! * Is the scheduler defined on the states indicated by the selected-states bitvector? @@ -50,14 +50,6 @@ namespace storm { */ void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0); - /*! - * Gets the choice defined by the scheduler for the given model and memory state. - * - * @param state The state for which to get the choice. - * @param memoryState the memory state which we consider. - */ - SchedulerChoice const& getChoice(uint_fast64_t modelState, OldChoice oldChoice, uint_fast64_t memoryState = 0) ; - /*! * Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state */ @@ -92,8 +84,14 @@ namespace storm { */ void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; private: - std::vector>>> schedulerChoiceMapping; + boost::optional memoryStructure; + std::vector>> schedulerChoiceMapping; + + bool printUndefinedChoices = false; + uint_fast64_t numOfUndefinedChoices; + uint_fast64_t numOfDeterministicChoices; + uint_fast64_t numOfDontCareStates; std::vector numberOfChoicesPerState; uint_fast64_t numberOfChoices; }; diff --git a/src/storm/storage/PostSchedulerChoice.cpp b/src/storm/storage/PostSchedulerChoice.cpp new file mode 100644 index 000000000..ca714a6a4 --- /dev/null +++ b/src/storm/storage/PostSchedulerChoice.cpp @@ -0,0 +1,63 @@ +#include "storm/storage/PostSchedulerChoice.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + namespace storage { + + template + PostSchedulerChoice::PostSchedulerChoice() { + // Intentionally left empty + } + + template + void PostSchedulerChoice::addChoice(uint_fast64_t oldChoiceIndex, uint_fast64_t newChoiceIndex) { + choiceMap.emplace_back(oldChoiceIndex, newChoiceIndex); + } + + template + std::vector> const& PostSchedulerChoice::getChoiceMap() const { + return choiceMap; + } + + template + std::tuple const& PostSchedulerChoice::getChoice(uint_fast64_t choiceIndex) const { + return choiceMap.at(choiceIndex); + } + + template + bool PostSchedulerChoice::isEmpty() const { + return choiceMap.size() == 0; + } + + template + std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice) { + if (!schedulerChoice.isEmpty()) { + bool firstChoice = true; + for(auto const& choice : schedulerChoice.getChoiceMap()) { + if(firstChoice) firstChoice = false; + else out << ", "; + out << std::get<0>(choice) << " -> " << std::get<1>(choice); + } + } else { + out << "undefined"; + } + return out; + } + + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + template class PostSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + + } +} diff --git a/src/storm/storage/PostSchedulerChoice.h b/src/storm/storage/PostSchedulerChoice.h new file mode 100644 index 000000000..29deb3ddb --- /dev/null +++ b/src/storm/storage/PostSchedulerChoice.h @@ -0,0 +1,46 @@ +#pragma once + +#include "storm/utility/constants.h" + +namespace storm { + namespace storage { + + template + class PostSchedulerChoice { + + public: + + /*! + * Creates an undefined scheduler choice + */ + PostSchedulerChoice(); + + /* + * + */ + void addChoice(uint_fast64_t oldChoiceIndex, uint_fast64_t newChoiceIndex); + + /* + * + */ + bool isEmpty() const; + + /* + * + */ + std::vector> const& getChoiceMap() const; + + /* + * + */ + std::tuple const& getChoice(uint_fast64_t choiceIndex) const; + + private: + //std::vector>> choiceMap; + std::vector> choiceMap; + }; + + template + std::ostream& operator<<(std::ostream& out, PostSchedulerChoice const& schedulerChoice); + } +} diff --git a/src/storm/storage/PreScheduler.cpp b/src/storm/storage/PreScheduler.cpp index 0f1cf775d..bb09a81f1 100644 --- a/src/storm/storage/PreScheduler.cpp +++ b/src/storm/storage/PreScheduler.cpp @@ -8,11 +8,36 @@ namespace storm { namespace storage { template - PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { + uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; + schedulerChoices = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); + //dontCareStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, false)); + numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; + numOfDeterministicChoices = 0; + numOfDontCareStates = 0; } template - PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { + } + + template + bool PreScheduler::isMemorylessScheduler() const { + return getNumberOfMemoryStates() == 1; + } + + template + uint_fast64_t PreScheduler::getNumberOfMemoryStates() const { + return memoryStructure ? memoryStructure->getNumberOfStates() : 1; + } + + template + void PreScheduler::setChoice(PreSchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { + STORM_LOG_ASSERT(memoryState < this->getNumberOfMemoryStates(), "Illegal memory state index"); + STORM_LOG_ASSERT(modelState < this->schedulerChoices[memoryState].size(), "Illegal model state index"); + + auto& schedulerChoice = schedulerChoices[memoryState][modelState]; + schedulerChoice = choice; } template @@ -67,23 +92,23 @@ namespace storm { } // Print choice info - SchedulerChoice const& choice = this->schedulerChoices[memoryState][state]; - if (choice.isDefined()) { + PreSchedulerChoice const& choices = this->schedulerChoices[memoryState][state]; + if (!choices.isEmpty()) { bool firstChoice = true; - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + for (auto const& choiceProbPair : choices.getChoiceMap()) { if (firstChoice) { firstChoice = false; } else { stateString << "; "; } - stateString << choiceProbPair.second << ": ("; + stateString << std::get<0>(choiceProbPair) << ": ("; if (choiceOriginsGiven) { - stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceProbPair)); } else { - stateString << choiceProbPair.first; + stateString << std::get<1>(choiceProbPair); } if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceProbPair)); stateString << " {" << boost::join(choiceLabels, ", ") << "}"; } stateString << ")"; diff --git a/src/storm/storage/PreScheduler.h b/src/storm/storage/PreScheduler.h index 8207456e1..5cfa2e8cb 100644 --- a/src/storm/storage/PreScheduler.h +++ b/src/storm/storage/PreScheduler.h @@ -3,7 +3,7 @@ #include #include #include -#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/PreSchedulerChoice.h" #include "storm/storage/Scheduler.h" #include "storm/logic/ShieldExpression.h" @@ -12,14 +12,11 @@ namespace storm { /* * TODO needs obvious changes in all comment blocks - * This class defines which action is chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i - * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). - * A Choice can be undefined, deterministic */ template - class PreScheduler : public Scheduler { + class PreScheduler { public: - typedef uint_fast64_t OldChoice; + /*! * Initializes a scheduler for the given number of model states. * @@ -29,14 +26,25 @@ namespace storm { PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); + bool isMemorylessScheduler() const; + uint_fast64_t getNumberOfMemoryStates() const; + + void setChoice(PreSchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState); + /*! * Prints the scheduler to the given output stream. - * @param out The output stream - * @param model If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices) - * @param skipUniqueChoices If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. - * Requires a model to be given. */ void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + + private: + boost::optional memoryStructure; + std::vector>> schedulerChoices; + + bool printUndefinedChoices = false; + + uint_fast64_t numOfUndefinedChoices; + uint_fast64_t numOfDeterministicChoices; + uint_fast64_t numOfDontCareStates; }; } } diff --git a/src/storm/storage/PreSchedulerChoice.cpp b/src/storm/storage/PreSchedulerChoice.cpp new file mode 100644 index 000000000..e9fda23ac --- /dev/null +++ b/src/storm/storage/PreSchedulerChoice.cpp @@ -0,0 +1,56 @@ +#include "storm/storage/PreSchedulerChoice.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + namespace storage { + + template + PreSchedulerChoice::PreSchedulerChoice() { + // Intentionally left empty + } + + template + void PreSchedulerChoice::addChoice(uint_fast64_t choiceIndex, ValueType probToSatisfy) { + choiceMap.emplace_back(probToSatisfy, choiceIndex); + } + + template + std::vector> const& PreSchedulerChoice::getChoiceMap() const { + return choiceMap; + } + + template + bool PreSchedulerChoice::isEmpty() const { + return choiceMap.size() == 0; + } + + template + std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice) { + out << schedulerChoice.getChoiceMap().size(); + if (!schedulerChoice.isEmpty()) { + for(auto const& choice : schedulerChoice.getChoiceMap()) { + out << std::get<0>(choice) << ": " << std::get<1>(choice); + } + } else { + out << "undefined"; + } + return out; + } + + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + template class PreSchedulerChoice; + template std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + + } +} diff --git a/src/storm/storage/PreSchedulerChoice.h b/src/storm/storage/PreSchedulerChoice.h new file mode 100644 index 000000000..3e4074e84 --- /dev/null +++ b/src/storm/storage/PreSchedulerChoice.h @@ -0,0 +1,42 @@ +#pragma once + +#include "storm/utility/constants.h" + +namespace storm { + namespace storage { + + template + class PreSchedulerChoice { + + public: + + /*! + * Creates an undefined scheduler choice + */ + PreSchedulerChoice(); + + /* + * + */ + void addChoice(uint_fast64_t choiceIndex, ValueType probToSatisfy); + + /* + * + */ + bool isEmpty() const; + + /* + * + */ + std::vector> const& getChoiceMap() const; + + private: + // For now we only consider shields with deterministic choices. + //std::map> choiceMap; + std::vector> choiceMap; + }; + + template + std::ostream& operator<<(std::ostream& out, PreSchedulerChoice const& schedulerChoice); + } +} From 48d37ccc502c0fbd3739756f3accd445aa57d32a Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 20 Sep 2021 18:53:56 +0200 Subject: [PATCH 02/13] fixed intending --- src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 3e8cd7569..f44a7cef7 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -216,7 +216,7 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); } return result; } From 5bf552a43aa9d35a6e962c190aab16b964d1653c Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 28 Sep 2021 18:27:00 +0200 Subject: [PATCH 03/13] multiplier reduce also returns choices --- src/storm/solver/Multiplier.cpp | 29 +++++++++++++++-------------- src/storm/solver/Multiplier.h | 2 +- 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index e5df00b05..4e4fa9abe 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -75,7 +75,7 @@ namespace storm { progress.startNewMeasurement(0); for (uint64_t i = 0; i < n; ++i) { multiply(env, x, b, choiceValues); - reduce(env, dir, choiceValues, rowGroupIndices, x); + reduce(env, dir, rowGroupIndices, choiceValues, x); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications"); break; @@ -90,33 +90,34 @@ namespace storm { } template - void Multiplier::reduce(Environment const& env, OptimizationDirection const& dir, std::vector const& choiceValues, std::vector::index_type> rowGroupIndices, std::vector& result, storm::storage::BitVector const* dirOverride) const { - auto choice_it = choiceValues.begin(); + void Multiplier::reduce(Environment const& env, OptimizationDirection const& dir, std::vector::index_type> const& rowGroupIndices, std::vector const& choiceValues, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { + auto choiceValue_it = choiceValues.begin(); + auto optChoice_it = choiceValues.begin(); for(uint state = 0; state < rowGroupIndices.size(); state++) { uint rowGroupSize; if(state == 0) { rowGroupSize = rowGroupIndices[state]; } else { - rowGroupSize = rowGroupIndices[state] - rowGroupIndices[state-1]; + rowGroupSize = rowGroupIndices[state] - rowGroupIndices[state - 1]; } if(dirOverride != nullptr) { if((dir == storm::OptimizationDirection::Minimize && !dirOverride->get(state)) || (dir == storm::OptimizationDirection::Maximize && dirOverride->get(state))) { - result.at(state) = *std::min_element(choice_it, choice_it + rowGroupSize); - choice_it += rowGroupSize; - } - else { - result.at(state) = *std::max_element(choice_it, choice_it + rowGroupSize); - choice_it += rowGroupSize; + optChoice_it = std::min_element(choiceValue_it, choiceValue_it + rowGroupSize); + } else { + optChoice_it = std::max_element(choiceValue_it, choiceValue_it + rowGroupSize); } } else { if(dir == storm::OptimizationDirection::Minimize) { - result.at(state) = *std::min_element(choice_it, choice_it + rowGroupSize); - choice_it += rowGroupSize; + optChoice_it = std::min_element(choiceValue_it, choiceValue_it + rowGroupSize); } else { - result.at(state) = *std::max_element(choice_it, choice_it + rowGroupSize); - choice_it += rowGroupSize; + optChoice_it = std::max_element(choiceValue_it, choiceValue_it + rowGroupSize); } } + result.at(state) = *optChoice_it; + if(choices) { + choices->at(state) = std::distance(choiceValue_it, optChoice_it); + } + choiceValue_it += rowGroupSize; } } diff --git a/src/storm/solver/Multiplier.h b/src/storm/solver/Multiplier.h index 5e132a628..fc300ff4b 100644 --- a/src/storm/solver/Multiplier.h +++ b/src/storm/solver/Multiplier.h @@ -141,7 +141,7 @@ namespace storm { */ virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const; - void reduce(Environment const& env, OptimizationDirection const& dir, std::vector const& choiceValues, std::vector::index_type> rowGroupIndices, std::vector& result, storm::storage::BitVector const* dirOverride = nullptr) const; + void reduce(Environment const& env, OptimizationDirection const& dir, std::vector::index_type> const& rowGroupIndices, std::vector const& choiceValues, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; protected: mutable std::unique_ptr> cachedVector; From e406b00c024e1aaa7bb953ceeb6b243e6c301cc6 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 28 Sep 2021 18:29:45 +0200 Subject: [PATCH 04/13] 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; }; } From 7f5f6eeee0d8d2eb5bc5ea56a75f627ac58da3e2 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 28 Sep 2021 18:30:43 +0200 Subject: [PATCH 05/13] adapted to changes for Multiplier::reduce --- src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 2 +- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 461435816..68951bf1b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -146,7 +146,7 @@ namespace storm { if(goal.isShieldingTask()) { multiplier->multiply(env, result, nullptr, choiceValues); - multiplier->reduce(env, goal.direction(), choiceValues, transitionMatrix.getRowGroupIndices(), result, nullptr); + multiplier->reduce(env, goal.direction(), transitionMatrix.getRowGroupIndices(), choiceValues, result); } else { multiplier->multiplyAndReduce(env, dir, result, nullptr, result); diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index bc18f35ff..31ddac9da 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -112,7 +112,7 @@ namespace storm { auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); auto rowGroupIndices = transitionMatrix.getRowGroupIndices(); rowGroupIndices.erase(rowGroupIndices.begin()); - multiplier->reduce(env, goal.direction(), b, rowGroupIndices, result, &statesOfCoalition); + multiplier->reduce(env, goal.direction(), rowGroupIndices, b, result, nullptr, &statesOfCoalition); if (goal.isShieldingTask()) { choiceValues = b; } From 01335948d4236fe0d60f88c6179658ee603e5d75 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 28 Sep 2021 18:31:05 +0200 Subject: [PATCH 06/13] LraViHelper now also computes all choiceValues --- ...eNondeterministicInfiniteHorizonHelper.cpp | 8 ++-- .../infinitehorizon/internal/LraViHelper.cpp | 38 ++++++++++++++++--- .../infinitehorizon/internal/LraViHelper.h | 6 ++- 3 files changed, 41 insertions(+), 11 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp index 1fc6aa295..907d76ecb 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp @@ -183,19 +183,19 @@ namespace storm { } else { // We assume an MDP (with nondeterministic timed states and no instant states) storm::modelchecker::helper::internal::LraViHelper viHelper(mec, this->_transitionMatrix, aperiodicFactor); - return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices); + return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices, choiceValues); } } - + template ValueType SparseNondeterministicInfiniteHorizonHelper::computeLraForMecLp(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& mec) { // Create an LP solver auto solver = storm::utility::solver::LpSolverFactory().create("LRA for MEC"); - + // Now build the LP formulation as described in: // Guck et al.: Modelling and Analysis of Markov Reward Automata (ATVA'14), https://doi.org/10.1007/978-3-319-11936-6_13 solver->setOptimizationDirection(invert(this->getOptimizationDirection())); - + // Create variables // TODO: Investigate whether we can easily make the variables bounded std::map stateToVariableMap; diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 15c12ba95..83181ca37 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -159,7 +159,7 @@ namespace storm { template - ValueType LraViHelper::performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates, storm::solver::OptimizationDirection const* dir, std::vector* choices) { + ValueType LraViHelper::performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates, storm::solver::OptimizationDirection const* dir, std::vector* choices, std::vector* choiceValues) { initializeNewValues(stateValueGetter, actionValueGetter, exitRates); ValueType precision = storm::utility::convertNumber(env.solver().lra().getPrecision()); bool relative = env.solver().lra().getRelativeTerminationCriterion(); @@ -219,7 +219,7 @@ namespace storm { if(!gameNondetTs()) { prepareNextIteration(env); } - performIterationStep(env, dir, choices); + performIterationStep(env, dir, choices, choiceValues); } if(gameNondetTs()) { storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); @@ -358,7 +358,20 @@ namespace storm { } template - void LraViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir, std::vector* choices) { + void LraViHelper::setInputModelChoiceValues(std::vector& choiceValues, std::vector const& localMecChoiceValues) const { + // Transform the local choiceValues (within this mec) to choice values for the input model + uint64_t localState = 0; + for (auto const& element : _component) { + uint64_t elementState = element.first; + uint64_t rowIndex = _transitionMatrix.getRowGroupIndices()[elementState]; + uint64_t rowGroupSize = _transitionMatrix.getRowGroupEntryCount(elementState); + std::copy(localMecChoiceValues.begin(), localMecChoiceValues.begin() + rowGroupSize, &choiceValues.at(rowIndex)); + localState++; + } + } + + template + void LraViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir, std::vector* choices, std::vector* choiceValues) { STORM_LOG_ASSERT(!((nondetTs() || nondetIs()) && dir == nullptr), "No optimization direction provided for model with nondeterminism"); // Initialize value vectors, multiplers, and solver if this has not been done, yet if (!_TsMultiplier) { @@ -378,19 +391,34 @@ namespace storm { } else { // Also keep track of the choices made. std::vector tsChoices(_TsTransitions.getRowGroupCount()); - _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices); + std::vector resultChoiceValues(_TsTransitions.getRowCount()); + + _TsMultiplier->multiply(env, xOld(), &_TsChoiceValues, resultChoiceValues); + auto rowGroupIndices = this->_TsTransitions.getRowGroupIndices(); + rowGroupIndices.erase(rowGroupIndices.begin()); + _TsMultiplier->reduce(env, *dir, rowGroupIndices, resultChoiceValues, xNew(), &tsChoices); + // Note that nondeterminism within the timed states means that there can not be instant states (We either have MDPs or MAs) // Hence, in this branch we don't have to care for choices at instant states. STORM_LOG_ASSERT(!_hasInstantStates, "Nondeterministic timed states are only supported if there are no instant states."); setInputModelChoices(*choices, tsChoices); + setInputModelChoiceValues(*choiceValues, resultChoiceValues); } } else if(gameNondetTs()) { // TODO DRYness? exact same behaviour as case above? if (choices == nullptr) { _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), nullptr, _statesOfCoalition); } else { + // Also keep track of the choices made. std::vector tsChoices(_TsTransitions.getRowGroupCount()); - _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices, _statesOfCoalition); + std::vector resultChoiceValues(_TsTransitions.getRowCount()); + + _TsMultiplier->multiply(env, xOld(), &_TsChoiceValues, resultChoiceValues); + auto rowGroupIndices = this->_TsTransitions.getRowGroupIndices(); + rowGroupIndices.erase(rowGroupIndices.begin()); + _TsMultiplier->reduce(env, *dir, rowGroupIndices, resultChoiceValues, xNew(), &tsChoices); + setInputModelChoices(*choices, tsChoices); // no components -> no need for that call? + setInputModelChoiceValues(*choiceValues, resultChoiceValues); } } else { _TsMultiplier->multiply(env, xOld(), &_TsChoiceValues, xNew()); diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h index abd1576de..369d718b8 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h @@ -68,7 +68,7 @@ namespace storm { * @return The (optimal) long run average value of the specified component. * @note it is possible to call this method multiple times with different values. However, other changes to the environment or the optimization direction might not have the expected effect due to caching. */ - ValueType performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates = nullptr, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr); + ValueType performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates = nullptr, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr, std::vector* choiceValues = nullptr); private: @@ -89,7 +89,7 @@ namespace storm { * Note that these choices will be inserted w.r.t. the original model states/choices, i.e. the size of the vector should match the state-count of the input model * @pre when calling this the first time, initializeNewValues must have been called before. Moreover, prepareNextIteration must be called between two calls of this. */ - void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr); + void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr, std::vector* choiceValues = nullptr); struct ConvergenceCheckResult { bool isPrecisionAchieved; @@ -111,6 +111,8 @@ namespace storm { void setInputModelChoices(std::vector& choices, std::vector const& localMecChoices, bool setChoiceZeroToMarkovianStates = false, bool setChoiceZeroToProbabilisticStates = false) const; + void setInputModelChoiceValues(std::vector& choiceValues, std::vector const& localMecChoiceValues) const; + /// Returns true iff the given state is a timed state bool isTimedState(uint64_t const& inputModelStateIndex) const; From 454bffe03f76ba2bc5d054f0e589b5747ca7c988 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 10:39:52 +0100 Subject: [PATCH 07/13] major changes to shield handling - Introduced OptimalPre and OptimalPost shields - Renamed *Safety to PreShield and PostShield - Introduced min case for shields - fixed coalition states in shield handling --- .../parser/FormulaParserGrammar.cpp | 20 ++++--- .../parser/FormulaParserGrammar.h | 2 +- src/storm/logic/ShieldExpression.cpp | 26 +++++---- src/storm/logic/ShieldExpression.h | 10 ++-- src/storm/shields/AbstractShield.h | 8 ++- src/storm/shields/OptimalShield.cpp | 54 ++++++++++++++++--- src/storm/shields/OptimalShield.h | 10 ++-- .../{PostSafetyShield.cpp => PostShield.cpp} | 27 +++++----- .../{PostSafetyShield.h => PostShield.h} | 4 +- .../{PreSafetyShield.cpp => PreShield.cpp} | 25 +++++---- .../{PreSafetyShield.h => PreShield.h} | 4 +- src/storm/shields/ShieldHandling.cpp | 19 ++++--- src/storm/shields/ShieldHandling.h | 6 +-- .../storm/parser/GameShieldingParserTest.cpp | 12 ++--- .../storm/parser/MdpShieldingParserTest.cpp | 12 ++--- 15 files changed, 153 insertions(+), 86 deletions(-) rename src/storm/shields/{PostSafetyShield.cpp => PostShield.cpp} (62%) rename src/storm/shields/{PostSafetyShield.h => PostShield.h} (53%) rename src/storm/shields/{PreSafetyShield.cpp => PreShield.cpp} (62%) rename src/storm/shields/{PreSafetyShield.h => PreShield.h} (53%) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index ea96f31a2..2aae130bd 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -184,16 +184,21 @@ namespace storm { shieldExpression.name("shield expression"); - shieldingType = (qi::lit("PreSafety")[qi::_val = storm::logic::ShieldingType::PreSafety] | - qi::lit("PostSafety")[qi::_val = storm::logic::ShieldingType::PostSafety] | - qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield"); + shieldingType = (qi::lit("PreSafety")[qi::_val = storm::logic::ShieldingType::PreSafety] | + qi::lit("PostSafety")[qi::_val = storm::logic::ShieldingType::PostSafety] | + qi::lit("OptimalPre")[qi::_val = storm::logic::ShieldingType::OptimalPre] | + qi::lit("OptimalPost")[qi::_val = storm::logic::ShieldingType::OptimalPost] | + qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::OptimalPost]) // backwards compatability, will be disabled in the future + > -qi::lit("Shield"); shieldingType.name("shielding type"); - probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ]; - probability.name("double between 0 and 1"); + //probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ]; + //probability.name("double between 0 and 1"); + comparisonValue = qi::double_[qi::_val = qi::_1 ]; + comparisonValue.name("double comparison value"); shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | - qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; + qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > comparisonValue)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; shieldComparison.name("shield comparison type"); #pragma clang diagnostic push @@ -649,10 +654,9 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct) { if(comparisonStruct.is_initialized()) { - STORM_LOG_WARN_COND(type != storm::logic::ShieldingType::Optimal , "Comparison for optimal shield will be ignored."); return std::shared_ptr(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); } else { - STORM_LOG_THROW(type == storm::logic::ShieldingType::Optimal , storm::exceptions::WrongFormatException, "Construction of safety shield needs a comparison parameter (lambda or gamma)"); + STORM_LOG_INFO("Construction of shield without a comparison parameter (lambda or gamma) will default to 'lambda=0'"); return std::shared_ptr(new storm::logic::ShieldExpression(type, name)); } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 9f0953577..972f19028 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -237,7 +237,7 @@ namespace storm { // Shielding properties qi::rule(), Skipper> shieldExpression; qi::rule shieldingType; - qi::rule probability; + qi::rule comparisonValue; qi::rule, qi::locals, Skipper> shieldComparison; // Start symbol diff --git a/src/storm/logic/ShieldExpression.cpp b/src/storm/logic/ShieldExpression.cpp index a9cbeb088..74a86e79f 100644 --- a/src/storm/logic/ShieldExpression.cpp +++ b/src/storm/logic/ShieldExpression.cpp @@ -26,8 +26,12 @@ namespace storm { return type == storm::logic::ShieldingType::PostSafety; } - bool ShieldExpression::isOptimalShield() const { - return type == storm::logic::ShieldingType::Optimal; + bool ShieldExpression::isOptimalPreShield() const { + return type == storm::logic::ShieldingType::OptimalPre; + } + + bool ShieldExpression::isOptimalPostShield() const { + return type == storm::logic::ShieldingType::OptimalPost; } double ShieldExpression::getValue() const { @@ -36,9 +40,10 @@ namespace storm { std::string ShieldExpression::typeToString() const { switch(type) { - case storm::logic::ShieldingType::PostSafety: return "PostSafety"; - case storm::logic::ShieldingType::PreSafety: return "PreSafety"; - case storm::logic::ShieldingType::Optimal: return "Optimal"; + case storm::logic::ShieldingType::PostSafety: return "Post"; + case storm::logic::ShieldingType::PreSafety: return "Pre"; + case storm::logic::ShieldingType::OptimalPre: return "OptimalPre"; + case storm::logic::ShieldingType::OptimalPost: return "OptimalPost"; } } @@ -57,14 +62,13 @@ namespace storm { std::string prettyString = ""; std::string comparisonType = isRelative() ? "relative" : "absolute"; switch(type) { - case storm::logic::ShieldingType::PostSafety: prettyString += "Post-Safety"; break; - case storm::logic::ShieldingType::PreSafety: prettyString += "Pre-Safety"; break; - case storm::logic::ShieldingType::Optimal: prettyString += "Optimal"; break; + case storm::logic::ShieldingType::PostSafety: prettyString += "Post-Safety"; break; + case storm::logic::ShieldingType::PreSafety: prettyString += "Pre-Safety"; break; + case storm::logic::ShieldingType::OptimalPre: prettyString += "Optimal-Pre"; break; + case storm::logic::ShieldingType::OptimalPost: prettyString += "Optimal-Post"; break; } prettyString += "-Shield "; - if(!(type == storm::logic::ShieldingType::Optimal)) { - prettyString += "with " + comparisonType + " comparison (" + comparisonToString() + " = " + std::to_string(value) + "):"; - } + prettyString += "with " + comparisonType + " comparison (" + comparisonToString() + " = " + std::to_string(value) + "):"; return prettyString; } diff --git a/src/storm/logic/ShieldExpression.h b/src/storm/logic/ShieldExpression.h index b214f3baa..f13575591 100644 --- a/src/storm/logic/ShieldExpression.h +++ b/src/storm/logic/ShieldExpression.h @@ -9,7 +9,8 @@ namespace storm { enum class ShieldingType { PostSafety, PreSafety, - Optimal + OptimalPre, + OptimalPost }; enum class ShieldComparison { Absolute, Relative }; @@ -23,7 +24,8 @@ namespace storm { bool isRelative() const; bool isPreSafetyShield() const; bool isPostSafetyShield() const; - bool isOptimalShield() const; + bool isOptimalPreShield() const; + bool isOptimalPostShield() const; double getValue() const; @@ -36,8 +38,8 @@ namespace storm { private: ShieldingType type; - ShieldComparison comparison; - double value; + ShieldComparison comparison = ShieldComparison::Relative; + double value = 0; std::string filename; }; diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index d93da4407..b479efe71 100644 --- a/src/storm/shields/AbstractShield.h +++ b/src/storm/shields/AbstractShield.h @@ -21,9 +21,13 @@ namespace tempest { namespace utility { template struct ChoiceFilter { - bool operator()(ValueType v, ValueType max, double shieldValue) { + bool operator()(ValueType v, ValueType opt, double shieldValue) { Compare compare; - if(relative) return compare(v, max * shieldValue); + if(relative && std::is_same>::value) { + return compare(v, opt + opt * shieldValue); + } else if(relative && std::is_same>::value) { + return compare(v, opt * shieldValue); + } else return compare(v, shieldValue); } }; diff --git a/src/storm/shields/OptimalShield.cpp b/src/storm/shields/OptimalShield.cpp index 0bd26908d..8be4b1fef 100644 --- a/src/storm/shields/OptimalShield.cpp +++ b/src/storm/shields/OptimalShield.cpp @@ -6,27 +6,65 @@ namespace tempest { namespace shields { template - OptimalShield::OptimalShield(std::vector const& rowGroupIndices, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), precomputedChoices(precomputedChoices) { + OptimalShield::OptimalShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), choiceValues(choiceValues) { // Intentionally left empty. } template - storm::storage::OptimalScheduler OptimalShield::construct() { - storm::storage::OptimalScheduler shield(this->rowGroupIndices.size() - 1); - // TODO Needs fixing as soon as we support MDPs + storm::storage::PostScheduler OptimalShield::construct() { + if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { + if(this->shieldingExpression->isRelative()) { + return constructWithCompareType, true>(); + } else { + return constructWithCompareType, false>(); + } + } else { + if(this->shieldingExpression->isRelative()) { + return constructWithCompareType, true>(); + } else { + return constructWithCompareType, false>(); + } + } + } + + template + template + storm::storage::PostScheduler OptimalShield::constructWithCompareType() { + tempest::shields::utility::ChoiceFilter choiceFilter; + storm::storage::PostScheduler shield(this->rowGroupIndices.size() - 1, this->computeRowGroupSizes()); + auto choice_it = this->choiceValues.begin(); if(this->coalitionStates.is_initialized()) { - this->relevantStates = ~this->relevantStates; + this->relevantStates &= this->coalitionStates.get(); } for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; if(this->relevantStates.get(state)) { - shield.setChoice(precomputedChoices[state], state); + auto maxProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it; + ValueType maxProbability = *(choice_it + maxProbabilityIndex); + if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { + STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); + shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); + choice_it += rowGroupSize; + continue; + } + storm::storage::PostSchedulerChoice choiceMapping; + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { + choiceMapping.addChoice(choice, choice); + } else { + choiceMapping.addChoice(choice, maxProbabilityIndex); + } + } + shield.setChoice(choiceMapping, state, 0); } else { - shield.setChoice(storm::storage::Distribution(), state); + shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); + choice_it += rowGroupSize; } } return shield; } - // Explicitly instantiate appropriate + + // Explicitly instantiate appropriate classes template class OptimalShield::index_type>; #ifdef STORM_HAVE_CARL template class OptimalShield::index_type>; diff --git a/src/storm/shields/OptimalShield.h b/src/storm/shields/OptimalShield.h index 03bff3542..b7c55712e 100644 --- a/src/storm/shields/OptimalShield.h +++ b/src/storm/shields/OptimalShield.h @@ -1,7 +1,7 @@ #pragma once #include "storm/shields/AbstractShield.h" -#include "storm/storage/OptimalScheduler.h" +#include "storm/storage/PostScheduler.h" namespace tempest { namespace shields { @@ -9,11 +9,13 @@ namespace tempest { template class OptimalShield : public AbstractShield { public: - OptimalShield(std::vector const& rowGroupIndices, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + OptimalShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); - storm::storage::OptimalScheduler construct(); + storm::storage::PostScheduler construct(); + template + storm::storage::PostScheduler constructWithCompareType(); private: - std::vector precomputedChoices; + std::vector choiceValues; }; } } diff --git a/src/storm/shields/PostSafetyShield.cpp b/src/storm/shields/PostShield.cpp similarity index 62% rename from src/storm/shields/PostSafetyShield.cpp rename to src/storm/shields/PostShield.cpp index 311da2832..5ef487ad0 100644 --- a/src/storm/shields/PostSafetyShield.cpp +++ b/src/storm/shields/PostShield.cpp @@ -1,4 +1,4 @@ -#include "storm/shields/PostSafetyShield.h" +#include "storm/shields/PostShield.h" #include @@ -6,12 +6,12 @@ namespace tempest { namespace shields { template - PostSafetyShield::PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), choiceValues(choiceValues) { + PostShield::PostShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), choiceValues(choiceValues) { // Intentionally left empty. } template - storm::storage::PostScheduler PostSafetyShield::construct() { + storm::storage::PostScheduler PostShield::construct() { if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { if(this->shieldingExpression->isRelative()) { return constructWithCompareType, true>(); @@ -29,19 +29,22 @@ namespace tempest { template template - storm::storage::PostScheduler PostSafetyShield::constructWithCompareType() { + storm::storage::PostScheduler PostShield::constructWithCompareType() { tempest::shields::utility::ChoiceFilter choiceFilter; storm::storage::PostScheduler shield(this->rowGroupIndices.size() - 1, this->computeRowGroupSizes()); auto choice_it = this->choiceValues.begin(); if(this->coalitionStates.is_initialized()) { - this->relevantStates &= this->coalitionStates.get(); + this->relevantStates &= ~this->coalitionStates.get(); } for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; if(this->relevantStates.get(state)) { - auto maxProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it; - ValueType maxProbability = *(choice_it + maxProbabilityIndex); - if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { + auto optProbabilityIndex = std::min_element(choice_it, choice_it + rowGroupSize) - choice_it; + if(std::is_same>::value) { + optProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it; + } + ValueType optProbability = *(choice_it + optProbabilityIndex); + if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); shield.setChoice(storm::storage::PostSchedulerChoice(), state, 0); choice_it += rowGroupSize; @@ -49,10 +52,10 @@ namespace tempest { } storm::storage::PostSchedulerChoice choiceMapping; for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { + if(choiceFilter(*choice_it, optProbability, this->shieldingExpression->getValue())) { choiceMapping.addChoice(choice, choice); } else { - choiceMapping.addChoice(choice, maxProbabilityIndex); + choiceMapping.addChoice(choice, optProbabilityIndex); } } shield.setChoice(choiceMapping, state, 0); @@ -65,9 +68,9 @@ namespace tempest { } // Explicitly instantiate appropriate classes - template class PostSafetyShield::index_type>; + template class PostShield::index_type>; #ifdef STORM_HAVE_CARL - template class PostSafetyShield::index_type>; + template class PostShield::index_type>; #endif } } diff --git a/src/storm/shields/PostSafetyShield.h b/src/storm/shields/PostShield.h similarity index 53% rename from src/storm/shields/PostSafetyShield.h rename to src/storm/shields/PostShield.h index 6f04e53c3..f2a43905f 100644 --- a/src/storm/shields/PostSafetyShield.h +++ b/src/storm/shields/PostShield.h @@ -7,9 +7,9 @@ namespace tempest { namespace shields { template - class PostSafetyShield : public AbstractShield { + class PostShield : public AbstractShield { public: - PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + PostShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); storm::storage::PostScheduler construct(); template diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreShield.cpp similarity index 62% rename from src/storm/shields/PreSafetyShield.cpp rename to src/storm/shields/PreShield.cpp index f4374b929..a16b777c7 100644 --- a/src/storm/shields/PreSafetyShield.cpp +++ b/src/storm/shields/PreShield.cpp @@ -1,4 +1,4 @@ -#include "storm/shields/PreSafetyShield.h" +#include "storm/shields/PreShield.h" #include @@ -6,12 +6,12 @@ namespace tempest { namespace shields { template - PreSafetyShield::PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), choiceValues(choiceValues) { + PreShield::PreShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), choiceValues(choiceValues) { // Intentionally left empty. } template - storm::storage::PreScheduler PreSafetyShield::construct() { + storm::storage::PreScheduler PreShield::construct() { if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { if(this->shieldingExpression->isRelative()) { return constructWithCompareType, true>(); @@ -29,26 +29,31 @@ namespace tempest { template template - storm::storage::PreScheduler PreSafetyShield::constructWithCompareType() { + storm::storage::PreScheduler PreShield::constructWithCompareType() { tempest::shields::utility::ChoiceFilter choiceFilter; storm::storage::PreScheduler shield(this->rowGroupIndices.size() - 1); auto choice_it = this->choiceValues.begin(); if(this->coalitionStates.is_initialized()) { - this->relevantStates &= this->coalitionStates.get(); + this->relevantStates &= ~this->coalitionStates.get(); } for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; if(this->relevantStates.get(state)) { storm::storage::PreSchedulerChoice enabledChoices; - ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize); - if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { + ValueType optProbability; + if(std::is_same>::value) { + optProbability = *std::max_element(choice_it, choice_it + rowGroupSize); + } else { + optProbability = *std::min_element(choice_it, choice_it + rowGroupSize); + } + if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); shield.setChoice(storm::storage::PreSchedulerChoice(), state, 0); choice_it += rowGroupSize; continue; } for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { + if(choiceFilter(*choice_it, optProbability, this->shieldingExpression->getValue())) { enabledChoices.addChoice(choice, *choice_it); } } @@ -63,9 +68,9 @@ namespace tempest { return shield; } // Explicitly instantiate appropriate classes - template class PreSafetyShield::index_type>; + template class PreShield::index_type>; #ifdef STORM_HAVE_CARL - template class PreSafetyShield::index_type>; + template class PreShield::index_type>; #endif } } diff --git a/src/storm/shields/PreSafetyShield.h b/src/storm/shields/PreShield.h similarity index 53% rename from src/storm/shields/PreSafetyShield.h rename to src/storm/shields/PreShield.h index 8a4667bf2..6e98dd7e8 100644 --- a/src/storm/shields/PreSafetyShield.h +++ b/src/storm/shields/PreShield.h @@ -7,9 +7,9 @@ namespace tempest { namespace shields { template - class PreSafetyShield : public AbstractShield { + class PreShield : public AbstractShield { public: - PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + PreShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); storm::storage::PreScheduler construct(); template diff --git a/src/storm/shields/ShieldHandling.cpp b/src/storm/shields/ShieldHandling.cpp index 69240f6f1..007959d5d 100644 --- a/src/storm/shields/ShieldHandling.cpp +++ b/src/storm/shields/ShieldHandling.cpp @@ -10,11 +10,12 @@ namespace tempest { void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { std::ofstream stream; storm::utility::openFile(shieldFilename(shieldingExpression), stream); + if(coalitionStates.is_initialized()) coalitionStates.get().complement(); if(shieldingExpression->isPreSafetyShield()) { - PreSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + PreShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); shield.construct().printToStream(stream, shieldingExpression, model); } else if(shieldingExpression->isPostSafetyShield()) { - PostSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + PostShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); shield.construct().printToStream(stream, shieldingExpression, model); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString()); @@ -24,11 +25,15 @@ namespace tempest { } template - void createQuantitativeShield(std::shared_ptr> model, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { + void createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { std::ofstream stream; storm::utility::openFile(shieldFilename(shieldingExpression), stream); - if(shieldingExpression->isOptimalShield()) { - OptimalShield shield(model->getTransitionMatrix().getRowGroupIndices(), precomputedChoices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + if(coalitionStates.is_initialized()) coalitionStates.get().complement(); // TODO CHECK THIS!!! + if(shieldingExpression->isOptimalPreShield()) { + PreShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + shield.construct().printToStream(stream, shieldingExpression, model); + } else if(shieldingExpression->isOptimalPostShield()) { + PostShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); shield.construct().printToStream(stream, shieldingExpression, model); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString()); @@ -38,10 +43,10 @@ namespace tempest { } // Explicitly instantiate appropriate template void createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); - template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); #ifdef STORM_HAVE_CARL template void createShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); - template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + template void createQuantitativeShield::index_type>(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); #endif } } diff --git a/src/storm/shields/ShieldHandling.h b/src/storm/shields/ShieldHandling.h index 2b21a8522..768888a7d 100644 --- a/src/storm/shields/ShieldHandling.h +++ b/src/storm/shields/ShieldHandling.h @@ -10,8 +10,8 @@ #include "storm/logic/ShieldExpression.h" #include "storm/shields/AbstractShield.h" -#include "storm/shields/PreSafetyShield.h" -#include "storm/shields/PostSafetyShield.h" +#include "storm/shields/PreShield.h" +#include "storm/shields/PostShield.h" #include "storm/shields/OptimalShield.h" #include "storm/io/file.h" @@ -27,6 +27,6 @@ namespace tempest { void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); template - void createQuantitativeShield(std::shared_ptr> model, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + void createQuantitativeShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); } } diff --git a/src/test/storm/parser/GameShieldingParserTest.cpp b/src/test/storm/parser/GameShieldingParserTest.cpp index 53ae456a7..6279efc42 100644 --- a/src/test/storm/parser/GameShieldingParserTest.cpp +++ b/src/test/storm/parser/GameShieldingParserTest.cpp @@ -20,15 +20,15 @@ TEST(GameShieldingParserTest, PreSafetyShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); - EXPECT_TRUE(shieldExpression->isPreSafetyShield()); - EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_TRUE(shieldExpression->isPreShield()); + EXPECT_FALSE(shieldExpression->isPostShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); EXPECT_EQ(filename, shieldExpression->getFilename()); } -TEST(GameShieldingParserTest, PostSafetyShieldTest) { +TEST(GameShieldingParserTest, PostShieldTest) { storm::parser::FormulaParser formulaParser; std::string filename = "postSafetyShieldFileName"; @@ -46,7 +46,7 @@ TEST(GameShieldingParserTest, PostSafetyShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_TRUE(shieldExpression->isPostSafetyShield()); + EXPECT_TRUE(shieldExpression->isPostShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); @@ -74,8 +74,8 @@ TEST(GameShieldingParserTest, OptimalShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(filename, shieldExpression->getFilename()); -} \ No newline at end of file +} diff --git a/src/test/storm/parser/MdpShieldingParserTest.cpp b/src/test/storm/parser/MdpShieldingParserTest.cpp index 2baf68f30..85ffe9883 100644 --- a/src/test/storm/parser/MdpShieldingParserTest.cpp +++ b/src/test/storm/parser/MdpShieldingParserTest.cpp @@ -18,19 +18,19 @@ TEST(MdpShieldingParserTest, PreSafetyShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_TRUE(shieldExpression->isPreSafetyShield()); - EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); EXPECT_EQ(filename, shieldExpression->getFilename()); } -TEST(MdpShieldingParserTest, PostSafetyShieldTest) { +TEST(MdpShieldingParserTest, PostShieldTest) { storm::parser::FormulaParser formulaParser; std::string filename = "postSafetyShieldFileName"; std::string value = "0.95"; - std::string input = "<" + filename + ", PostSafety, lambda=" + value + "> Pmin=? [X !\"label\"]"; + std::string input = "<" + filename + ", Post, lambda=" + value + "> Pmin=? [X !\"label\"]"; std::shared_ptr formula(nullptr); std::vector property; @@ -40,7 +40,7 @@ TEST(MdpShieldingParserTest, PostSafetyShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_TRUE(shieldExpression->isPostSafetyShield()); + EXPECT_TRUE(shieldExpression->isPostShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); @@ -65,8 +65,8 @@ TEST(MdpShieldingParserTest, OptimalShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(filename, shieldExpression->getFilename()); -} \ No newline at end of file +} From a88aae44d33ecdd5b5e565f2c06f8f07c905e0f1 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 10:41:49 +0100 Subject: [PATCH 08/13] fixed some shield construction calls --- .../prctl/SparseMdpPrctlModelChecker.cpp | 5 ++++- .../rpatl/SparseSmgRpatlModelChecker.cpp | 12 ++++++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index a48995526..2b61631ae 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -298,7 +298,10 @@ namespace storm { auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); - if (checkTask.isProduceSchedulersSet()) { + if(checkTask.isShieldingTask()) { + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, allStatesBv); + } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } return result; diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index f44a7cef7..ca7271aa9 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -144,7 +144,8 @@ namespace storm { 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()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } @@ -160,7 +161,8 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } @@ -194,7 +196,8 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); } return result; } @@ -235,7 +238,8 @@ namespace storm { std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if(checkTask.isShieldingTask()) { - tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getProducedOptimalChoices(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), statesOfCoalition, statesOfCoalition); + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition); } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } From 4fbd2dd4133625b00c7ba7b0ec315c9c8e94496a Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 10:42:04 +0100 Subject: [PATCH 09/13] SMG LRA can now be used for Optimal Shields --- ...deterministicGameInfiniteHorizonHelper.cpp | 21 ++++++++++-- ...ondeterministicGameInfiniteHorizonHelper.h | 5 +++ ...eNondeterministicInfiniteHorizonHelper.cpp | 2 +- .../infinitehorizon/internal/LraViHelper.cpp | 32 +++++++++++++------ 4 files changed, 47 insertions(+), 13 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp index d9e2681a6..0149834ba 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -52,6 +52,12 @@ namespace storm { return scheduler; } + template + std::vector SparseNondeterministicGameInfiniteHorizonHelper::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 SparseNondeterministicGameInfiniteHorizonHelper::createDecomposition() { @@ -65,8 +71,6 @@ namespace storm { this->_computedLongRunComponentDecomposition = std::make_unique>(this->_transitionMatrix, *this->_backwardTransitions); this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get(); - //STORM_LOG_DEBUG("\n" << this->_transitionMatrix); - STORM_LOG_DEBUG("GMEC: " << *(this->_longRunComponentDecomposition)); } } @@ -91,6 +95,13 @@ namespace storm { } this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); } + // Allocate memory for the choice values. + if (this->isProduceChoiceValuesSet()) { + if (!this->_choiceValues.is_initialized()) { + this->_choiceValues.emplace(); + } + this->_choiceValues->resize(this->_transitionMatrix.getRowCount()); + } storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod(); if (method == storm::solver::LraMethod::LinearProgramming) { @@ -111,13 +122,17 @@ 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()) { STORM_LOG_THROW(false, storm::exceptions::InternalException, "We cannot handle continuous time games."); } else { storm::modelchecker::helper::internal::LraViHelper viHelper(mec, this->_transitionMatrix, aperiodicFactor, nullptr, nullptr, &statesOfCoalition); - return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices); + return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices, choiceValues); } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h index e6aa54752..9388fce4e 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h @@ -58,6 +58,11 @@ namespace storm { */ storm::storage::Scheduler extractScheduler() const; + /*! + * @return the computed choice values for the states. + */ + std::vector getChoiceValues() const; + ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component); ValueType computeLraVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec); diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp index 907d76ecb..d84422398 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp @@ -89,7 +89,7 @@ namespace storm { this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); } // Allocate memory for the choice values. - if (this->isProduceSchedulerSet()) { + if (this->isProduceChoiceValuesSet()) { if (!this->_choiceValues.is_initialized()) { this->_choiceValues.emplace(); } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 83181ca37..8ec234e64 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -214,7 +214,7 @@ namespace storm { STORM_LOG_TRACE("LRA computation converged after " << iter << " iterations."); } - if (choices) { + if (choices || choiceValues) { // We will be doing one more iteration step and track scheduler choices this time. if(!gameNondetTs()) { prepareNextIteration(env); @@ -222,8 +222,11 @@ namespace storm { performIterationStep(env, dir, choices, choiceValues); } if(gameNondetTs()) { - storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); - result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ? + storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); + result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ? + if(choiceValues) { + storm::utility::vector::applyPointwise(*choiceValues, *choiceValues, [this, &iter] (ValueType const& c_i) -> ValueType { return (c_i * _uniformizationRate) / (double)iter; }); + } } return result; } @@ -360,13 +363,16 @@ namespace storm { template void LraViHelper::setInputModelChoiceValues(std::vector& choiceValues, std::vector const& localMecChoiceValues) const { // Transform the local choiceValues (within this mec) to choice values for the input model + uint64_t localState = 0; + uint64_t choiceValuesOffset = 0; for (auto const& element : _component) { uint64_t elementState = element.first; uint64_t rowIndex = _transitionMatrix.getRowGroupIndices()[elementState]; uint64_t rowGroupSize = _transitionMatrix.getRowGroupEntryCount(elementState); - std::copy(localMecChoiceValues.begin(), localMecChoiceValues.begin() + rowGroupSize, &choiceValues.at(rowIndex)); + std::copy(localMecChoiceValues.begin() + choiceValuesOffset, localMecChoiceValues.begin() + choiceValuesOffset + rowGroupSize, &choiceValues.at(rowIndex)); localState++; + choiceValuesOffset += rowGroupSize; } } @@ -386,7 +392,7 @@ namespace storm { // Compute the values obtained by a single uniformization step between timed states only if (nondetTs() && !gameNondetTs()) { - if (choices == nullptr) { + if (choices == nullptr && choiceValues == nullptr) { _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew()); } else { // Also keep track of the choices made. @@ -401,8 +407,12 @@ namespace storm { // Note that nondeterminism within the timed states means that there can not be instant states (We either have MDPs or MAs) // Hence, in this branch we don't have to care for choices at instant states. STORM_LOG_ASSERT(!_hasInstantStates, "Nondeterministic timed states are only supported if there are no instant states."); - setInputModelChoices(*choices, tsChoices); - setInputModelChoiceValues(*choiceValues, resultChoiceValues); + if(choices != nullptr) { + setInputModelChoices(*choices, tsChoices); + } + if(choiceValues != nullptr) { + setInputModelChoiceValues(*choiceValues, resultChoiceValues); + } } } else if(gameNondetTs()) { // TODO DRYness? exact same behaviour as case above? if (choices == nullptr) { @@ -417,8 +427,12 @@ namespace storm { rowGroupIndices.erase(rowGroupIndices.begin()); _TsMultiplier->reduce(env, *dir, rowGroupIndices, resultChoiceValues, xNew(), &tsChoices); - setInputModelChoices(*choices, tsChoices); // no components -> no need for that call? - setInputModelChoiceValues(*choiceValues, resultChoiceValues); + if(choices != nullptr) { + setInputModelChoices(*choices, tsChoices); // no components -> no need for that call? + } + if(choiceValues != nullptr) { + setInputModelChoiceValues(*choiceValues, resultChoiceValues); + } } } else { _TsMultiplier->multiply(env, xOld(), &_TsChoiceValues, xNew()); From 449d5b31b91b031dafb1fff371096c8b02382fd3 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 10:42:29 +0100 Subject: [PATCH 10/13] changed some output for shield creation --- src/storm-cli-utilities/model-handling.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index f0ec400fe..e41bdf47f 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -838,7 +838,7 @@ namespace storm { void printModelCheckingProperty(storm::jani::Property const& property) { if(property.isShieldingProperty()) { - STORM_PRINT(std::endl << "Creating a " << property.getShieldingExpression()->typeToString() << " shield for:"); + STORM_PRINT(std::endl << "Creating " << property.getShieldingExpression()->typeToString() << " shield for:"); } STORM_PRINT(std::endl << "Model checking property \"" << property.getName() << "\": " << *property.getRawFormula() << " ..." << std::endl); } From 2c22a1e90a4f03ba3b9f409a7e705f0084ada6d9 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 12:09:27 +0100 Subject: [PATCH 11/13] fixed some issues with testing --- src/storm/logic/ShieldExpression.cpp | 4 ++++ src/storm/logic/ShieldExpression.h | 1 + src/test/storm/parser/GameShieldingParserTest.cpp | 9 ++++----- src/test/storm/parser/MdpShieldingParserTest.cpp | 9 ++++----- 4 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/storm/logic/ShieldExpression.cpp b/src/storm/logic/ShieldExpression.cpp index 74a86e79f..841d1a400 100644 --- a/src/storm/logic/ShieldExpression.cpp +++ b/src/storm/logic/ShieldExpression.cpp @@ -26,6 +26,10 @@ namespace storm { return type == storm::logic::ShieldingType::PostSafety; } + bool ShieldExpression::isOptimalShield() const { + return type == storm::logic::ShieldingType::OptimalPre || type == storm::logic::ShieldingType::OptimalPost; + } + bool ShieldExpression::isOptimalPreShield() const { return type == storm::logic::ShieldingType::OptimalPre; } diff --git a/src/storm/logic/ShieldExpression.h b/src/storm/logic/ShieldExpression.h index f13575591..808ebddf9 100644 --- a/src/storm/logic/ShieldExpression.h +++ b/src/storm/logic/ShieldExpression.h @@ -24,6 +24,7 @@ namespace storm { bool isRelative() const; bool isPreSafetyShield() const; bool isPostSafetyShield() const; + bool isOptimalShield() const; bool isOptimalPreShield() const; bool isOptimalPostShield() const; diff --git a/src/test/storm/parser/GameShieldingParserTest.cpp b/src/test/storm/parser/GameShieldingParserTest.cpp index 6279efc42..a6ed3cb88 100644 --- a/src/test/storm/parser/GameShieldingParserTest.cpp +++ b/src/test/storm/parser/GameShieldingParserTest.cpp @@ -20,8 +20,8 @@ TEST(GameShieldingParserTest, PreSafetyShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); - EXPECT_TRUE(shieldExpression->isPreShield()); - EXPECT_FALSE(shieldExpression->isPostShield()); + EXPECT_TRUE(shieldExpression->isPreSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); @@ -46,7 +46,7 @@ TEST(GameShieldingParserTest, PostShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_TRUE(shieldExpression->isPostShield()); + EXPECT_TRUE(shieldExpression->isPostSafetyShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); @@ -74,8 +74,7 @@ TEST(GameShieldingParserTest, OptimalShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_FALSE(shieldExpression->isPostShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); - EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(filename, shieldExpression->getFilename()); } diff --git a/src/test/storm/parser/MdpShieldingParserTest.cpp b/src/test/storm/parser/MdpShieldingParserTest.cpp index 85ffe9883..84b69d6db 100644 --- a/src/test/storm/parser/MdpShieldingParserTest.cpp +++ b/src/test/storm/parser/MdpShieldingParserTest.cpp @@ -18,7 +18,7 @@ TEST(MdpShieldingParserTest, PreSafetyShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_TRUE(shieldExpression->isPreSafetyShield()); - EXPECT_FALSE(shieldExpression->isPostShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); @@ -30,7 +30,7 @@ TEST(MdpShieldingParserTest, PostShieldTest) { std::string filename = "postSafetyShieldFileName"; std::string value = "0.95"; - std::string input = "<" + filename + ", Post, lambda=" + value + "> Pmin=? [X !\"label\"]"; + std::string input = "<" + filename + ", PostSafety, lambda=" + value + "> Pmin=? [X !\"label\"]"; std::shared_ptr formula(nullptr); std::vector property; @@ -40,7 +40,7 @@ TEST(MdpShieldingParserTest, PostShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_TRUE(shieldExpression->isPostShield()); + EXPECT_TRUE(shieldExpression->isPostSafetyShield()); EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); @@ -65,8 +65,7 @@ TEST(MdpShieldingParserTest, OptimalShieldTest) { std::shared_ptr shieldExpression(nullptr); ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); EXPECT_FALSE(shieldExpression->isPreSafetyShield()); - EXPECT_FALSE(shieldExpression->isPostShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); - EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(filename, shieldExpression->getFilename()); } From d4ae043601c6a80cc009e62db846106627030c28 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 12:09:41 +0100 Subject: [PATCH 12/13] adapted shield testing output to new changes --- .../mdp-shields/dieSelectionPostSafetylambda07Pmin.shield | 8 ++++---- .../mdp-shields/dieSelectionPreSafetygamma08Pmin.shield | 2 ++ .../mdp-shields/dieSelectionPreSafetylambda08Pmin.shield | 7 +++++++ 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield index 5cbf8cc99..89cc541ed 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield @@ -1,8 +1,8 @@ ___________________________________________________________________ Post-Safety-Shield with relative comparison (lambda = 0.700000): model state: correction [: ()}: - 0 0: 2; 1: 2; 2: 2 - 1 0: 0; 1: 0; 2: 0 - 3 0: 2; 1: 2; 2: 2 - 4 0: 2; 1: 2; 2: 2 + 0 0: 0; 1: 1; 2: 2 + 1 0: 0; 1: 1; 2: 2 + 3 0: 0; 1: 1; 2: 2 + 4 0: 0; 1: 1; 2: 2 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield index 6b32fa01a..000eb1c42 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield @@ -2,5 +2,7 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.800000): model state: choice(s) [: ()}: 0 0.58: (0); 0.566: (1); 0.552: (2) + 1 0.7942: (1); 0.7599: (2) 3 0.755: (0); 0.706: (1); 0.657: (2) + 6 0.79: (1); 0.755: (2) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield index dcd83f02c..b4ed673b8 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield @@ -1,4 +1,11 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.800000): model state: choice(s) [: ()}: + 0 0.58: (0); 0.566: (1); 0.552: (2) + 1 0.8285: (0); 0.7942: (1); 0.7599: (2) + 2 0.8775: (0); 0.902: (1); 0.9265: (2) + 3 0.755: (0); 0.706: (1); 0.657: (2) + 4 1: (0); 1: (1); 1: (2) + 5 1: (0); 1: (1); 1: (2) + 6 0.825: (0); 0.79: (1); 0.755: (2) ___________________________________________________________________ From 50cf8d8e7f3399d5575e9b303deef45a0c59d00a Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 13:40:55 +0100 Subject: [PATCH 13/13] updated smg shield tests --- .../rightDecisionPostSafetyGamma05PminF5.shield | 3 +-- .../rightDecisionPostSafetyGamma09PminF3.shield | 6 ++++-- .../rightDecisionPostSafetyLambda05PminF5.shield | 9 +++++---- .../rightDecisionPostSafetyLambda09PminF3.shield | 9 +++++---- .../rightDecisionPreSafetyGamma05PminF5.shield | 3 +-- .../rightDecisionPreSafetyGamma09PminF3.shield | 6 ++++-- .../rightDecisionPreSafetyLambda05PminF5.shield | 9 +++++---- .../rightDecisionPreSafetyLambda09PminF3.shield | 9 +++++---- .../ShieldGenerationSmgRpatlModelCheckerTest.cpp | 16 ++++++++-------- 9 files changed, 38 insertions(+), 32 deletions(-) diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield index c5e6ddce1..7e07d7004 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield @@ -1,6 +1,5 @@ ___________________________________________________________________ Post-Safety-Shield with absolute comparison (gamma = 0.500000): model state: correction [: ()}: - 4 0: 0 - 5 0: 0 + 7 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield index dbdb1771a..f5c8bef12 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield @@ -1,6 +1,8 @@ ___________________________________________________________________ Post-Safety-Shield with absolute comparison (gamma = 0.900000): model state: correction [: ()}: - 4 0: 0 - 5 0: 0 + 1 0: 0; 1: 0 + 2 0: 0 + 7 0: 0 + 10 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield index 6385fca02..4cfcbf587 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Post-Safety-Shield with relative comparison (lambda = 0.500000): model state: correction [: ()}: - 0 0: 0; 1: 1 - 4 0: 0 - 5 0: 0 - 9 0: 0; 1: 1 + 1 0: 0; 1: 1 + 2 0: 0 + 7 0: 0 + 8 0: 0 + 10 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield index 24a913b11..2431c28d3 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Post-Safety-Shield with relative comparison (lambda = 0.900000): model state: correction [: ()}: - 0 0: 0; 1: 1 - 4 0: 0 - 5 0: 0 - 9 0: 0; 1: 1 + 1 0: 0; 1: 1 + 2 0: 0 + 7 0: 0 + 8 0: 0 + 10 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield index 854110128..54eba5a4f 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield @@ -1,6 +1,5 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.500000): model state: choice(s) [: ()}: - 4 0: (0) - 5 0: (0) + 7 0: (0) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield index 5afcb6598..b2ef15a42 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield @@ -1,6 +1,8 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.900000): model state: choice(s) [: ()}: - 4 0: (0) - 5 0: (0) + 1 0.9: (0) + 2 0: (0) + 7 0: (0) + 10 0.9: (0) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield index 363275926..b841e7bbe 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.500000): model state: choice(s) [: ()}: - 0 0: (1) - 4 0: (0) - 5 0: (0) - 9 0: (1) + 1 0.9: (0); 1: (1) + 2 1: (0) + 7 0: (0) + 8 1: (0) + 10 0.9: (0) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield index eb3d29cd3..56a2a010c 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.900000): model state: choice(s) [: ()}: - 0 0: (1) - 4 0: (0) - 5 0: (0) - 9 0: (1) + 1 0.9: (0); 1: (1) + 2 0: (0) + 7 0: (0) + 8 1: (0) + 10 0.9: (0) ___________________________________________________________________ diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index b0f26f02b..096766c29 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -108,22 +108,22 @@ namespace { // testing create shielding expressions std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[2] + ", PreSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[6] + ", PostSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[8] + ", PreSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; formulasString += "; <" + fileNames[10] + ", PreSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; formulasString += "; <" + fileNames[12] + ", PostSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; formulasString += "; <" + fileNames[14] + ", PostSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); auto smg = std::move(modelFormulas.first);