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

ignore dontCare States while printing 

TODO Scheduler printing will need refactoring

 Conflicts:
	src/storm/storage/Scheduler.cpp
	src/storm/storage/Scheduler.h
tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
77ced0aefe
commit
6b0aaeadb4
2 changed files with 20 additions and 47 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 48
      src/storm/storage/Scheduler.cpp
  2. 19
      src/storm/storage/Scheduler.h

48
src/storm/storage/Scheduler.cpp
View File

@ -13,20 +13,20 @@ namespace storm {
Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure) : memoryStructure(memoryStructure) {
uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1;
schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates));
reachableStates = std::vector<storm::storage::BitVector>(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true));
dontCareStates = std::vector<storm::storage::BitVector>(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, false));
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates;
numOfDeterministicChoices = 0;
numOfUnreachableStates = 0;
numOfDontCareStates = 0;
}
template <typename ValueType>
Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure>&& memoryStructure) : memoryStructure(std::move(memoryStructure)) {
uint_fast64_t numOfMemoryStates = this->memoryStructure ? this->memoryStructure->getNumberOfStates() : 1;
schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates));
reachableStates = std::vector<storm::storage::BitVector>(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true));
dontCareStates = std::vector<storm::storage::BitVector>(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, false));
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates;
numOfDeterministicChoices = 0;
numOfUnreachableStates = 0;
numOfDontCareStates = 0;
}
template <typename ValueType>
@ -35,7 +35,7 @@ namespace storm {
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
auto& schedulerChoice = schedulerChoices[memoryState][modelState];
if (reachableStates[memoryState].get(modelState)) {
if (!dontCareStates[memoryState].get(modelState)) {
if (schedulerChoice.isDefined()) {
if (!choice.isDefined()) {
++numOfUndefinedChoices;
@ -87,13 +87,13 @@ namespace storm {
}
template <typename ValueType>
void Scheduler<ValueType>::setStateUnreachable(uint_fast64_t modelState, uint_fast64_t memoryState) {
void Scheduler<ValueType>::setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState) {
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
auto& schedulerChoice = schedulerChoices[memoryState][modelState];
if (reachableStates[memoryState].get(modelState)) {
reachableStates[memoryState].set(modelState, false);
++numOfUnreachableStates;
if (!dontCareStates[memoryState].get(modelState)) {
dontCareStates[memoryState].set(modelState, true);
++numOfDontCareStates;
// Choices for unreachable states are not considered undefined or deterministic
if (!schedulerChoice.isDefined()) {
@ -106,27 +106,8 @@ namespace storm {
}
template <typename ValueType>
void Scheduler<ValueType>::setStateReachable(uint_fast64_t modelState, uint_fast64_t memoryState) {
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
auto& schedulerChoice = schedulerChoices[memoryState][modelState];
if (!reachableStates[memoryState].get(modelState)) {
reachableStates[memoryState].set(modelState, true);
--numOfUnreachableStates;
// Choices for unreachable states are not considered undefined or deterministic
if (!schedulerChoice.isDefined()) {
++numOfUndefinedChoices;
} else if (schedulerChoice.isDeterministic()) {
++numOfDeterministicChoices;
}
}
}
template <typename ValueType>
bool Scheduler<ValueType>::isStateReachable(uint_fast64_t modelState, uint64_t memoryState) const {
return reachableStates[memoryState].get(modelState);
bool Scheduler<ValueType>::isDontCare(uint_fast64_t modelState, uint64_t memoryState) const {
return dontCareStates[memoryState].get(modelState);
}
template<typename ValueType>
@ -154,7 +135,7 @@ namespace storm {
template <typename ValueType>
bool Scheduler<ValueType>::isDeterministicScheduler() const {
return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfUnreachableStates;
return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfDontCareStates;
}
template <typename ValueType>
@ -174,7 +155,6 @@ namespace storm {
template <typename ValueType>
void Scheduler<ValueType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
// TODO ignore unreachable states
STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler.");
bool const stateValuationsGiven = model != nullptr && model->hasStateValuations();
@ -267,9 +247,8 @@ namespace storm {
}
// Print memory updates
if(!isMemorylessScheduler()) {
stateString << std::setw(30); //todo set width
out << std::setw(8);
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
bool firstUpdate = true;
@ -282,7 +261,6 @@ namespace storm {
stateString << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
//out << ", model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = ?) ";
}
}
stateString << std::endl;

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

@ -61,25 +61,18 @@ namespace storm {
SchedulerChoice<ValueType> const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const;
/*!
* Set the combination of model state and memoryStructure state to unreachable.
* Set the combination of model state and memoryStructure state to dontCare.
* This means the corresponding choices are neither considered undefined nor deterministic.
*
* @param modelState The state of the model.
* @param memoryState The state of the memoryStructure.
*/
void setStateUnreachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
/*!
* Set the combination of model state and memoryStructure state to reachable.
*
* @param modelState The state of the model.
* @param memoryState The state of the memoryStructure.
*/
void setStateReachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
void setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
/*!
* Is the combination of model state and memoryStructure state to reachable?
*/
bool isStateReachable(uint_fast64_t modelState, uint64_t memoryState = 0) const;
bool isDontCare(uint_fast64_t modelState, uint64_t memoryState = 0) const;
/*!
* Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state
@ -152,8 +145,10 @@ namespace storm {
std::vector<storm::storage::BitVector> reachableStates;
uint_fast64_t numOfUndefinedChoices; // Only consider reachable ones
std::vector<storm::storage::BitVector> dontCareStates; // Their choices are neither considered deterministic nor undefined
uint_fast64_t numOfUndefinedChoices;
uint_fast64_t numOfDeterministicChoices;
uint_fast64_t numOfUnreachableStates;
uint_fast64_t numOfDontCareStates;
};
}
}
Write Preview
Loading…
Cancel
Save