From 62dd371411fa720c7f3a3ea9a7d318fe3bcde07e Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 26 Jun 2017 14:22:22 +0200 Subject: [PATCH] storm-pars cli --- src/storm-pars-cli/CMakeLists.txt | 7 + src/storm-pars-cli/storm-pars.cpp | 362 ++++++++++++++++++++++++++++++ 2 files changed, 369 insertions(+) create mode 100644 src/storm-pars-cli/CMakeLists.txt create mode 100644 src/storm-pars-cli/storm-pars.cpp diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt new file mode 100644 index 000000000..9cd155e35 --- /dev/null +++ b/src/storm-pars-cli/CMakeLists.txt @@ -0,0 +1,7 @@ +# Create storm-pars. +add_executable(storm-pars-cli ${PROJECT_SOURCE_DIR}/src/storm-pars-cli/storm-pars.cpp) +target_link_libraries(storm-pars-cli storm-pars) # Adding headers for xcode +set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars") + +# installation +install(TARGETS storm-pars-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp new file mode 100644 index 000000000..8ffaa852e --- /dev/null +++ b/src/storm-pars-cli/storm-pars.cpp @@ -0,0 +1,362 @@ + +#include "storm-pars/api/storm-pars.h" +#include "storm-pars/settings/ParsSettings.h" +#include "storm-pars/settings/modules/ParametricSettings.h" +#include "storm-pars/settings/modules/RegionSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/api/storm.h" +#include "storm/cli/cli.h" +#include "storm/models/ModelBase.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/utility/file.h" +#include "storm/utility/initialize.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/macros.h" + +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BisimulationSettings.h" + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/NotSupportedException.h" + +#include "storm/cli/cli.cpp" + +namespace storm { + namespace pars { + + typedef typename storm::cli::SymbolicInput SymbolicInput; + + template + std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + return storm::api::buildSparseModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet()); + } + + template + std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + storm::utility::Stopwatch modelBuildingWatch(true); + + std::shared_ptr result; + if (input.model) { + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + result = storm::cli::buildModelDd(input); + } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + result = storm::pars::buildModelSparse(input, ioSettings); + } + } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { + STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); + result = storm::cli::buildModelExplicit(ioSettings); + } + + modelBuildingWatch.stop(); + if (result) { + STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); + } + + return result; + } + + + template + std::vector> parseRegions(std::shared_ptr const& model) { + std::vector> result; + auto regionSettings = storm::settings::getModule(); + if (regionSettings.isRegionSet()) { + result = storm::api::parseRegions(regionSettings.getRegionString(), *model); + } + return result; + } + + template + std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + auto parametricSettings = storm::settings::getModule(); + + std::pair, bool> result = std::make_pair(model, false); + + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as>()); + result.second = true; + } + + if (generalSettings.isBisimulationSet()) { + result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as>(), input, bisimulationSettings); + result.second = true; + } + + if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { + result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)); + result.second = true; + } + + return result; + } + + template + std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + + std::pair, bool> result = std::make_pair(model, false); + + auto coreSettings = storm::settings::getModule(); + if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { + // Currently, hybrid engine for parametric models just referrs to building the model symbolically. + STORM_LOG_INFO("Translating symbolic model to sparse model..."); + result.first = storm::api::transformSymbolicToSparseModel(model); + result.second = true; + // Invoke preprocessing on the sparse model + auto sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.first->as>(), input); + if (sparsePreprocessingResult.second) { + result.first = sparsePreprocessingResult.first; + } + } + return result; + } + + template + std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + storm::utility::Stopwatch preprocessingWatch(true); + + std::pair, bool> result = std::make_pair(model, false); + if (model->isSparseModel()) { + result = storm::pars::preprocessSparseModel(result.first->as>(), input); + } else { + STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); + result = storm::pars::preprocessDdModel(result.first->as>(), input); + } + + if (result.second) { + STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); + } + return result; + } + + template + void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { + if (result) { + STORM_PRINT_AND_LOG("Result (initial states): "); + + auto const* regionCheckResult = dynamic_cast const*>(result.get()); + if (regionCheckResult != nullptr) { + auto regionSettings = storm::settings::getModule(); + std::stringstream outStream; + if (regionSettings.isPrintFullResultSet()) { + regionCheckResult->writeToStream(outStream); + } else { + regionCheckResult->writeCondensedToStream(outStream); + } + outStream << std::endl; + if (!regionSettings.isPrintNoIllustrationSet()) { + auto const* regionRefinementCheckResult = dynamic_cast const*>(regionCheckResult); + if (regionRefinementCheckResult != nullptr) { + regionRefinementCheckResult->writeIllustrationToStream(outStream); + } + } + STORM_PRINT_AND_LOG(outStream.str()); + } else { + STORM_PRINT_AND_LOG(*result); + } + if (watch) { + STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl); + } + } else { + STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); + } + } + + template + void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback) { + for (auto const& property : properties) { + storm::cli::printModelCheckingProperty(property); + storm::utility::Stopwatch watch(true); + std::unique_ptr result = verificationCallback(property.getRawFormula()); + watch.stop(); + printInitialStatesResult(result, property, &watch); + postprocessingCallback(result); + } + } + + template + std::pair>, std::shared_ptr> performSimplification(std::shared_ptr> const& model, std::shared_ptr const& formula) { + auto parametricSettings = storm::settings::getModule(); + + std::pair>, std::shared_ptr> result; + + if (!(parametricSettings.isSimplifySet() && storm::api::simplifyParametricModel(model, formula, result.first, result.second))) { + result = std::make_pair(model, formula); + } + + return result; + } + + template + void verifyPropertiesWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input) { + verifyProperties(input.properties, + [&model] (std::shared_ptr const& formula) { + auto simplificationResult = performSimplification(model, formula); + std::unique_ptr result = storm::api::verifyWithSparseEngine(simplificationResult.first, storm::api::createTask(simplificationResult.second, true)); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(simplificationResult.first->getInitialStates())); + return result; + }, + [&model] (std::unique_ptr const& result) { + auto parametricSettings = storm::settings::getModule(); + if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { + auto dtmc = model->template as>(); + storm::api::exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()],storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } + }); + } + + template + void verifyRegionsWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { + STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions."); + + auto parametricSettings = storm::settings::getModule(); + auto regionSettings = storm::settings::getModule(); + + std::function(std::shared_ptr const& formula)> verificationCallback; + std::function const&)> postprocessingCallback; + + if (regions.size() == 1) { + STORM_PRINT_AND_LOG(std::endl << "Analyzing parameter region " << regions.front()); + } else { + STORM_PRINT_AND_LOG(std::endl << "Analyzing " << regions.size() << " parameter regions"); + } + + auto engine = regionSettings.getRegionCheckEngine(); + STORM_PRINT_AND_LOG(" using " << engine); + + // Check the given set of regions with or without refinement + if (regionSettings.isRefineSet()) { + STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions."); + STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl); + verificationCallback = [&] (std::shared_ptr const& formula) { + ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getRefinementThreshold()); + auto simplificationResult = performSimplification(model, formula); + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(simplificationResult.first, storm::api::createTask(simplificationResult.second, true), regions.front(), refinementThreshold, engine); + return result; + }; + } else { + STORM_PRINT_AND_LOG("." << std::endl); + verificationCallback = [&] (std::shared_ptr const& formula) { + auto simplificationResult = performSimplification(model, formula); + std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(simplificationResult.first, storm::api::createTask(simplificationResult.second, true), regions, engine); + return result; + }; + } + + postprocessingCallback = [&] (std::unique_ptr const& result) { + if (parametricSettings.exportResultToFile()) { + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); + } + }; + + verifyProperties(input.properties, verificationCallback, postprocessingCallback); + } + + template + void verifyWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { + if (regions.empty()) { + storm::pars::verifyPropertiesWithSparseEngine(model, input); + } else { + storm::pars::verifyRegionsWithSparseEngine(model, input, regions); + } + } + + template + void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions) { + STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); + storm::pars::verifyWithSparseEngine(model->as>(), input, regions); + } + + template + void processInputWithValueTypeAndDdlib(SymbolicInput& input) { + auto coreSettings = storm::settings::getModule(); + auto ioSettings = storm::settings::getModule(); + + auto engine = coreSettings.getEngine(); + STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); + + std::shared_ptr model; + if (!ioSettings.isNoBuildModelSet()) { + model = storm::pars::buildModel(engine, input, ioSettings); + } + + if (model) { + model->printModelInformationToStream(std::cout); + } + + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); + + if (model) { + auto preprocessingResult = storm::pars::preprocessModel(model, input); + if (preprocessingResult.second) { + model = preprocessingResult.first; + model->printModelInformationToStream(std::cout); + } + } + + std::vector> regions = parseRegions(model); + + if (model) { + storm::cli::exportModel(model, input); + verifyParametricModel(model, input, regions); + } + } + + void processOptions() { + // Start by setting some urgent options (log levels, resources, etc.) + storm::cli::setUrgentOptions(); + + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) + SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); + + auto coreSettings = storm::settings::getModule(); + auto engine = coreSettings.getEngine(); + STORM_LOG_WARN_COND(engine != storm::settings::modules::CoreSettings::Engine::Dd || engine != storm::settings::modules::CoreSettings::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); + + processInputWithValueTypeAndDdlib(symbolicInput); + } + + int64_t process(const int argc, const char** argv) { + storm::utility::setUp(); + storm::cli::printHeader("Storm-pars", argc, argv); + storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); + + storm::utility::Stopwatch totalTimer(true); + if (!storm::cli::parseOptions(argc, argv)) { + return -1; + } + + processOptions(); + + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + + storm::utility::cleanUp(); + return 0; + } + } +} + + +/*! + * Main entry point of the executable storm-pars. + */ +int main(const int argc, const char** argv) { + + try { + return storm::pars::process(argc, argv); + } catch (storm::exceptions::BaseException const& exception) { + STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what()); + return 1; + } catch (std::exception const& exception) { + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pars to terminate. The message of this exception is: " << exception.what()); + return 2; + } +}