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

possibly skip undefined choices in schedulers

main
Stefan Pranger 4 years ago
parent
c78981dc1a
commit
dc430a3213
3 changed files with 131 additions and 113 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. 92
      src/storm/storage/PostScheduler.cpp
  2. 146
      src/storm/storage/Scheduler.cpp
  3. 6
      src/storm/storage/Scheduler.h

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

@ -100,62 +100,66 @@ namespace storm {
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));
std::stringstream stateString;
// Print the state info
if (stateValuationsGiven) {
stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state));
} else {
stateString << std::setw(widthOfStates) << state;
}
stateString << " ";
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;
stateString << std::to_string(choiceIndex) << ": ";
} else {
out << std::setw(widthOfStates) << state;
stateString << std::setw(widthOfStates + 5) << std::to_string(choiceIndex) << ": ";
}
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) << ": ";
if (choice.isDefined()) {
if (choice.isDeterministic()) {
if (choiceOriginsGiven) {
stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
} else {
stateString << choice.getDeterministicChoice();
}
if (choiceLabelsGiven) {
auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
stateString << " {" << boost::join(choiceLabels, ", ") << "}";
}
} else {
out << std::setw(widthOfStates + 5) << std::to_string(choiceIndex) << ": ";
}
if (choice.isDefined()) {
if (choice.isDeterministic()) {
bool firstChoice = true;
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
if (firstChoice) {
firstChoice = false;
} else {
stateString << " + ";
}
stateString << choiceProbPair.second << ": (";
if (choiceOriginsGiven) {
out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first);
} else {
out << choice.getDeterministicChoice();
stateString << choiceProbPair.first;
}
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 << ")";
stateString << " {" << boost::join(choiceLabels, ", ") << "}";
}
stateString << ")";
}
} else {
out << "undefined.";
}
// Todo: print memory updates
out << std::endl;
} else {
if(!this->printUndefinedChoices) goto skipStatesWithUndefinedChoices;
stateString << "undefined.";
}
// Todo: print memory updates
stateString << std::endl;
}
out << stateString.str();
// jump to label if we find one undefined choice.
skipStatesWithUndefinedChoices:;
}
}

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

@ -8,7 +8,7 @@
namespace storm {
namespace storage {
template <typename ValueType>
Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure) : memoryStructure(memoryStructure) {
uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1;
@ -16,7 +16,7 @@ namespace storm {
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates;
numOfDeterministicChoices = 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;
@ -24,7 +24,7 @@ namespace storm {
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates;
numOfDeterministicChoices = 0;
}
template <typename ValueType>
void Scheduler<ValueType>::setChoice(SchedulerChoice<ValueType> const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) {
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
@ -50,7 +50,7 @@ namespace storm {
++numOfDeterministicChoices;
}
}
schedulerChoice = choice;
}
@ -71,7 +71,7 @@ namespace storm {
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
setChoice(SchedulerChoice<ValueType>(), modelState, memoryState);
}
template <typename ValueType>
SchedulerChoice<ValueType> const& Scheduler<ValueType>::getChoice(uint_fast64_t modelState, uint_fast64_t memoryState) const {
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
@ -96,17 +96,17 @@ namespace storm {
}
return result;
}
template <typename ValueType>
bool Scheduler<ValueType>::isPartialScheduler() const {
return numOfUndefinedChoices != 0;
}
template <typename ValueType>
bool Scheduler<ValueType>::isDeterministicScheduler() const {
return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices;
}
template <typename ValueType>
bool Scheduler<ValueType>::isMemorylessScheduler() const {
return getNumberOfMemoryStates() == 1;
@ -125,7 +125,7 @@ namespace storm {
template <typename ValueType>
void Scheduler<ValueType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
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();
bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling();
bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins();
@ -135,7 +135,7 @@ namespace storm {
}
widthOfStates = std::max(widthOfStates, (uint_fast64_t)12);
uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0;
out << "___________________________________________________________________" << std::endl;
out << (isPartialScheduler() ? "Partially" : "Fully") << " defined ";
out << (isMemorylessScheduler() ? "memoryless " : "");
@ -146,76 +146,79 @@ namespace storm {
out << ":" << std::endl;
STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given.");
out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl;
for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) {
// Check whether the state is skipped
if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) {
++numOfSkippedStatesWithUniqueChoice;
continue;
}
// Print the state info
if (stateValuationsGiven) {
out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state));
for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) {
std::stringstream stateString;
// Check whether the state is skipped
if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) {
++numOfSkippedStatesWithUniqueChoice;
continue;
}
// Print the state info
if (stateValuationsGiven) {
stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state));
} else {
stateString << std::setw(widthOfStates) << state;
}
stateString << " ";
bool firstMemoryState = true;
for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
// Indent if this is not the first memory state
if (firstMemoryState) {
firstMemoryState = false;
} else {
out << std::setw(widthOfStates) << state;
stateString << std::setw(widthOfStates) << "";
stateString << " ";
}
out << " ";
bool firstMemoryState = true;
for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
// Indent if this is not the first memory state
if (firstMemoryState) {
firstMemoryState = false;
// Print the memory state info
if (!isMemorylessScheduler()) {
stateString << "m" << std::setw(8) << memoryState;
}
// Print choice info
SchedulerChoice<ValueType> const& choice = schedulerChoices[memoryState][state];
if (choice.isDefined()) {
if (choice.isDeterministic()) {
if (choiceOriginsGiven) {
stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
} else {
stateString << choice.getDeterministicChoice();
}
if (choiceLabelsGiven) {
auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
stateString << " {" << boost::join(choiceLabels, ", ") << "}";
}
} else {
out << std::setw(widthOfStates) << "";
out << " ";
}
// Print the memory state info
if (!isMemorylessScheduler()) {
out << "m" << std::setw(8) << memoryState;
}
// Print choice info
SchedulerChoice<ValueType> const& choice = schedulerChoices[memoryState][state];
if (choice.isDefined()) {
if (choice.isDeterministic()) {
bool firstChoice = true;
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
if (firstChoice) {
firstChoice = false;
} else {
stateString << " + ";
}
stateString << choiceProbPair.second << ": (";
if (choiceOriginsGiven) {
out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first);
} else {
out << choice.getDeterministicChoice();
stateString << choiceProbPair.first;
}
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 << ")";
stateString << " {" << boost::join(choiceLabels, ", ") << "}";
}
stateString << ")";
}
} else {
out << "undefined.";
}
// Todo: print memory updates
out << std::endl;
} else {
if(!printUndefinedChoices) continue;
stateString << "undefined.";
}
// Todo: print memory updates
out << stateString.str();
out << std::endl;
}
}
if (numOfSkippedStatesWithUniqueChoice > 0) {
out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl;
@ -271,10 +274,15 @@ namespace storm {
out << output.dump(4);
}
template <typename ValueType>
void Scheduler<ValueType>::setPrintUndefinedChoices(bool value) {
printUndefinedChoices = value;
}
template class Scheduler<double>;
template class Scheduler<float>;
template class Scheduler<storm::RationalNumber>;
template class Scheduler<storm::RationalFunction>;
}
}

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

@ -1,6 +1,8 @@
#pragma once
#include <cstdint>
#include <sstream>
#include "storm/storage/memorystructure/MemoryStructure.h"
#include "storm/storage/SchedulerChoice.h"
@ -117,10 +119,14 @@ namespace storm {
*/
void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
void setPrintUndefinedChoices(bool value = true);
private:
boost::optional<storm::storage::MemoryStructure> memoryStructure;
std::vector<std::vector<SchedulerChoice<ValueType>>> schedulerChoices;
bool printUndefinedChoices = false;
protected:
uint_fast64_t numOfUndefinedChoices;
uint_fast64_t numOfDeterministicChoices;

Write Preview
Loading…
Cancel
Save