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

introduced PostScheduler 

this allows for different choice mappings per state, in the sense of
'what should I schedule if another scheduler has already picked a
different action'
main
Stefan Pranger 5 years ago
parent
4b2e7e020f
commit
5562007866
3 changed files with 283 additions and 16 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 167
      src/storm/storage/PostScheduler.cpp
  2. 100
      src/storm/storage/PostScheduler.h
  3. 32
      src/storm/storage/Scheduler.h

167
src/storm/storage/PostScheduler.cpp
View File

@ -0,0 +1,167 @@
#include "storm/utility/vector.h"
#include "storm/storage/PostScheduler.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
#include <boost/algorithm/string/join.hpp>
namespace storm {
namespace storage {
template <typename ValueType>
PostScheduler<ValueType>::PostScheduler(uint_fast64_t numberOfModelStates, std::vector<uint_fast64_t> numberOfChoicesPerState, boost::optional<storm::storage::MemoryStructure> const& memoryStructure) : Scheduler<ValueType>(numberOfModelStates, memoryStructure) {
STORM_LOG_DEBUG(numberOfChoicesPerState.size() << " " << numberOfModelStates);
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<std::vector<std::vector<SchedulerChoice<ValueType>>>>(numOfMemoryStates, std::vector<std::vector<SchedulerChoice<ValueType>>>(numberOfModelStates));
for(uint state = 0; state < numberOfModelStates; state++) {
schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]);
}
numberOfChoices = 0;
for(std::vector<uint_fast64_t>::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it)
numberOfChoices += *it;
this->numOfUndefinedChoices = numOfMemoryStates * numberOfChoices;
this->numOfDeterministicChoices = 0;
}
template <typename ValueType>
PostScheduler<ValueType>::PostScheduler(uint_fast64_t numberOfModelStates, std::vector<uint_fast64_t> numberOfChoicesPerState, boost::optional<storm::storage::MemoryStructure>&& memoryStructure) : Scheduler<ValueType>(numberOfModelStates, 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<std::vector<std::vector<SchedulerChoice<ValueType>>>>(numOfMemoryStates, std::vector<std::vector<SchedulerChoice<ValueType>>>(numberOfModelStates));
for(uint state = 0; state < numberOfModelStates; state++) {
schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]);
}
numberOfChoices = 0;
for(std::vector<uint_fast64_t>::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it)
numberOfChoices += *it;
this->numOfUndefinedChoices = numOfMemoryStates * numberOfChoices;
this->numOfDeterministicChoices = 0;
}
template <typename ValueType>
void PostScheduler<ValueType>::setChoice(OldChoice const& oldChoice, SchedulerChoice<ValueType> const& newChoice, 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");
//auto& schedulerChoice = schedulerChoiceMapping[memoryState][modelState];
//if (schedulerChoice.isDefined()) {
// if (!choice.isDefined()) {
// ++numOfUndefinedChoices;
// }
//} else {
// if (choice.isDefined()) {
// assert(numOfUndefinedChoices > 0);
// --numOfUndefinedChoices;
// }
//}
//if (schedulerChoice.isDeterministic()) {
// if (!choice.isDeterministic()) {
// assert(numOfDeterministicChoices > 0);
// --numOfDeterministicChoices;
// }
//} else {
// if (choice.isDeterministic()) {
// ++numOfDeterministicChoices;
// }
//}
schedulerChoiceMapping[memoryState][modelState][oldChoice] = newChoice;
}
template <typename ValueType>
SchedulerChoice<ValueType> const& PostScheduler<ValueType>::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];
}
template <typename ValueType>
bool PostScheduler<ValueType>::isDeterministicScheduler() const {
return true;
}
template <typename ValueType>
bool PostScheduler<ValueType>::isMemorylessScheduler() const {
return true;
}
template <typename ValueType>
void PostScheduler<ValueType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
bool const stateValuationsGiven = model != nullptr && model->hasStateValuations();
bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling();
bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins();
uint_fast64_t widthOfStates = std::to_string(schedulerChoiceMapping.front().size()).length();
if (stateValuationsGiven) {
widthOfStates += model->getStateValuations().getStateInfo(schedulerChoiceMapping.front().size() - 1).length() + 5;
}
widthOfStates = std::max(widthOfStates, (uint_fast64_t)12);
uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0;
out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl;
for (uint_fast64_t state = 0; state < schedulerChoiceMapping.front().size(); ++state) {
// Print the state info
if (stateValuationsGiven) {
out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state));
} else {
out << std::setw(widthOfStates) << state;
}
out << " ";
bool firstChoiceIndex = true;
for(uint choiceIndex = 0; choiceIndex < schedulerChoiceMapping[0][state].size(); choiceIndex++) {
SchedulerChoice<ValueType> const& choice = schedulerChoiceMapping[0][state][choiceIndex];
if(firstChoiceIndex) {
firstChoiceIndex = false;
out << std::to_string(choiceIndex) << ": ";
} else {
out << std::setw(widthOfStates + 5) << std::to_string(choiceIndex) << ": ";
}
if (choice.isDefined()) {
if (choice.isDeterministic()) {
if (choiceOriginsGiven) {
out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
} else {
out << choice.getDeterministicChoice();
}
if (choiceLabelsGiven) {
auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
out << " {" << boost::join(choiceLabels, ", ") << "}";
}
} else {
bool firstChoice = true;
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
if (firstChoice) {
firstChoice = false;
} else {
out << " + ";
}
out << choiceProbPair.second << ": (";
if (choiceOriginsGiven) {
out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first);
} else {
out << choiceProbPair.first;
}
if (choiceLabelsGiven) {
auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
out << " {" << boost::join(choiceLabels, ", ") << "}";
}
out << ")";
}
}
} else {
out << "undefined.";
}
// Todo: print memory updates
out << std::endl;
}
}
}
template class PostScheduler<double>;
#ifdef STORM_HAVE_CARL
template class PostScheduler<storm::RationalNumber>;
#endif
}
}

100
src/storm/storage/PostScheduler.h
View File

@ -0,0 +1,100 @@
#pragma once
#include <cstdint>
#include <map>
#include "storm/storage/SchedulerChoice.h"
#include "storm/storage/Scheduler.h"
namespace storm {
namespace storage {
/*
* 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 <typename ValueType>
class PostScheduler : public Scheduler<ValueType> {
public:
typedef uint_fast64_t OldChoice;
/*!
* Initializes a scheduler for the given number of model states.
*
* @param numberOfModelStates number of model states
* @param memoryStructure the considered memory structure. If not given, the scheduler is considered as memoryless.
*/
PostScheduler(uint_fast64_t numberOfModelStates, std::vector<uint_fast64_t> numberOfChoicesPerState, boost::optional<storm::storage::MemoryStructure> const& memoryStructure = boost::none);
PostScheduler(uint_fast64_t numberOfModelStates, std::vector<uint_fast64_t> numberOfChoicesPerState, boost::optional<storm::storage::MemoryStructure>&& memoryStructure);
/*!
* Sets the choice defined by the scheduler for the given state.
*
* @param choice The choice to set for the given state.
* @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<ValueType> const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState = 0);
/*!
* Is the scheduler defined on the states indicated by the selected-states bitvector?
*/
bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const;
/*!
* Clears the choice defined by the scheduler for the given state.
*
* @param modelState The state of the model for which to clear the choice.
* @param memoryState The state of the memoryStructure for which to clear the choice.
*/
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<ValueType> 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
*/
//storm::storage::BitVector computeActionSupport(std::vector<uint64_t> const& nondeterministicChoiceIndicies) const;
/*!
* Retrieves whether all defined choices are deterministic
*/
bool isDeterministicScheduler() const;
/*!
* Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state)
*/
bool isMemorylessScheduler() const;
/*!
* Retrieves the number of memory states this scheduler considers.
*/
//uint_fast64_t getNumberOfMemoryStates() const;
/*!
* Retrieves the memory structure associated with this scheduler
*/
//boost::optional<storm::storage::MemoryStructure> const& getMemoryStructure() const;
/*!
* 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<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
private:
std::vector<std::vector<std::vector<SchedulerChoice<ValueType>>>> schedulerChoiceMapping;
std::vector<uint_fast64_t> numberOfChoicesPerState;
uint_fast64_t numberOfChoices;
};
}
}

32
src/storm/storage/Scheduler.h
View File

@ -5,10 +5,9 @@
#include "storm/storage/SchedulerChoice.h" #include "storm/storage/SchedulerChoice.h"
namespace storm { namespace storm {
namespace storage { namespace storage {
template <typename ValueType>
class PostScheduler;
/* /*
* 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 * 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). * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states).
@ -17,7 +16,8 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
class Scheduler { class Scheduler {
public: public:
friend class PostScheduler<ValueType>;
/*! /*!
* Initializes a scheduler for the given number of model states. * Initializes a scheduler for the given number of model states.
* *
@ -26,7 +26,7 @@ namespace storm {
*/ */
Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure = boost::none); Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure = boost::none);
Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure>&& memoryStructure); Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure>&& memoryStructure);
/*! /*!
* Sets the choice defined by the scheduler for the given state. * Sets the choice defined by the scheduler for the given state.
* *
@ -40,7 +40,7 @@ namespace storm {
* Is the scheduler defined on the states indicated by the selected-states bitvector? * Is the scheduler defined on the states indicated by the selected-states bitvector?
*/ */
bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const; bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const;
/*! /*!
* Clears the choice defined by the scheduler for the given state. * Clears the choice defined by the scheduler for the given state.
* *
@ -48,7 +48,7 @@ namespace storm {
* @param memoryState The state of the memoryStructure for which to clear the choice. * @param memoryState The state of the memoryStructure for which to clear the choice.
*/ */
void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0); 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. * Gets the choice defined by the scheduler for the given model and memory state.
* *
@ -66,22 +66,22 @@ namespace storm {
* Retrieves whether there is a pair of model and memory state for which the choice is undefined. * Retrieves whether there is a pair of model and memory state for which the choice is undefined.
*/ */
bool isPartialScheduler() const; bool isPartialScheduler() const;
/*! /*!
* Retrieves whether all defined choices are deterministic * Retrieves whether all defined choices are deterministic
*/ */
bool isDeterministicScheduler() const; bool isDeterministicScheduler() const;
/*! /*!
* Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state) * Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state)
*/ */
bool isMemorylessScheduler() const; bool isMemorylessScheduler() const;
/*! /*!
* Retrieves the number of memory states this scheduler considers. * Retrieves the number of memory states this scheduler considers.
*/ */
uint_fast64_t getNumberOfMemoryStates() const; uint_fast64_t getNumberOfMemoryStates() const;
/*! /*!
* Retrieves the memory structure associated with this scheduler * Retrieves the memory structure associated with this scheduler
*/ */
@ -101,7 +101,7 @@ namespace storm {
} }
return newScheduler; return newScheduler;
} }
/*! /*!
* Prints the scheduler to the given output stream. * Prints the scheduler to the given output stream.
* @param out The output stream * @param out The output stream
@ -111,19 +111,19 @@ namespace storm {
*/ */
void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const; void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
/*! /*!
* Prints the scheduler in json format to the given output stream. * Prints the scheduler in json format to the given output stream.
*/ */
void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const; void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
private: private:
boost::optional<storm::storage::MemoryStructure> memoryStructure; boost::optional<storm::storage::MemoryStructure> memoryStructure;
std::vector<std::vector<SchedulerChoice<ValueType>>> schedulerChoices; std::vector<std::vector<SchedulerChoice<ValueType>>> schedulerChoices;
protected:
uint_fast64_t numOfUndefinedChoices; uint_fast64_t numOfUndefinedChoices;
uint_fast64_t numOfDeterministicChoices; uint_fast64_t numOfDeterministicChoices;
}; };
} }
} }
Write Preview
Loading…
Cancel
Save