From de2243b09543efc01bb7f5dff1c390ef986c5b25 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Fri, 11 Aug 2023 09:00:47 +0200 Subject: [PATCH] addded post scheduler json export removed workaround in pre scheduler json --- src/storm/storage/PostScheduler.cpp | 124 +++++++++++++--------------- src/storm/storage/PreScheduler.cpp | 78 ++++++++--------- 2 files changed, 96 insertions(+), 106 deletions(-) diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 35873ea31..420b4b4e7 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/src/storm/storage/PostScheduler.cpp @@ -130,74 +130,62 @@ namespace storm { template void PostScheduler::printJsonToStream(std::ostream& out, std::shared_ptr> 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."); - // STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); - // storm::json 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; - // } - - // for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { - // storm::json stateChoicesJson; - // if (model && model->hasStateValuations()) { - // stateChoicesJson["s"] = model->getStateValuations().template toJson(state); - // } else { - // stateChoicesJson["s"] = state; - // } - - // if (!isMemorylessScheduler()) { - // stateChoicesJson["m"] = memoryState; - // } - - // auto const &choice = schedulerChoices[memoryState][state]; - // storm::json choicesJson; - - // for (auto const &choiceProbPair : choice.getChoiceMap()) { - // uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] ;//+ choiceProbPair.first; - // storm::json 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(choiceLabels.begin(), - // choiceLabels.end()); - // } - // choiceJson["index"] = globalChoiceIndex; - // choiceJson["prob"] = storm::utility::convertNumber( - // std::get<1>(choiceProbPair)); - - // // Memory updates - // if(!isMemorylessScheduler()) { - // choiceJson["memory-updates"] = std::vector>(); - // uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state]; //+ std::get<0>(choiceProbPair); - // for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { - // storm::json updateJson; - // // next model state - // if (model && model->hasStateValuations()) { - // updateJson["s'"] = model->getStateValuations().template toJson(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)); - // } - // if (!choicesJson.is_null()) { - // stateChoicesJson["c"] = std::move(choicesJson); - // output.push_back(std::move(stateChoicesJson)); - // } - // } - // } - // out << output.dump(4); + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoiceMapping.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::json output; + for (uint64_t state = 0; state < schedulerChoiceMapping.front().size(); ++state) { + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + continue; + } + + storm::json stateChoicesJson; + if (model && model->hasStateValuations()) { + stateChoicesJson["s"] = model->getStateValuations().template toJson(state); + } else { + stateChoicesJson["s"] = state; + } + + auto const &choice = schedulerChoiceMapping[0][state]; + storm::json choicesJson; + if (!choice.getChoiceMap().empty()) { + for (auto const &choiceProbPair : choice.getChoiceMap()) { + uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<0>(choiceProbPair); + uint64_t globalChoiceCorrectionIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get<1>(choiceProbPair); + storm::json choiceJson; + if (model && model->hasChoiceOrigins() && + model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != + model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) { + auto choiceOriginJson = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex); + auto choiceOriginCorrectionJson = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceCorrectionIndex); + std::string choiceActionLabel = choiceOriginJson["action-label"]; + std::string choiceCorrectionActionLabel = choiceOriginCorrectionJson["action-label"]; + choiceOriginJson["action-label"] = choiceActionLabel.append(": ").append(choiceCorrectionActionLabel); + choiceJson["origin"] = choiceOriginJson; + } + if (model && model->hasChoiceLabeling()) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex); + + choiceJson["labels"] = std::vector(choiceLabels.begin(), + choiceLabels.end()); + } + choiceJson["index"] = globalChoiceIndex; + choiceJson["prob"] = storm::utility::convertNumber( + std::get<1>(choiceProbPair)); + + + choicesJson.push_back(std::move(choiceJson)); + } + } else { + choicesJson = "undefined"; + } + + stateChoicesJson["c"] = std::move(choicesJson); + output.push_back(std::move(stateChoicesJson)); + + } + + out << output.dump(4); } diff --git a/src/storm/storage/PreScheduler.cpp b/src/storm/storage/PreScheduler.cpp index 373b8986e..bc3e6e833 100644 --- a/src/storm/storage/PreScheduler.cpp +++ b/src/storm/storage/PreScheduler.cpp @@ -165,48 +165,50 @@ namespace storm { auto const &choice = schedulerChoices[memoryState][state]; storm::json choicesJson; - - for (auto const &choiceProbPair : choice.getChoiceMap()) { - uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get(choiceProbPair); - storm::json 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(choiceLabels.begin(), - choiceLabels.end()); - } - choiceJson["index"] = globalChoiceIndex; - choiceJson["prob"] = storm::utility::convertNumber( - std::get(choiceProbPair)); - - // Memory updates - if(!isMemorylessScheduler()) { - choiceJson["memory-updates"] = std::vector>(); - uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get(choiceProbPair); - for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { - storm::json updateJson; - // next model state - if (model && model->hasStateValuations()) { - updateJson["s'"] = model->getStateValuations().template toJson(entryIt->getColumn()); - } else { - updateJson["s'"] = entryIt->getColumn(); + if (!choice.getChoiceMap().empty()) { + for (auto const &choiceProbPair : choice.getChoiceMap()) { + uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get(choiceProbPair); + storm::json 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(choiceLabels.begin(), + choiceLabels.end()); + } + choiceJson["index"] = globalChoiceIndex; + choiceJson["prob"] = storm::utility::convertNumber( + std::get(choiceProbPair)); + + // Memory updates + if(!isMemorylessScheduler()) { + choiceJson["memory-updates"] = std::vector>(); + uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + std::get(choiceProbPair); + for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { + storm::json updateJson; + // next model state + if (model && model->hasStateValuations()) { + updateJson["s'"] = model->getStateValuations().template toJson(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)); } - // 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)); - } - if (!choicesJson.is_null()) { - stateChoicesJson["c"] = std::move(choicesJson); - output.push_back(std::move(stateChoicesJson)); + choicesJson.push_back(std::move(choiceJson)); + } + } else { + choicesJson = "undefined"; } + + stateChoicesJson["c"] = std::move(choicesJson); + output.push_back(std::move(stateChoicesJson)); } } out << output.dump(4);