Added an export of check results to json.

CHANGELOG.md

@@ -7,6 +7,8 @@ The releases of major and minor versions contain an overview of changes since th
 
 Version 1.6.x
 -------------
+## Version 1.6.4 (20xx/xx)
+- Added an export of  check results to json. Use `--exportresult` in the command line interface.
 
 ## Version 1.6.3 (2020/11)
 - Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives.

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

@@ -995,8 +995,7 @@ namespace storm {
         void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
             auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
             auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-            verifyProperties<ValueType>(input,
-                                        [&sparseModel,&ioSettings,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+            auto verificationCallback = [&sparseModel,&ioSettings,&mpi] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
                                             bool filterForInitialStates = states->isInitialFormula();
                                             auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
                                             if (ioSettings.isExportSchedulerSet()) {
@@ -1014,14 +1013,21 @@ namespace storm {
                                                 result->filter(filter->asQualitativeCheckResult());
                                             }
                                             return result;
-                                        },
-                                        [&sparseModel,&ioSettings] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
+                                        };
+            uint64_t exportCount = 0; // this number will be prepended to the export file name of schedulers and/or check results in case of multiple properties.
+            auto postprocessingCallback = [&sparseModel,&ioSettings,&input,&exportCount] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
                                             if (ioSettings.isExportSchedulerSet()) {
                                                 if (result->isExplicitQuantitativeCheckResult()) {
                                                     if (result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()) {
                                                         auto const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
                                                         STORM_PRINT_AND_LOG("Exporting scheduler ... ")
-                                                        storm::api::exportScheduler(sparseModel, scheduler, ioSettings.getExportSchedulerFilename());
+                                                        if (input.model) {
+                                                            STORM_LOG_WARN_COND(sparseModel->hasStateValuations(), "No information of state valuations available. The scheduler output will use internal state ids. You might be interested in building the model with state valuations using --buildstateval.");
+                                                            STORM_LOG_WARN_COND(sparseModel->hasChoiceLabeling() || sparseModel->hasChoiceOrigins(), "No symbolic choice information is available. The scheduler output will use internal choice ids. You might be interested in building the model with choice labels or choice origins using --buildchoicelab or --buildchoiceorig.");
+                                                            STORM_LOG_WARN_COND(sparseModel->hasChoiceLabeling() && !sparseModel->hasChoiceOrigins(), "Only partial choice information is available. You might want to build the model with choice origins using --buildchoicelab or --buildchoiceorig.");
+                                                        }
+                                                        STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties.");
+                                                        storm::api::exportScheduler(sparseModel, scheduler, (exportCount == 0 ? std::string("") : std::to_string(exportCount)) + ioSettings.getExportSchedulerFilename());
                                                     } else {
                                                         STORM_LOG_ERROR("Scheduler requested but could not be generated.");
                                                     }
@@ -1029,7 +1035,14 @@ namespace storm {
                                                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
                                                 }
                                             }
-                                        });
+                                            if (ioSettings.isExportCheckResultSet()) {
+                                                STORM_LOG_WARN_COND(sparseModel->hasStateValuations(), "No information of state valuations available. The result output will use internal state ids. You might be interested in building the model with state valuations using --buildstateval.");
+                                                STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties.");
+                                                storm::api::exportCheckResultToJson(sparseModel, result, (exportCount == 0 ? std::string("") : std::to_string(exportCount)) + ioSettings.getExportCheckResultFilename());
+                                            }
+                                            ++exportCount;
+                                        };
+            verifyProperties<ValueType>(input,verificationCallback, postprocessingCallback);
         }
         
         template <storm::dd::DdType DdType, typename ValueType>

src/storm/api/export.h

@@ -7,6 +7,10 @@
 #include "storm/io/file.h"
 #include "storm/utility/macros.h"
 #include "storm/storage/Scheduler.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/exceptions/NotSupportedException.h"
 
 namespace storm {
     
@@ -59,5 +63,23 @@ namespace storm {
             storm::utility::closeFile(stream);
         }
         
+        template <typename ValueType>
+        void exportCheckResultToJson(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult> const& checkResult, std::string const& filename) {
+            std::ofstream stream;
+            storm::utility::openFile(filename, stream);
+            if (checkResult->isExplicitQualitativeCheckResult()) {
+                stream << checkResult->asExplicitQualitativeCheckResult().toJson(model->getOptionalStateValuations()).dump(4);
+            } else {
+                STORM_LOG_THROW(checkResult->isExplicitQuantitativeCheckResult(), storm::exceptions::NotSupportedException, "Export of check results is only supported for explicit check results (e.g. in the sparse engine)");
+                stream << checkResult->template asExplicitQuantitativeCheckResult<ValueType>().toJson(model->getOptionalStateValuations()).dump(4);
+            }
+            storm::utility::closeFile(stream);
+        }
+        
+        template <>
+        void exportCheckResultToJson<storm::RationalFunction>(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const&, std::unique_ptr<storm::modelchecker::CheckResult> const&, std::string const&) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export of check results is not supported for rational functions. ");
+        }
+        
     }
 }

src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp

@@ -234,5 +234,39 @@ namespace storm {
                 this->truthValues = newMap;
             }
         }
+        
+        template<typename JsonRationalType>
+        void insertJsonEntry(storm::json<JsonRationalType>& json, uint64_t const& id, bool value, boost::optional<storm::storage::sparse::StateValuations> const& stateValuations = boost::none) {
+            storm::json<JsonRationalType> entry;
+            if (stateValuations) {
+                entry["s"] = stateValuations->template toJson<JsonRationalType>(id);
+            } else {
+                entry["s"] = id;
+            }
+            entry["v"] = value;
+            json.push_back(std::move(entry));
+        }
+        
+        template<typename JsonRationalType>
+        storm::json<JsonRationalType> ExplicitQualitativeCheckResult::toJson(boost::optional<storm::storage::sparse::StateValuations> const& stateValuations) const {
+            storm::json<JsonRationalType> result;
+            if (this->isResultForAllStates()) {
+                vector_type const& valuesAsVector = boost::get<vector_type>(truthValues);
+                for (uint64_t state = 0; state < valuesAsVector.size(); ++state) {
+                    insertJsonEntry(result, state, valuesAsVector.get(state), stateValuations);
+                }
+            } else {
+                map_type const& valuesAsMap = boost::get<map_type>(truthValues);
+                for (auto const& stateValue : valuesAsMap) {
+                    insertJsonEntry(result, stateValue.first, stateValue.second, stateValuations);
+                }
+            }
+            return result;
+        }
+        
+        template storm::json<double> ExplicitQualitativeCheckResult::toJson<double>(boost::optional<storm::storage::sparse::StateValuations> const&) const;
+        template storm::json<storm::RationalNumber> ExplicitQualitativeCheckResult::toJson<storm::RationalNumber>(boost::optional<storm::storage::sparse::StateValuations> const&) const;
+
+        
     }
 }

src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h

@@ -8,15 +8,19 @@
 #include "storm/modelchecker/results/QualitativeCheckResult.h"
 #include "storm/storage/sparse/StateType.h"
 #include "storm/storage/BitVector.h"
+#include "storm/storage/sparse/StateValuations.h"
+
 #include "storm/utility/OsDetection.h"
+#include "storm/adapters/JsonAdapter.h"
 
 namespace storm {
+    
     namespace modelchecker {
         class ExplicitQualitativeCheckResult : public QualitativeCheckResult {
         public:
             typedef storm::storage::BitVector vector_type;
             typedef std::map<storm::storage::sparse::state_type, bool> map_type;
-            
+
             ExplicitQualitativeCheckResult();
             virtual ~ExplicitQualitativeCheckResult() = default;
             ExplicitQualitativeCheckResult(map_type const& map);
@@ -60,6 +64,9 @@ namespace storm {
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             virtual void filter(QualitativeCheckResult const& filter) override;
+            
+            template<typename JsonRationalType = storm::RationalNumber>
+            storm::json<JsonRationalType> toJson(boost::optional<storm::storage::sparse::StateValuations> const& stateValuations = boost::none) const;
 
         private:
             static void performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, bool logicalAnd);

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -5,10 +5,10 @@
 #include "storm/utility/macros.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
+#include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/InvalidAccessException.h"
-#include "storm/adapters/RationalFunctionAdapter.h"
-
+#include "storm/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace modelchecker {
@@ -417,6 +417,40 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        void insertJsonEntry(storm::json<ValueType>& json, uint64_t const& id, ValueType const& value, boost::optional<storm::storage::sparse::StateValuations> const& stateValuations = boost::none) {
+            typename storm::json<ValueType> entry;
+            if (stateValuations) {
+                entry["s"] = stateValuations->template toJson<ValueType>(id);
+            } else {
+                entry["s"] = id;
+            }
+            entry["v"] = value;
+            json.push_back(std::move(entry));
+        }
+        
+        template<typename ValueType>
+        storm::json<ValueType> ExplicitQuantitativeCheckResult<ValueType>::toJson(boost::optional<storm::storage::sparse::StateValuations> const& stateValuations) const {
+            storm::json<ValueType> result;
+            if (this->isResultForAllStates()) {
+                vector_type const& valuesAsVector = boost::get<vector_type>(values);
+                for (uint64_t state = 0; state < valuesAsVector.size(); ++state) {
+                    insertJsonEntry(result, state, valuesAsVector[state], stateValuations);
+                }
+            } else {
+                map_type const& valuesAsMap = boost::get<map_type>(values);
+                for (auto const& stateValue : valuesAsMap) {
+                    insertJsonEntry(result, stateValue.first, stateValue.second, stateValuations);
+                }
+            }
+            return result;
+        }
+        
+        template<>
+        storm::json<storm::RationalFunction> ExplicitQuantitativeCheckResult<storm::RationalFunction>::toJson(boost::optional<storm::storage::sparse::StateValuations> const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export of Check results is not supported for Rational Functions.");
+        }
+        
         template class ExplicitQuantitativeCheckResult<double>;
 
 #ifdef STORM_HAVE_CARL

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h

@@ -9,7 +9,10 @@
 #include "storm/modelchecker/results/QuantitativeCheckResult.h"
 #include "storm/storage/sparse/StateType.h"
 #include "storm/storage/Scheduler.h"
+#include "storm/storage/sparse/StateValuations.h"
+
 #include "storm/utility/OsDetection.h"
+#include "storm/adapters/JsonAdapter.h"
 
 namespace storm {
     namespace modelchecker {
@@ -70,6 +73,8 @@ namespace storm {
             storm::storage::Scheduler<ValueType> const& getScheduler() const;
             storm::storage::Scheduler<ValueType>& getScheduler();
             
+            storm::json<ValueType> toJson(boost::optional<storm::storage::sparse::StateValuations> const& stateValuations = boost::none) const;
+            
         private:
             // The values of the quantitative check result.
             boost::variant<vector_type, map_type> values;

src/storm/settings/modules/IOSettings.cpp

@@ -25,6 +25,7 @@ namespace storm {
             const std::string IOSettings::exportCdfOptionName = "exportcdf";
             const std::string IOSettings::exportCdfOptionShortName = "cdf";
             const std::string IOSettings::exportSchedulerOptionName = "exportscheduler";
+            const std::string IOSettings::exportCheckResultOptionName = "exportresult";
             const std::string IOSettings::exportMonotonicityName = "exportmonotonicity";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
@@ -63,6 +64,7 @@ namespace storm {
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file. Use file extension '.json' to export in json.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportCheckResultOptionName, false, "Exports the result to a given file (if supported by engine). The export will be in json.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportMonotonicityName, false, "Exports the result of monotonicity checking to the given file.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
@@ -175,6 +177,14 @@ namespace storm {
             std::string IOSettings::getExportSchedulerFilename() const {
                 return this->getOption(exportSchedulerOptionName).getArgumentByName("filename").getValueAsString();
             }
+            
+            bool IOSettings::isExportCheckResultSet() const {
+                return this->getOption(exportCheckResultOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string IOSettings::getExportCheckResultFilename() const {
+                return this->getOption(exportCheckResultOptionName).getArgumentByName("filename").getValueAsString();
+            }
 
             bool IOSettings::isExportMonotonicitySet() const {
                 return this->getOption(exportMonotonicityName).getHasOptionBeenSet();

src/storm/settings/modules/IOSettings.h

@@ -105,6 +105,16 @@ namespace storm {
                  * Retrieves a filename to which an optimal scheduler will be exported.
                  */
                  std::string getExportSchedulerFilename() const;
+                
+                /*!
+                 * Retrieves whether the check result should be exported.
+                 */
+                bool isExportCheckResultSet() const;
+                
+                /*!
+                 * Retrieves a filename to which the check result should be exported.
+                 */
+                 std::string getExportCheckResultFilename() const;
 
                 /*!
                 * Retrieves whether an optimal scheduler is to be exported
@@ -360,6 +370,7 @@ namespace storm {
                 static const std::string exportCdfOptionName;
                 static const std::string exportCdfOptionShortName;
                 static const std::string exportSchedulerOptionName;
+                static const std::string exportCheckResultOptionName;
                 static const std::string exportMonotonicityName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;