From c6b984ca51e12fd795c2b2573bbb66423dd22dfc Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 6 Mar 2020 13:39:33 +0100 Subject: [PATCH] Do not perform the conversion from a prism program to a jani model twice. --- src/storm-cli-utilities/cli.cpp | 4 +- src/storm-cli-utilities/model-handling.h | 116 ++++++++++++++--------- src/storm-pars-cli/storm-pars.cpp | 4 +- src/storm-pomdp-cli/storm-pomdp.cpp | 4 +- src/storm/utility/Portfolio.cpp | 20 ++-- src/storm/utility/Portfolio.h | 9 +- 6 files changed, 85 insertions(+), 72 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index df10dcbf1..12bd6a16f 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -246,10 +246,10 @@ namespace storm { SymbolicInput symbolicInput = parseSymbolicInput(); // Obtain settings for model processing - ModelProcessingInformation mpi = getModelProcessingInformation(symbolicInput); + ModelProcessingInformation mpi; // Preprocess the symbolic input - symbolicInput = preprocessSymbolicInput(symbolicInput, mpi.engine); + std::tie(symbolicInput, mpi) = preprocessSymbolicInput(symbolicInput); // Export symbolic input (if requested) exportSymbolicInput(symbolicInput); diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index d8f666faf..c75423612 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -156,6 +156,9 @@ namespace storm { // If set, bisimulation will be applied. bool applyBisimulation; + // If set, a transformation to Jani will be enforced + bool transformToJani; + // Which data type is to be used for numbers ... enum class ValueType { FinitePrecision, @@ -175,16 +178,17 @@ namespace storm { void getModelProcessingInformationPortfolio(SymbolicInput const& input, ModelProcessingInformation& mpi) { auto hints = storm::settings::getModule(); - STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a symbolic model (PRISM or JANI."); + STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model."); + STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model."); std::vector const& properties = input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties; STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a property."); STORM_LOG_WARN_COND(properties.size() == 1, "Portfolio engine does not support decisions based on multiple properties. Only the first property will be considered."); storm::utility::Portfolio pf; if (hints.isNumberStatesSet()) { - pf.predict(input.model.get(), properties.front(), hints.getNumberStates()); + pf.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates()); } else { - pf.predict(input.model.get(), properties.front()); + pf.predict(input.model->asJaniModel(), properties.front()); } mpi.engine = pf.getEngine(); @@ -202,8 +206,14 @@ namespace storm { << std::noboolalpha << std::endl); } - ModelProcessingInformation getModelProcessingInformation(SymbolicInput const& input) { + /*! + * Sets the model processing information based on the given input. + * Finding the right model processing information might require a conversion to jani. + * In this case, the jani conversion is stored in the transformedJaniInput pointer (unless it is null) + */ + ModelProcessingInformation getModelProcessingInformation(SymbolicInput const& input, std::shared_ptr const& transformedJaniInput = nullptr) { ModelProcessingInformation mpi; + auto ioSettings = storm::settings::getModule(); auto coreSettings = storm::settings::getModule(); auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); @@ -224,10 +234,29 @@ namespace storm { } // Since the remaining settings could depend on the ones above, we need apply the portfolio engine now. - bool usePortfolio = mpi.engine == storm::utility::Engine::Portfolio; + bool usePortfolio = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Portfolio; if (usePortfolio) { - // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic) - getModelProcessingInformationPortfolio(input, mpi); + if (input.model->isJaniModel()) { + // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic) + getModelProcessingInformationPortfolio(input, mpi); + } else { + // Transform Prism to jani first + STORM_LOG_ASSERT(input.model->isPrismProgram(), "Unexpected type of input."); + SymbolicInput janiInput; + janiInput.properties = input.properties; + storm::prism::Program const& prog = input.model.get().asPrismProgram(); + auto modelAndProperties = prog.toJani(input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties); + janiInput.model = modelAndProperties.first; + if (!modelAndProperties.second.empty()) { + janiInput.preprocessedProperties = std::move(modelAndProperties.second); + } + // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic) + getModelProcessingInformationPortfolio(janiInput, mpi); + if (transformedJaniInput) { + // We cache the transformation result. + *transformedJaniInput = std::move(janiInput); + } + } } // Check whether these settings are compatible with the provided input. @@ -255,8 +284,16 @@ namespace storm { STORM_LOG_WARN("The model checking query does not seem to be supported for the selected engine. Storm will try to solve the query, but you will most likely get an error for at least one of the provided properties."); } } - + // Set whether a transformation to jani is required or necessary + mpi.transformToJani = ioSettings.isPrismToJaniSet(); + auto builderType = storm::utility::getBuilderType(mpi.engine); + bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit; + STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); + bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) && (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA); + STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForDdMA, "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model."); + mpi.transformToJani |= (transformToJaniForJit || transformToJaniForDdMA); + // Set the Valuetype used during model building mpi.buildValueType = mpi.verificationValueType; if (bisimulationSettings.useExactArithmeticInDdBisimulation()) { @@ -294,17 +331,11 @@ namespace storm { } } - SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::utility::Engine const& engine) { + std::pair preprocessSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); - auto builderType = storm::utility::getBuilderType(engine); SymbolicInput output = input; - if (output.model && output.model.get().isJaniModel()) { - storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType); - storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures); - } - // Substitute constant definitions in symbolic input. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); std::map constantDefinitions; @@ -315,34 +346,37 @@ namespace storm { if (!output.properties.empty()) { output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions); } - ensureNoUndefinedPropertyConstants(output.properties); + auto transformedJani = std::make_shared(); + ModelProcessingInformation mpi = getModelProcessingInformation(output, transformedJani); + + auto builderType = storm::utility::getBuilderType(mpi.engine); // Check whether conversion for PRISM to JANI is requested or necessary. - if (input.model && input.model.get().isPrismProgram()) { - bool transformToJani = ioSettings.isPrismToJaniSet(); - 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."); - bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) && (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA); - STORM_LOG_WARN_COND(transformToJani || !transformToJaniForDdMA, "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model."); - transformToJani |= (transformToJaniForJit || transformToJaniForDdMA); - - if (transformToJani) { - storm::prism::Program const& model = output.model.get().asPrismProgram(); - auto modelAndProperties = model.toJani(output.properties); - - // Remove functions here - modelAndProperties.first.substituteFunctions(); - - output.model = modelAndProperties.first; - - if (!modelAndProperties.second.empty()) { - output.preprocessedProperties = std::move(modelAndProperties.second); + if (output.model && output.model.get().isPrismProgram()) { + if (mpi.transformToJani) { + if (transformedJani->model) { + // Use the cached transformation if possible + output = std::move(*transformedJani); + } else { + storm::prism::Program const& model = output.model.get().asPrismProgram(); + auto modelAndProperties = model.toJani(output.properties); + + output.model = modelAndProperties.first; + + if (!modelAndProperties.second.empty()) { + output.preprocessedProperties = std::move(modelAndProperties.second); + } } } } - return output; + if (output.model && output.model.get().isJaniModel()) { + storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType); + storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures); + } + + return {output, mpi}; } void exportSymbolicInput(SymbolicInput const& input) { @@ -355,16 +389,6 @@ namespace storm { } } - SymbolicInput parseAndPreprocessSymbolicInput(storm::utility::Engine const& engine) { - // Get the used builder type to handle cases where preprocessing depends on it - auto buildSettings = storm::settings::getModule(); - - SymbolicInput input = parseSymbolicInput(); - input = preprocessSymbolicInput(input, engine); - exportSymbolicInput(input); - return input; - } - std::vector> createFormulasToRespect(std::vector const& properties) { std::vector> result = storm::api::extractFormulasFromProperties(properties); diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 0b7ff3bbd..4ae3fde89 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -783,8 +783,8 @@ namespace storm { // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) auto symbolicInput = storm::cli::parseSymbolicInput(); - auto mpi = storm::cli::getModelProcessingInformation(symbolicInput); - symbolicInput = storm::cli::preprocessSymbolicInput(symbolicInput, mpi.engine); + storm::cli::ModelProcessingInformation mpi; + std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput); processInputWithValueTypeAndDdlib(symbolicInput, mpi); } diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 3da5f6662..6b8cfefa1 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -99,8 +99,8 @@ int main(const int argc, const char** argv) { auto const& pomdpSettings = storm::settings::getModule(); auto symbolicInput = storm::cli::parseSymbolicInput(); - auto mpi = storm::cli::getModelProcessingInformation(symbolicInput); - symbolicInput = storm::cli::preprocessSymbolicInput(symbolicInput, mpi.engine); + storm::cli::ModelProcessingInformation mpi; + std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput); // We should not export here if we are going to do some processing first. auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, mpi); diff --git a/src/storm/utility/Portfolio.cpp b/src/storm/utility/Portfolio.cpp index c45f51d2b..2045ed153 100644 --- a/src/storm/utility/Portfolio.cpp +++ b/src/storm/utility/Portfolio.cpp @@ -34,15 +34,7 @@ namespace storm { } struct Features { - Features(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property) { - if (!modelDescription.isJaniModel()) { - initialize(modelDescription.toJani().asJaniModel(), property); - } else { - initialize(modelDescription.asJaniModel(), property); - } - } - - void initialize(storm::jani::Model const& model, storm::jani::Property const& property) { + Features(storm::jani::Model const& model, storm::jani::Property const& property) { continuousTime = !model.isDiscreteTimeModel(); nondeterminism = !model.isDeterministicModel(); propertyType = getPropertyType(property); @@ -65,9 +57,9 @@ namespace storm { // Intentionally left empty } - void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property) { + void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property) { typedef pfinternal::PropertyType PropertyType; - auto f = pfinternal::Features(modelDescription, property); + auto f = pfinternal::Features(model, property); { // Decision tree start if (f.numEdges <= 618) { @@ -171,12 +163,12 @@ namespace storm { } - void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property, uint64_t stateEstimate) { + void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t stateEstimate) { typedef pfinternal::PropertyType PropertyType; - auto f = pfinternal::Features(modelDescription, property); + auto f = pfinternal::Features(model, property); f.stateEstimate = stateEstimate; // TODO: Actually make use of the estimate - predict(modelDescription, property); + predict(model, property); } storm::utility::Engine Portfolio::getEngine() const { diff --git a/src/storm/utility/Portfolio.h b/src/storm/utility/Portfolio.h index 8fceda6b8..472369bc7 100644 --- a/src/storm/utility/Portfolio.h +++ b/src/storm/utility/Portfolio.h @@ -5,13 +5,10 @@ namespace storm { namespace jani { + class Model; class Property; } - namespace storage { - class SymbolicModelDescription; - } - namespace utility { class Portfolio { public: @@ -20,13 +17,13 @@ namespace storm { /*! * Predicts "good" settings for the provided model checking query */ - void predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property); + void predict(storm::jani::Model const& model, storm::jani::Property const& property); /*! * Predicts "good" settings for the provided model checking query * @param stateEstimate A hint that gives a (rough) estimate for the number of states. */ - void predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property, uint64_t stateEstimate); + void predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t stateEstimate); /// Retrieve "good" settings after calling predict. storm::utility::Engine getEngine() const;