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

fixed scheduler print after large merge

tempestpy_adaptions
Stefan Pranger 3 years ago
parent
4fd16ff45f
commit
7550934b2e
1 changed files with 21 additions and 60 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. 51
      src/storm/storage/Scheduler.cpp

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

@ -182,6 +182,7 @@ namespace storm {
if (!isMemorylessScheduler()) { if (!isMemorylessScheduler()) {
out << " with " << getNumberOfMemoryStates() << " memory states"; out << " with " << getNumberOfMemoryStates() << " memory states";
} }
out << ":" << std::endl; out << ":" << std::endl;
STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); 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)" << (isMemorylessScheduler() ? "" : " memory updates: ") << std::endl; out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << (isMemorylessScheduler() ? "" : " memory updates: ") << std::endl;
@ -203,22 +204,6 @@ namespace storm {
bool firstMemoryState = true; bool firstMemoryState = true;
for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
// Indent if this is not the first memory state
if (firstMemoryState) {
firstMemoryState = false;
} else {
stateString << std::setw(widthOfStates) << "";
stateString << " ";
}
// Print the memory state info
if (!isMemorylessScheduler()) {
stateString << "m" << std::setw(8) << memoryState;
}
stateString << " ";
bool firstMemoryState = true;
for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
// Ignore dontCare states // Ignore dontCare states
if(skipDontCareStates && isDontCare(state, memoryState)) { if(skipDontCareStates && isDontCare(state, memoryState)) {
continue; continue;
@ -228,13 +213,14 @@ namespace storm {
if (firstMemoryState) { if (firstMemoryState) {
firstMemoryState = false; firstMemoryState = false;
} else { } else {
out << std::setw(widthOfStates) << "";
out << " ";
stateString << std::setw(widthOfStates) << "";
stateString << " ";
} }
// Print the memory state info // Print the memory state info
if (!isMemorylessScheduler()) { if (!isMemorylessScheduler()) {
out << "m="<< memoryState << std::setw(8) << "";
stateString << "m" << std::setw(8) << memoryState;
} }
stateString << " ";
// Print choice info // Print choice info
SchedulerChoice<ValueType> const& choice = schedulerChoices[memoryState][state]; SchedulerChoice<ValueType> const& choice = schedulerChoices[memoryState][state];
@ -289,38 +275,13 @@ namespace storm {
stateString << ", "; stateString << ", ";
} }
stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
// out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
}
}
}
// Print memory updates
if(!isMemorylessScheduler()) {
out << std::setw(widthOfStates) << "";
// The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state.
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
bool firstUpdate = true;
for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) {
if (firstUpdate) {
firstUpdate = false;
} else {
out << ", ";
} }
out << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
// out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
} }
}
} }
out << stateString.str();
out << std::endl; out << std::endl;
} }
stateString << stateString.str();
stateString << std::endl;
}
} }
if (numOfSkippedStatesWithUniqueChoice > 0) { if (numOfSkippedStatesWithUniqueChoice > 0) {
out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl;

Write Preview
Loading…
Cancel
Save