diff --git a/CHANGELOG.md b/CHANGELOG.md index c4555c987..5c9f74db7 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index db1581e49..fda64be44 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -995,8 +995,7 @@ namespace storm { void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto sparseModel = model->as>(); auto const& ioSettings = storm::settings::getModule(); - verifyProperties(input, - [&sparseModel,&ioSettings,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { + auto verificationCallback = [&sparseModel,&ioSettings,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); if (ioSettings.isExportSchedulerSet()) { @@ -1014,14 +1013,21 @@ namespace storm { result->filter(filter->asQualitativeCheckResult()); } return result; - }, - [&sparseModel,&ioSettings] (std::unique_ptr 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 const& result) { if (ioSettings.isExportSchedulerSet()) { if (result->isExplicitQuantitativeCheckResult()) { if (result->template asExplicitQuantitativeCheckResult().hasScheduler()) { auto const& scheduler = result->template asExplicitQuantitativeCheckResult().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(input,verificationCallback, postprocessingCallback); } template diff --git a/src/storm/api/export.h b/src/storm/api/export.h index e0d0fdf2a..c16adacf4 100644 --- a/src/storm/api/export.h +++ b/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 + void exportCheckResultToJson(std::shared_ptr> const& model, std::unique_ptr 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().toJson(model->getOptionalStateValuations()).dump(4); + } + storm::utility::closeFile(stream); + } + + template <> + void exportCheckResultToJson(std::shared_ptr> const&, std::unique_ptr const&, std::string const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export of check results is not supported for rational functions. "); + } + } } diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp index 8dd14275c..0313cd8dc 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -234,5 +234,39 @@ namespace storm { this->truthValues = newMap; } } + + template + void insertJsonEntry(storm::json& json, uint64_t const& id, bool value, boost::optional const& stateValuations = boost::none) { + storm::json entry; + if (stateValuations) { + entry["s"] = stateValuations->template toJson(id); + } else { + entry["s"] = id; + } + entry["v"] = value; + json.push_back(std::move(entry)); + } + + template + storm::json ExplicitQualitativeCheckResult::toJson(boost::optional const& stateValuations) const { + storm::json result; + if (this->isResultForAllStates()) { + vector_type const& valuesAsVector = boost::get(truthValues); + for (uint64_t state = 0; state < valuesAsVector.size(); ++state) { + insertJsonEntry(result, state, valuesAsVector.get(state), stateValuations); + } + } else { + map_type const& valuesAsMap = boost::get(truthValues); + for (auto const& stateValue : valuesAsMap) { + insertJsonEntry(result, stateValue.first, stateValue.second, stateValuations); + } + } + return result; + } + + template storm::json ExplicitQualitativeCheckResult::toJson(boost::optional const&) const; + template storm::json ExplicitQualitativeCheckResult::toJson(boost::optional const&) const; + + } } diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h index af883e1e0..a38daab4f 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/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 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 + storm::json toJson(boost::optional const& stateValuations = boost::none) const; private: static void performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, bool logicalAnd); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index a3e7d2f6f..c191941b9 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/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 + void insertJsonEntry(storm::json& json, uint64_t const& id, ValueType const& value, boost::optional const& stateValuations = boost::none) { + typename storm::json entry; + if (stateValuations) { + entry["s"] = stateValuations->template toJson(id); + } else { + entry["s"] = id; + } + entry["v"] = value; + json.push_back(std::move(entry)); + } + + template + storm::json ExplicitQuantitativeCheckResult::toJson(boost::optional const& stateValuations) const { + storm::json result; + if (this->isResultForAllStates()) { + vector_type const& valuesAsVector = boost::get(values); + for (uint64_t state = 0; state < valuesAsVector.size(); ++state) { + insertJsonEntry(result, state, valuesAsVector[state], stateValuations); + } + } else { + map_type const& valuesAsMap = boost::get(values); + for (auto const& stateValue : valuesAsMap) { + insertJsonEntry(result, stateValue.first, stateValue.second, stateValuations); + } + } + return result; + } + + template<> + storm::json ExplicitQuantitativeCheckResult::toJson(boost::optional const&) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export of Check results is not supported for Rational Functions."); + } + template class ExplicitQuantitativeCheckResult; #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index 57be3266f..e6fe5a178 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/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 const& getScheduler() const; storm::storage::Scheduler& getScheduler(); + storm::json toJson(boost::optional const& stateValuations = boost::none) const; + private: // The values of the quantitative check result. boost::variant values; diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 7069c453a..82d2de9c8 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/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(); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 447913665..3c7f0bb44 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/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;