From 71100e9d653c24bbb419f21e4eebb22990b7ccd6 Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Tue, 27 Jul 2021 20:42:38 +0200
Subject: [PATCH] scheduler json export
Conflicts:
src/storm/storage/Scheduler.cpp
---
.../helper/ltl/SparseLTLHelper.cpp | 7 +-
.../modelchecker/helper/ltl/SparseLTLHelper.h | 4 +-
src/storm/storage/Scheduler.cpp | 102 +++++++++++-------
3 files changed, 70 insertions(+), 43 deletions(-)
diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
index b315aa2c0..527cb3868 100644
--- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
+++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
@@ -45,7 +45,7 @@ namespace storm {
STORM_LOG_ASSERT(this->_producedChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?");
STORM_LOG_ASSERT(this->_memoryTransitions.is_initialized(), "Trying to extract the DA transition structure but none is available. Was there a computation call before?");
STORM_LOG_ASSERT(this->_memoryInitialStates.is_initialized(), "Trying to extract the initial states of the DA but there are none available. Was there a computation call before?");
- STORM_LOG_ASSERT(this->_dontCareStates.is_initialized(), "Trying to extract the dontCare states of the Scheduler but there are none available. Was there a computation call before?");
+ STORM_LOG_ASSERT(this->_dontCareStates.is_initialized(), "Trying to extract the Scheduler-dontCare states but there are none available. Was there a computation call before?");
// Create a memory structure for the MDP scheduler with memory. If hasRelevantStates is set, we only consider initial model states relevant.
@@ -147,7 +147,7 @@ namespace storm {
}
for (auto const& conjunction : dnf) {
- // determine the set of states of the subMDP that can satisfy the condition, remove all states that would violate Fins in the conjunction
+ // Determine the set of states of the subMDP that can satisfy the condition, remove all states that would violate Fins in the conjunction.
storm::storage::BitVector allowed(transitionMatrix.getRowGroupCount(), true);
STORM_LOG_INFO("Handle conjunction " << i);
@@ -182,7 +182,7 @@ namespace storm {
STORM_LOG_DEBUG(" Allowed states: " << allowed);
- // compute MECs in the allowed fragment
+ // Compute MECs in the allowed fragment
storm::storage::MaximalEndComponentDecomposition<ValueType> mecs(transitionMatrix, backwardTransitions, allowed);
allMECs += mecs.size();
for (const auto& mec : mecs) {
@@ -387,7 +387,6 @@ namespace storm {
}
}
-
}
}
}
diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
index 8b85a07de..3d7c21abe 100644
--- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
+++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
@@ -25,8 +25,8 @@ namespace storm {
public:
/*!
- * The type of the product automaton (DTMC or MDP) that is used during the computation.
- */
+ * The type of the product automaton (DTMC or MDP) that is used during the computation.
+ */
using productModelType = typename std::conditional<Nondeterministic, storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Dtmc<ValueType>>::type;
/*!
diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp
index 51a3f40e8..268fb3b0b 100644
--- a/src/storm/storage/Scheduler.cpp
+++ b/src/storm/storage/Scheduler.cpp
@@ -248,7 +248,7 @@ namespace storm {
// Print memory updates
if(!isMemorylessScheduler()) {
- out << std::setw(8);
+ out << std::setw(widthOfStates) << "";
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
bool firstUpdate = true;
@@ -258,10 +258,9 @@ namespace storm {
} else {
stateString << ", ";
}
- 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 << "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()) <<")";
+ }
stateString << std::endl;
}
@@ -275,11 +274,6 @@ namespace storm {
}
out << "___________________________________________________________________" << std::endl;
- // TODO only for tests:
- if(!isMemorylessScheduler()) {
- out << memoryStructure->toString();
- out << std::endl;
- }
}
template <>
@@ -289,44 +283,78 @@ namespace storm {
template <typename ValueType>
void Scheduler<ValueType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
- //TODO not defined for memory and unreachable states are not considered
STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler.");
STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given.");
- STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers with memory not implemented.");
storm::json<storm::RationalNumber> output;
for (uint64_t state = 0; state < schedulerChoices.front().size(); ++state) {
// Check whether the state is skipped
if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) {
continue;
}
- storm::json<storm::RationalNumber> stateChoicesJson;
- if (model && model->hasStateValuations()) {
- stateChoicesJson["s"] = model->getStateValuations().template toJson<storm::RationalNumber>(state);
- } else {
- stateChoicesJson["s"] = state;
- }
- auto const& choice = schedulerChoices.front()[state];
- storm::json<storm::RationalNumber> choicesJson;
- if (choice.isDefined()) {
- for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
- uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
- storm::json<storm::RationalNumber> choiceJson;
- if (model && model->hasChoiceOrigins() && model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) {
- choiceJson["origin"] = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex);
- }
- if (model && model->hasChoiceLabeling()) {
- auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex);
- choiceJson["labels"] = std::vector<std::string>(choiceLabels.begin(), choiceLabels.end());
+
+ for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
+ // Ignore dontCare states
+ if ((!isMemorylessScheduler()) && isDontCare(state, memoryState)) {
+ continue;
+ }
+
+ storm::json<storm::RationalNumber> stateChoicesJson;
+ if (model && model->hasStateValuations()) {
+ stateChoicesJson["s"] = model->getStateValuations().template toJson<storm::RationalNumber>(state);
+ } else {
+ stateChoicesJson["s"] = state;
+ }
+
+ if (!isMemorylessScheduler()) {
+ stateChoicesJson["m"] = memoryState;
+ }
+
+ auto const &choice = schedulerChoices[memoryState][state];
+ storm::json<storm::RationalNumber> choicesJson;
+ if (choice.isDefined()) {
+ for (auto const &choiceProbPair : choice.getChoiceAsDistribution()) {
+ uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
+ storm::json<storm::RationalNumber> choiceJson;
+ if (model && model->hasChoiceOrigins() &&
+ model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) !=
+ model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) {
+ choiceJson["origin"] = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex);
+ }
+ if (model && model->hasChoiceLabeling()) {
+ auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex);
+ choiceJson["labels"] = std::vector<std::string>(choiceLabels.begin(),
+ choiceLabels.end());
+ }
+ choiceJson["index"] = globalChoiceIndex;
+ choiceJson["prob"] = storm::utility::convertNumber<storm::RationalNumber>(
+ choiceProbPair.second);
+
+ // Memory updates
+ if(!isMemorylessScheduler()) {
+ choiceJson["memory-updates"] = std::vector<storm::json<storm::RationalNumber>>();
+ uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
+ for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) {
+ storm::json<storm::RationalNumber> updateJson;
+ // next model state
+ if (model && model->hasStateValuations()) {
+ updateJson["s'"] = model->getStateValuations().template toJson<storm::RationalNumber>(entryIt->getColumn());
+ } else {
+ updateJson["s'"] = entryIt->getColumn();
+ }
+ // next memory state
+ updateJson["m'"] = this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin());
+ choiceJson["memory-updates"].push_back(std::move(updateJson));
+ }
+ }
+
+ choicesJson.push_back(std::move(choiceJson));
}
- choiceJson["index"] = globalChoiceIndex;
- choiceJson["prob"] = storm::utility::convertNumber<storm::RationalNumber>(choiceProbPair.second);
- choicesJson.push_back(std::move(choiceJson));
+ } else {
+ choicesJson = "undefined";
}
- } else {
- choicesJson = "undefined";
+ stateChoicesJson["c"] = std::move(choicesJson);
+ output.push_back(std::move(stateChoicesJson));
}
- stateChoicesJson["c"] = std::move(choicesJson);
- output.push_back(std::move(stateChoicesJson));
}
out << output.dump(4);
}