From 80bfa6b56e1b769a9bef8b341b1d8825fa46e205 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 19 Mar 2019 16:18:54 +0100 Subject: [PATCH] Allow to quickly check a benchmark from the Quantitative Verification Benchmark Set. --- CHANGELOG.md | 1 + src/storm-cli-utilities/model-handling.h | 66 ++++++++-- src/storm/settings/modules/IOSettings.cpp | 12 +- src/storm/storage/Qvbs.cpp | 149 ++++++++++++++++++++++ src/storm/storage/Qvbs.h | 43 +++++++ 5 files changed, 252 insertions(+), 19 deletions(-) create mode 100644 src/storm/storage/Qvbs.cpp create mode 100644 src/storm/storage/Qvbs.h diff --git a/CHANGELOG.md b/CHANGELOG.md index 66372404c..9bd78afd2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,7 @@ Version 1.3.x ### Version 1.3.1 (under development) - Added support for multi-dimensional quantile queries +- Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the --qvbs option. - Allow bounded types for constants in JANI. - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index bde438b44..ae69cc1e2 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -42,6 +42,7 @@ #include "storm/settings/modules/AbstractionSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/ModelCheckerSettings.h" +#include "storm/storage/Qvbs.h" #include "storm/utility/Stopwatch.h" @@ -114,6 +115,20 @@ namespace storm { return input; } + void ensureNoUndefinedPropertyConstants(std::vector const& properties) { + // Make sure there are no undefined constants remaining in any property. + for (auto const& property : properties) { + std::set usedUndefinedConstants = property.getUndefinedConstants(); + if (!usedUndefinedConstants.empty()) { + std::vector undefinedConstantsNames; + for (auto const& constant : usedUndefinedConstants) { + undefinedConstantsNames.emplace_back(constant.getName()); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The property '" << property << " still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames, ",") << "."); + } + } + } + SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::builder::BuilderType const& builderType) { auto ioSettings = storm::settings::getModule(); @@ -130,18 +145,7 @@ namespace storm { output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions); } - // Make sure there are no undefined constants remaining in any property. - for (auto const& property : output.properties) { - std::set usedUndefinedConstants = property.getUndefinedConstants(); - if (!usedUndefinedConstants.empty()) { - std::vector undefinedConstantsNames; - for (auto const& constant : usedUndefinedConstants) { - undefinedConstantsNames.emplace_back(constant.getName()); - } - - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The property '" << property << " still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames, ",") << "."); - } - } + ensureNoUndefinedPropertyConstants(output.properties); // Check whether conversion for PRISM to JANI is requested or necessary. if (input.model && input.model.get().isPrismProgram()) { @@ -195,14 +199,48 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to determine the model builder type."); } + SymbolicInput parseAndPreprocessSymbolicInputQvbs(storm::settings::modules::IOSettings const& ioSettings, storm::builder::BuilderType const& builderType) { + // Parse the model input + SymbolicInput input; + storm::storage::QvbsBenchmark benchmark(ioSettings.getQvbsModelName()); + STORM_PRINT_AND_LOG(benchmark.getInfo(ioSettings.getQvbsInstanceIndex(), ioSettings.getQvbsPropertyFilter())); + storm::utility::Stopwatch modelParsingWatch(true); + storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType); + auto janiInput = storm::api::parseJaniModel(benchmark.getJaniFile(ioSettings.getQvbsInstanceIndex()), supportedFeatures, ioSettings.getQvbsPropertyFilter()); + input.model = std::move(janiInput.first); + input.properties = std::move(janiInput.second); + modelParsingWatch.stop(); + STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl); + + // Parse additional properties + boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); + parseProperties(ioSettings, input, propertyFilter); + + // Substitute constant definitions + auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex())); + input.model = input.model.get().preprocess(constantDefinitions); + if (!input.properties.empty()) { + input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions); + } + + ensureNoUndefinedPropertyConstants(input.properties); + return input; + } + SymbolicInput parseAndPreprocessSymbolicInput() { // Get the used builder type to handle cases where preprocessing depends on it auto buildSettings = storm::settings::getModule(); auto coreSettings = storm::settings::getModule(); + auto ioSettings = storm::settings::getModule(); auto builderType = getBuilderType(coreSettings.getEngine(), buildSettings.isJitSet()); - SymbolicInput input = parseSymbolicInput(builderType); - input = preprocessSymbolicInput(input, builderType); + SymbolicInput input; + if (ioSettings.isQvbsInputSet()) { + input = parseAndPreprocessSymbolicInputQvbs(ioSettings, builderType); + } else { + input = parseSymbolicInput(builderType); + input = preprocessSymbolicInput(input, builderType); + } exportSymbolicInput(input); return input; } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index a862290d3..c6e6582ca 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -90,7 +90,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, qvbsInputOptionName, false, "Selects a model from the Quantitative Verification Benchmark Set.").setShortName(qvbsInputOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("model", "The short model name as in the benchmark set.").build()) .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("instance-index", "The selected instance of this model.").setDefaultValueUnsignedInteger(0).build()) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The comma separated list of property names to check. Empty string checks all, [] checks none.").setDefaultValueString("").build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The comma separated list of property names to check. Omit to check all, \"\" to check none.").setDefaultValueString("").build()) .build()); #ifdef STORM_HAVE_QVBS std::string qvbsRootDefault = STORM_QVBS_ROOT; @@ -263,10 +263,12 @@ namespace storm { boost::optional> IOSettings::getQvbsPropertyFilter() const { std::string listAsString = this->getOption(qvbsInputOptionName).getArgumentByName("filter").getValueAsString(); - if (listAsString == "[]") { - return std::vector(); - } else if (listAsString == "") { - return boost::none; + if (listAsString == "") { + if (this->getOption(qvbsInputOptionName).getArgumentByName("filter").wasSetFromDefaultValue()) { + return boost::none; + } else { + return std::vector(); + } } else { return storm::parser::parseCommaSeperatedValues(listAsString); } diff --git a/src/storm/storage/Qvbs.cpp b/src/storm/storage/Qvbs.cpp new file mode 100644 index 000000000..b9d392386 --- /dev/null +++ b/src/storm/storage/Qvbs.cpp @@ -0,0 +1,149 @@ +#include "storm/storage/Qvbs.h" + +#include + +#include "storm/utility/macros.h" +#include "storm/utility/file.h" +#include "storm/utility/string.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + + modernjson::json readQvbsJsonFile(std::string const& filePath) { + STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(filePath), storm::exceptions::WrongFormatException, "QVBS json file " << filePath << " was not found."); + modernjson::json result; + std::ifstream file; + storm::utility::openFile(filePath, file); + result << file; + storm::utility::closeFile(file); + return result; + } + + std::string getString(modernjson::json const& structure, std::string const& errorInfo = "") { + if (structure.is_number_integer()) { + return std::to_string(structure.get()); + } else if (structure.is_number_float()) { + return std::to_string(structure.get()); + } else if (structure.is_string()) { + return structure.get(); + } else if (structure.is_boolean()) { + return structure.get() ? "true" : "false"; + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Expected a string, number, or bool, got '" << structure.dump() << "' " << errorInfo); + } + return ""; + } + + std::string findModelPath(std::string const& modelName) { + std::string rootIndexFile = storm::settings::getModule().getQvbsRoot() + "/index.json"; + + auto modelPaths = readQvbsJsonFile(rootIndexFile); + storm::utility::string::SimilarStrings similarNames(modelName, 0.6, false); + for (auto const& pathJson : modelPaths) { + STORM_LOG_THROW(pathJson.count("path") == 1, storm::exceptions::WrongFormatException, "QVBS file " << rootIndexFile << " has unexpected format."); + std::string path = getString(pathJson["path"], "Path entry in QVBS file " + rootIndexFile); + std::string currModelName = path.substr(path.find("/") + 1); + if (currModelName == modelName) { + return storm::settings::getModule().getQvbsRoot() + "/" + path; + } else { + similarNames.add(currModelName); + } + } + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "QVBS model '" + modelName + "' was not found. " + similarNames.toDidYouMeanString()); + return ""; + } + + QvbsBenchmark::QvbsBenchmark(std::string const& modelName) { + std::string actualModelName = modelName; + std::transform(actualModelName.begin(), actualModelName.end(), actualModelName.begin(), ::tolower); + modelPath = findModelPath(actualModelName); + std::string indexPath = modelPath + "/index.json"; + modelData = readQvbsJsonFile(indexPath); + + STORM_LOG_THROW(modelData.count("files") == 1, storm::exceptions::WrongFormatException, "No files in " + indexPath + "."); + for (auto const& fileJson : modelData["files"]) { + std::string janiFileName = getString(fileJson["file"], "file of " + indexPath + "."); + if (fileJson.count("open-parameter-values") == 1 && fileJson["open-parameter-values"].size() > 0) { + for (auto const& openParJson : fileJson["open-parameter-values"]) { + std::string constantDefString = ""; + if (openParJson.count("values") == 1) { + for (auto const& valueJson : openParJson["values"]) { + if (constantDefString != "") { + constantDefString += ","; + } + constantDefString += getString(valueJson["name"], "open-parameter-values in files in " + indexPath + ".") + "="; + constantDefString += getString(valueJson["value"], "open-parameter-values in files in " + indexPath + "."); + } + } + constantDefinitions.push_back(constantDefString); + janiFiles.push_back(modelPath + "/" + janiFileName); + instanceInfos.push_back(janiFileName + " \t" + constantDefString); + if (openParJson.count("states") == 1 && openParJson["states"].size() > 0) { + uint64_t states = 0; + for (auto const& statesJson : openParJson["states"]) { + auto note = getString(statesJson["note"]); + if (note.find("Storm") != std::string::npos) { + states = statesJson["number"].get(); + } + } + if (states > 0) { + instanceInfos.back() += " \t(" + std::to_string(states) + " states)"; + } + } + } + } else { + constantDefinitions.push_back(""); + janiFiles.push_back(janiFileName); + } + } + } + + std::string const& QvbsBenchmark::getJaniFile(uint64_t instanceIndex ) const { + STORM_LOG_THROW(instanceIndex < janiFiles.size(), storm::exceptions::InvalidArgumentException, "Instance index " << instanceIndex << " is too high."); + return janiFiles[instanceIndex]; + } + + std::string const& QvbsBenchmark::getConstantDefinition(uint64_t instanceIndex) const { + STORM_LOG_THROW(instanceIndex < constantDefinitions.size(), storm::exceptions::InvalidArgumentException, "Instance index " << instanceIndex << " is too high."); + return constantDefinitions[instanceIndex]; + } + + std::string QvbsBenchmark::getInfo(uint64_t instanceIndex, boost::optional> propertyFilter) const { + std::stringstream s; + s << "--------------------------------------------------------------" << std::endl; + s << "QVBS " << getString(modelData["type"]) << "-Benchmark: " << getString(modelData["name"]) << " (" << getString(modelData["short"]) << ") v" << getString(modelData["version"]) << std::endl; + if (instanceInfos.size() == 1) { + s << "1 instance:" << std::endl; + } else if (instanceInfos.size() > 1) { + s << instanceInfos.size() << " instances:" << std::endl; + } + for (uint64_t i = 0; i < instanceInfos.size(); ++ i) { + s << "\t" << (i==instanceIndex ? "*" : " ") << i << "\t" << instanceInfos[i] << std::endl; + } + if (modelData.count("properties") == 1) { + if (modelData["properties"].size() == 1) { + s << "1 property:" << std::endl; + } else if (modelData["properties"].size() > 1) { + s << modelData["properties"].size() << " properties:" << std::endl; + } + for (auto const& property : modelData["properties"]) { + std::string propertyName = getString(property["name"]); + s << "\t"; + if (!propertyFilter.is_initialized() || std::find(propertyFilter->begin(), propertyFilter->end(), propertyName) != propertyFilter->end()) { + s << "*"; + } else { + s << " "; + } + s << propertyName << " \t(" << getString(property["type"]) << ")" << std::endl; + } + } + s << "--------------------------------------------------------------" << std::endl; + return s.str(); + } + + } +} \ No newline at end of file diff --git a/src/storm/storage/Qvbs.h b/src/storm/storage/Qvbs.h new file mode 100644 index 000000000..d88c28bd9 --- /dev/null +++ b/src/storm/storage/Qvbs.h @@ -0,0 +1,43 @@ +#pragma once + +#include +#include +#include + +// JSON parser +#include "json.hpp" +namespace modernjson { + using json = nlohmann::json; +} + + +namespace storm { + namespace storage { + + /*! + * This class provides easy access to a benchmark of the Quantitative Verification Benchmark Set + * http://qcomp.org/benchmarks/ + */ + class QvbsBenchmark { + public: + /*! + * @param modelName the (short) model name of the considered model. + */ + QvbsBenchmark(std::string const& modelName); + + std::string const& getJaniFile(uint64_t instanceIndex = 0) const; + std::string const& getConstantDefinition(uint64_t instanceIndex = 0) const; + + std::string getInfo(uint64_t instanceIndex = 0, boost::optional> propertyFilter = boost::none) const; + private: + + std::vector janiFiles; + std::vector constantDefinitions; + std::vector instanceInfos; + + std::string modelPath; + modernjson::json modelData; + }; + } +} +