From 101b49b8985c554142dcce9fa701985241d3587f Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Sep 2018 15:42:48 +0200 Subject: [PATCH] detect unsupported jani-features directly upon parsing the model. --- src/storm-cli-utilities/model-handling.h | 70 ++++++++++---------- src/storm-parsers/api/model_descriptions.cpp | 19 +++++- src/storm-parsers/api/model_descriptions.h | 2 + src/storm/api/builder.h | 12 ++++ src/storm/builder/BuilderType.h | 11 +++ src/storm/storage/jani/Model.cpp | 33 +++++++++ src/storm/storage/jani/Model.h | 12 ++++ 7 files changed, 120 insertions(+), 39 deletions(-) create mode 100644 src/storm/builder/BuilderType.h diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index f0dfc5e6e..480e24a84 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -18,7 +18,8 @@ #include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/jani/Property.h" -#include "storm/logic/RewardAccumulationEliminationVisitor.h" + +#include "storm/builder/BuilderType.h" #include "storm/models/ModelBase.h" @@ -57,12 +58,13 @@ namespace storm { boost::optional> preprocessedProperties; }; - void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { + void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, storm::builder::BuilderType const& builderType) { if (ioSettings.isPrismOrJaniInputSet()) { if (ioSettings.isPrismInputSet()) { input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule().isPrismCompatibilityEnabled()); } else { - auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename()); + storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType); + auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), supportedFeatures); input.model = janiInput.first; auto const& janiPropertyInput = janiInput.second; @@ -96,23 +98,21 @@ namespace storm { } } - SymbolicInput parseSymbolicInput() { + SymbolicInput parseSymbolicInput(storm::builder::BuilderType const& builderType) { auto ioSettings = storm::settings::getModule(); // Parse the property filter, if any is given. boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); SymbolicInput input; - parseSymbolicModelDescription(ioSettings, input); + parseSymbolicModelDescription(ioSettings, input, builderType); parseProperties(ioSettings, input, propertyFilter); return input; } - SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) { + SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::builder::BuilderType const& builderType) { auto ioSettings = storm::settings::getModule(); - auto buildSettings = storm::settings::getModule(); - auto coreSettings = storm::settings::getModule(); SymbolicInput output = input; @@ -125,16 +125,12 @@ namespace storm { } if (!output.properties.empty()) { output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions); - if (output.model.is_initialized() && output.model->isJaniModel()) { - storm::logic::RewardAccumulationEliminationVisitor v(output.model->asJaniModel()); - v.eliminateRewardAccumulations(output.properties); - } } // Check whether conversion for PRISM to JANI is requested or necessary. if (input.model && input.model.get().isPrismProgram()) { bool transformToJani = ioSettings.isPrismToJaniSet(); - bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && buildSettings.isJitSet(); + bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit; STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); transformToJani |= transformToJaniForJit; @@ -154,25 +150,6 @@ namespace storm { } } - // Check whether transformations on the jani model are required - if (output.model && output.model.get().isJaniModel()) { - auto& janiModel = output.model.get().asJaniModel(); - // Check if functions need to be eliminated - if (janiModel.getModelFeatures().hasFunctions()) { - if (!output.preprocessedProperties) { - output.preprocessedProperties = output.properties; - } - janiModel.substituteFunctions(output.preprocessedProperties.get()); - } - - // Check if arrays need to be eliminated. This should be done after! eliminating the functions - if (janiModel.getModelFeatures().hasArrays() && (coreSettings.getEngine() != storm::settings::modules::CoreSettings::Engine::Sparse || buildSettings.isJitSet())) { - if (!output.preprocessedProperties) { - output.preprocessedProperties = output.properties; - } - janiModel.eliminateArrays(output.preprocessedProperties.get()); - } - } return output; } @@ -186,9 +163,29 @@ namespace storm { } } + storm::builder::BuilderType getBuilderType(storm::settings::modules::CoreSettings::Engine const& engine, bool useJit) { + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { + return storm::builder::BuilderType::Dd; + } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + if (useJit) { + return storm::builder::BuilderType::Jit; + } else { + return storm::builder::BuilderType::Explicit; + } + } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { + return storm::builder::BuilderType::Explicit; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to determine the model builder type."); + } + SymbolicInput parseAndPreprocessSymbolicInput() { - SymbolicInput input = parseSymbolicInput(); - input = preprocessSymbolicInput(input); + // Get the used builder type to handle cases where preprocessing depends on it + auto buildSettings = storm::settings::getModule(); + auto coreSettings = storm::settings::getModule(); + auto builderType = getBuilderType(coreSettings.getEngine(), buildSettings.isJitSet()); + + SymbolicInput input = parseSymbolicInput(builderType); + input = preprocessSymbolicInput(input, builderType); exportSymbolicInput(input); return input; } @@ -251,9 +248,10 @@ namespace storm { auto buildSettings = storm::settings::getModule(); std::shared_ptr result; if (input.model) { - if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { + auto builderType = getBuilderType(engine, buildSettings.isJitSet()); + if (builderType == storm::builder::BuilderType::Dd) { result = buildModelDd(input); - } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + } else if (builderType == storm::builder::BuilderType::Explicit || builderType == storm::builder::BuilderType::Jit) { result = buildModelSparse(input, buildSettings); } } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { diff --git a/src/storm-parsers/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp index a440dffef..fd26422af 100644 --- a/src/storm-parsers/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -6,9 +6,9 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/utility/macros.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/BuildSettings.h" namespace storm { namespace api { @@ -18,12 +18,25 @@ namespace storm { program.checkValidity(); return program; } - + std::pair> parseJaniModel(std::string const& filename) { + storm::jani::ModelFeatures features; + // Add derived-operators and state-exit-rewards as these can be handled by all model builders + features.add(storm::jani::ModelFeature::DerivedOperators); + features.add(storm::jani::ModelFeature::StateExitRewards); + return parseJaniModel(filename, features); + } + + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures) { std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename); + modelAndFormulae.first.checkValid(); + // TODO: properties + auto nonEliminatedFeatures = modelAndFormulae.first.restrictToFeatures(allowedFeatures); + STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of allowed features."); return modelAndFormulae; } + } } diff --git a/src/storm-parsers/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h index 533c5e8d1..ff1a44bcd 100644 --- a/src/storm-parsers/api/model_descriptions.h +++ b/src/storm-parsers/api/model_descriptions.h @@ -2,6 +2,7 @@ #include #include +#include namespace storm { namespace prism { @@ -17,6 +18,7 @@ namespace storm { storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false); std::pair> parseJaniModel(std::string const& filename); + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures); } } diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 8aa2e2e17..8461a52fe 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -5,6 +5,7 @@ #include "storm-parsers/parser/ImcaMarkovAutomatonParser.h" #include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/jani/ModelFeatures.h" #include "storm/storage/sparse/ModelComponents.h" #include "storm/models/sparse/Dtmc.h" @@ -16,6 +17,7 @@ #include "storm/builder/DdPrismModelBuilder.h" #include "storm/builder/DdJaniModelBuilder.h" +#include "storm/builder/BuilderType.h" #include "storm/generator/PrismNextStateGenerator.h" #include "storm/generator/JaniNextStateGenerator.h" @@ -29,6 +31,16 @@ namespace storm { namespace api { + storm::jani::ModelFeatures getSupportedJaniFeatures(storm::builder::BuilderType const& builderType) { + storm::jani::ModelFeatures features; + features.add(storm::jani::ModelFeature::DerivedOperators); + features.add(storm::jani::ModelFeature::StateExitRewards); + if (builderType == storm::builder::BuilderType::Explicit) { + features.add(storm::jani::ModelFeature::Arrays); + } + return features; + } + template std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel = false) { if (model.isPrismProgram()) { diff --git a/src/storm/builder/BuilderType.h b/src/storm/builder/BuilderType.h new file mode 100644 index 000000000..8e5e86ad0 --- /dev/null +++ b/src/storm/builder/BuilderType.h @@ -0,0 +1,11 @@ +#pragma once + +namespace storm { + namespace builder { + enum class BuilderType { + Explicit, + Dd, + Jit + }; + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 2285bcbaf..7aa546c85 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1031,6 +1031,39 @@ namespace storm { } } + ModelFeatures Model::restrictToFeatures(ModelFeatures const& modelFeatures) { + std::vector emptyPropertyVector; + return restrictToFeatures(modelFeatures, emptyPropertyVector); + } + + ModelFeatures Model::restrictToFeatures(ModelFeatures const& features, std::vector& properties) { + + ModelFeatures uncheckedFeatures = getModelFeatures(); + // Check if functions need to be eliminated. + if (uncheckedFeatures.hasFunctions() && !features.hasFunctions()) { + substituteFunctions(properties); + } + uncheckedFeatures.remove(ModelFeature::Functions); + + // Check if arrays need to be eliminated. This should be done after! eliminating the functions + if (uncheckedFeatures.hasArrays() && !features.hasArrays()) { + eliminateArrays(properties); + } + uncheckedFeatures.remove(ModelFeature::Arrays); + + // There is no elimination for state exit rewards + if (features.hasStateExitRewards()) { + uncheckedFeatures.remove(ModelFeature::StateExitRewards); + } + + // There is no elimination of derived operators + if (features.hasDerivedOperators()) { + uncheckedFeatures.remove(ModelFeature::DerivedOperators); + } + + return uncheckedFeatures; + } + void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) { this->initialStatesRestriction = initialStatesRestriction; } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index bc32a14c2..14ba38540 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -423,6 +423,18 @@ namespace storm { */ void eliminateArrays(std::vector& properties); + /*! + * Attempts to eliminate all features of this model that are not in the given set of features. + * @return The model features that could not be eliminated. + */ + ModelFeatures restrictToFeatures(ModelFeatures const& modelFeatures); + + /*! + * Attempts to eliminate all features of this model and the given properties that are not in the given set of features. + * @return The model features that could not be eliminated. + */ + ModelFeatures restrictToFeatures(ModelFeatures const& modelFeatures, std::vector& properties); + /*! * Retrieves whether there is an expression restricting the legal initial values of the global variables. */