added print to json for shields

added  filename to export shield

src/storm-cli-utilities/model-handling.h

@@ -1048,7 +1048,7 @@ namespace storm {
                                                     auto shield = result->template asExplicitQuantitativeCheckResult<ValueType>().getShield();
                                                     STORM_PRINT_AND_LOG("Exporting shield ...");
                                                     
-                                                    storm::api::exportShield(sparseModel, shield);
+                                                    storm::api::exportShield(sparseModel, shield, shield->getShieldFileName());
                                                 }
                                             }
 

src/storm/shields/AbstractShield.h

@@ -52,6 +52,8 @@ namespace tempest {
             std::string getShieldFileName() const;
 
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) = 0;
+            virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) = 0;
+
 
         protected:
             AbstractShield(std::vector<IndexType> const& rowGroupIndices, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);

src/storm/shields/OptimalShield.cpp

@@ -69,6 +69,11 @@ namespace tempest {
            this->construct().printToStream(out, this->shieldingExpression, model);
         }
 
+        template<typename ValueType, typename IndexType>
+        void OptimalShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "not supported yet");
+        }
+
         // Explicitly instantiate appropriate classes
         template class OptimalShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL

src/storm/shields/OptimalShield.h

@@ -15,6 +15,7 @@ namespace tempest {
             template<typename Compare, bool relative>
             storm::storage::PostScheduler<ValueType> constructWithCompareType();
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
+            virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
 
         private:
             std::vector<ValueType> choiceValues;

src/storm/shields/PostShield.cpp

@@ -73,6 +73,11 @@ namespace tempest {
            this->construct().printToStream(out, this->shieldingExpression, model);
         }
 
+        template<typename ValueType, typename IndexType>
+        void PostShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "not supported yet");
+        }
+
 
         // Explicitly instantiate appropriate classes
         template class PostShield<double, typename storm::storage::SparseMatrix<double>::index_type>;

src/storm/shields/PostShield.h

@@ -16,6 +16,7 @@ namespace tempest {
             storm::storage::PostScheduler<ValueType> constructWithCompareType();
 
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
+            virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
 
         private:
             std::vector<ValueType> choiceValues;

src/storm/shields/PreShield.cpp

@@ -74,6 +74,11 @@ namespace tempest {
            this->construct().printToStream(out, this->shieldingExpression, model);
         }
 
+        template<typename ValueType, typename IndexType>
+        void PreShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            this->construct().printJsonToStream(out, model);
+        }
+
 
         // Explicitly instantiate appropriate classes
         template class PreShield<double, typename storm::storage::SparseMatrix<double>::index_type>;

src/storm/shields/PreShield.h

@@ -16,6 +16,7 @@ namespace tempest {
             storm::storage::PreScheduler<ValueType> constructWithCompareType();
 
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
+            virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
 
         private:
             std::vector<ValueType> choiceValues;

src/storm/storage/PreScheduler.cpp

@@ -137,6 +137,84 @@ namespace storm {
             out << "___________________________________________________________________" << std::endl;
         }
 
+
+      
+
+        template <typename ValueType>
+        void PreScheduler<ValueType>::printJsonToStream(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.");
+            STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given.");
+            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;
+                }
+
+                for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
+                    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;
+
+                    for (auto const &choiceProbPair : choice.getChoiceMap()) {
+                        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>(
+                                std::get<1>(choiceProbPair));
+
+                        // Memory updates
+                        if(!isMemorylessScheduler()) {
+                            choiceJson["memory-updates"] = std::vector<storm::json<storm::RationalNumber>>();
+                            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<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));
+                    }
+                    if (!choicesJson.is_null()) {
+                        stateChoicesJson["c"] = std::move(choicesJson);
+                        output.push_back(std::move(stateChoicesJson));
+                    }
+                }
+            }
+            out << output.dump(4);
+        }
+
+
+
+
         template class PreScheduler<double>;
 #ifdef STORM_HAVE_CARL
         template class PreScheduler<storm::RationalNumber>;

src/storm/storage/PreScheduler.h

@@ -40,10 +40,16 @@ namespace storm {
             PreSchedulerChoice<ValueType> 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<storm::logic::ShieldExpression const> shieldingExpression, std::shared_ptr<storm::models::sparse::Model<ValueType>> 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<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
+
+
         private:
             boost::optional<storm::storage::MemoryStructure> memoryStructure;
             std::vector<std::vector<PreSchedulerChoice<ValueType>>> schedulerChoices;