diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index efcad6579..b932df8f0 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -1048,7 +1048,7 @@ namespace storm { auto shield = result->template asExplicitQuantitativeCheckResult().getShield(); STORM_PRINT_AND_LOG("Exporting shield ..."); - storm::api::exportShield(sparseModel, shield); + storm::api::exportShield(sparseModel, shield, shield->getShieldFileName()); } } diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index 26c2e1c63..8ca8d9117 100644 --- a/src/storm/shields/AbstractShield.h +++ b/src/storm/shields/AbstractShield.h @@ -52,6 +52,8 @@ namespace tempest { std::string getShieldFileName() const; virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) = 0; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) = 0; + protected: AbstractShield(std::vector const& rowGroupIndices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); diff --git a/src/storm/shields/OptimalShield.cpp b/src/storm/shields/OptimalShield.cpp index d1b5daadb..ff12e1c12 100644 --- a/src/storm/shields/OptimalShield.cpp +++ b/src/storm/shields/OptimalShield.cpp @@ -69,6 +69,11 @@ namespace tempest { this->construct().printToStream(out, this->shieldingExpression, model); } + template + void OptimalShield::printJsonToStream(std::ostream& out, std::shared_ptr> const& model) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "not supported yet"); + } + // Explicitly instantiate appropriate classes template class OptimalShield::index_type>; #ifdef STORM_HAVE_CARL diff --git a/src/storm/shields/OptimalShield.h b/src/storm/shields/OptimalShield.h index bae16d8af..0dac50587 100644 --- a/src/storm/shields/OptimalShield.h +++ b/src/storm/shields/OptimalShield.h @@ -15,6 +15,7 @@ namespace tempest { template storm::storage::PostScheduler constructWithCompareType(); virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) override; private: std::vector choiceValues; diff --git a/src/storm/shields/PostShield.cpp b/src/storm/shields/PostShield.cpp index 150ea94f6..b9165b45e 100644 --- a/src/storm/shields/PostShield.cpp +++ b/src/storm/shields/PostShield.cpp @@ -73,6 +73,11 @@ namespace tempest { this->construct().printToStream(out, this->shieldingExpression, model); } + template + void PostShield::printJsonToStream(std::ostream& out, std::shared_ptr> const& model) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "not supported yet"); + } + // Explicitly instantiate appropriate classes template class PostShield::index_type>; diff --git a/src/storm/shields/PostShield.h b/src/storm/shields/PostShield.h index 85a325f93..b857a9216 100644 --- a/src/storm/shields/PostShield.h +++ b/src/storm/shields/PostShield.h @@ -16,6 +16,7 @@ namespace tempest { storm::storage::PostScheduler constructWithCompareType(); virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) override; private: std::vector choiceValues; diff --git a/src/storm/shields/PreShield.cpp b/src/storm/shields/PreShield.cpp index a4437f3f3..716d4f8d1 100644 --- a/src/storm/shields/PreShield.cpp +++ b/src/storm/shields/PreShield.cpp @@ -74,6 +74,11 @@ namespace tempest { this->construct().printToStream(out, this->shieldingExpression, model); } + template + void PreShield::printJsonToStream(std::ostream& out, std::shared_ptr> const& model) { + this->construct().printJsonToStream(out, model); + } + // Explicitly instantiate appropriate classes template class PreShield::index_type>; diff --git a/src/storm/shields/PreShield.h b/src/storm/shields/PreShield.h index cdaee54f3..1b5f099b8 100644 --- a/src/storm/shields/PreShield.h +++ b/src/storm/shields/PreShield.h @@ -16,6 +16,7 @@ namespace tempest { storm::storage::PreScheduler constructWithCompareType(); virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) override; private: std::vector choiceValues; diff --git a/src/storm/storage/PreScheduler.cpp b/src/storm/storage/PreScheduler.cpp index d78400731..92069070b 100644 --- a/src/storm/storage/PreScheduler.cpp +++ b/src/storm/storage/PreScheduler.cpp @@ -137,6 +137,84 @@ namespace storm { out << "___________________________________________________________________" << std::endl; } + + + + template + void PreScheduler::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); + } + + + + template class PreScheduler; #ifdef STORM_HAVE_CARL template class PreScheduler; diff --git a/src/storm/storage/PreScheduler.h b/src/storm/storage/PreScheduler.h index 6277c5051..e695e0732 100644 --- a/src/storm/storage/PreScheduler.h +++ b/src/storm/storage/PreScheduler.h @@ -40,10 +40,16 @@ namespace storm { PreSchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; /*! - * Prints the scheduler to the given output stream. + * Prints the pre scheduler to the given output stream. */ void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + /*! + * Prints the pre scheduler in json format to the given output stream. + */ + void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + + private: boost::optional memoryStructure; std::vector>> schedulerChoices;