From 274bfef6527e30e46bb0e79c7bc6fa6b1ea2850d Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 12 Sep 2018 14:29:48 +0200 Subject: [PATCH] started to extend storm-conv for array elimination --- src/storm-conv-cli/storm-conv.cpp | 35 +++++++++++++++++++ src/storm-conv/api/storm-conv.cpp | 14 ++++++-- src/storm-conv/api/storm-conv.h | 2 +- .../options/JaniConversionOptions.cpp | 4 +-- .../converter/options/JaniConversionOptions.h | 8 ++++- .../modules/ConversionInputSettings.cpp | 13 ++++++- .../modules/ConversionInputSettings.h | 11 ++++++ .../settings/modules/JaniExportSettings.cpp | 12 +++++++ .../settings/modules/JaniExportSettings.h | 6 ++++ src/storm-gspn/api/storm-gspn.cpp | 5 +-- src/storm-pgcl-cli/storm-pgcl.cpp | 2 +- src/storm/storage/jani/Model.cpp | 7 ++-- src/storm/storage/jani/Model.h | 8 ++++- 13 files changed, 113 insertions(+), 14 deletions(-) diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index a499fccf2..1977cfdb7 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -124,14 +124,49 @@ namespace storm { } } + void processJaniInput() { + auto const& input = storm::settings::getModule(); + + // Parse the jani model + auto janiModelProperties = storm::api::parseJaniModel(input.getJaniInputFilename()); + storm::storage::SymbolicModelDescription janiModel(janiModelProperties.first); + // Parse properties (if available, otherwise take the ones from the jani file) + std::vector properties; + if (input.isPropertyInputSet()) { + boost::optional> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter()); + properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), janiModel, propertyFilter); + } else { + properties.insert(properties.end(), janiModelProperties.second.begin(), janiModelProperties.second.end()); + } + + // Substitute constant definitions in program and properties. + std::string constantDefinitionString = input.getConstantDefinitionString(); + auto constantDefinitions = janiModel.parseConstantDefinitions(constantDefinitionString); + janiModel = janiModel.preprocess(constantDefinitions); + if (!properties.empty()) { + properties = storm::api::substituteConstantsInProperties(properties, constantDefinitions); + } + + // Branch on the type of output + auto const& output = storm::settings::getModule(); + if (output.isJaniOutputSet()) { +// processJaniInputJaniOutput(janiModel.asJaniModel(), properties); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible."); + } + } + void processOptions() { // Start by setting some urgent options (log levels, etc.) setUrgentOptions(); // Branch on the type of input auto const& input = storm::settings::getModule(); + STORM_LOG_THROW(!(input.isPrismInputSet() && input.isJaniInputSet()), storm::exceptions::InvalidSettingsException, "Multiple input options were set."); if (input.isPrismInputSet()) { processPrismInput(); + } else if (input.isJaniInputSet()) { + processJaniInput(); } } } diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index aa37dd191..9a965fb65 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -11,7 +11,7 @@ namespace storm { namespace api { - void postprocessJani(storm::jani::Model& janiModel, storm::converter::JaniConversionOptions options) { + void transformJani(storm::jani::Model& janiModel, std::vector& properties, storm::converter::JaniConversionOptions const& options) { if (!options.locationVariables.empty()) { for (auto const& pair : options.locationVariables) { @@ -21,7 +21,7 @@ namespace storm { } } - if (options.exportFlattened) { + if (options.flatten) { std::shared_ptr smtSolverFactory; if (storm::settings::hasModule()) { smtSolverFactory = std::make_shared(); @@ -35,6 +35,14 @@ namespace storm { janiModel.makeStandardJaniCompliant(); } + if (!options.allowArrays && janiModel.getModelFeatures().hasArrays()) { + janiModel.eliminateArrays(properties); + } + + //if (!options.allowFunctions && janiModel.getModelFeatures().hasFunctions()) { + //janiModel = janiModel.substituteFunctions(); + //} + if (options.modelName) { janiModel.setName(options.modelName.get()); } @@ -53,7 +61,7 @@ namespace storm { } // Postprocess Jani model based on the options - postprocessJani(res.first, options.janiOptions); + transformJani(res.first, res.second, options.janiOptions); return res; } diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h index 42cbf804d..12e45269d 100644 --- a/src/storm-conv/api/storm-conv.h +++ b/src/storm-conv/api/storm-conv.h @@ -15,7 +15,7 @@ namespace storm { namespace api { - void postprocessJani(storm::jani::Model& janiModel, storm::converter::JaniConversionOptions options); + void transformJani(storm::jani::Model& janiModel, std::vector& properties, storm::converter::JaniConversionOptions const& options); std::pair> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties = std::vector(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions()); diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index 7b72c4797..4b7a78d76 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.cpp +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -3,11 +3,11 @@ namespace storm { namespace converter { - JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), exportFlattened(false) { + JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), flatten(false), allowArrays(true), allowFunctions(true) { // Intentionally left empty }; - JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), exportFlattened(settings.isExportFlattenedSet()) { + JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), flatten(settings.isExportFlattenedSet()), allowArrays(!settings.isEliminateArraysSet()), allowFunctions(!settings.isEliminateFunctionsSet()) { // Intentionally left empty }; } diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h index 000d9cc3b..34452315b 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.h +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -21,11 +21,17 @@ namespace storm { bool standardCompliant; /// If set, the model is transformed into a single automaton - bool exportFlattened; + bool flatten; /// If given, the model will get this name boost::optional modelName; + /// If not set, arrays in the model are eliminated + bool allowArrays; + + /// if not set, functions in the model are eliminated + bool allowFunctions; + }; } } diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.cpp b/src/storm-conv/settings/modules/ConversionInputSettings.cpp index cc91d597c..090efe901 100644 --- a/src/storm-conv/settings/modules/ConversionInputSettings.cpp +++ b/src/storm-conv/settings/modules/ConversionInputSettings.cpp @@ -20,6 +20,7 @@ namespace storm { const std::string ConversionInputSettings::prismInputOptionName = "prism"; const std::string ConversionInputSettings::prismCompatibilityOptionName = "prismcompat"; const std::string ConversionInputSettings::prismCompatibilityOptionShortName = "pc"; + const std::string ConversionInputSettings::janiInputOptionName = "jani"; ConversionInputSettings::ConversionInputSettings() : ModuleSettings(moduleName) { @@ -27,10 +28,12 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build()) .build()); - this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + ").").setShortName(constantsOptionShortName) + this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (e.g., via --" + prismInputOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); } @@ -42,6 +45,14 @@ namespace storm { return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString(); } + bool ConversionInputSettings::isJaniInputSet() const { + return this->getOption(janiInputOptionName).getHasOptionBeenSet(); + } + + std::string ConversionInputSettings::getJaniInputFilename() const { + return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString(); + } + bool ConversionInputSettings::isPrismCompatibilityEnabled() const { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.h b/src/storm-conv/settings/modules/ConversionInputSettings.h index 41cf6549e..27e0b4795 100644 --- a/src/storm-conv/settings/modules/ConversionInputSettings.h +++ b/src/storm-conv/settings/modules/ConversionInputSettings.h @@ -63,6 +63,16 @@ namespace storm { */ bool isPrismCompatibilityEnabled() const; + /*! + * Retrieves whether the Jani option was set. + */ + bool isJaniInputSet() const; + + /*! + * Retrieves the name of the file that contains the jani model specification if the model was given. + */ + std::string getJaniInputFilename() const; + bool check() const override; void finalize() override; @@ -78,6 +88,7 @@ namespace storm { static const std::string prismInputOptionName; static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; + static const std::string janiInputOptionName; }; diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp index 707e91dac..37fb525ab 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.cpp +++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp @@ -20,6 +20,8 @@ namespace storm { const std::string JaniExportSettings::locationVariablesOptionName = "location-variables"; const std::string JaniExportSettings::globalVariablesOptionName = "globalvars"; const std::string JaniExportSettings::compactJsonOptionName = "compactjson"; + const std::string JaniExportSettings::eliminateArraysOptionName = "eliminate-arrays"; + const std::string JaniExportSettings::eliminateFunctionsOptionName = "eliminate-functions"; JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) { @@ -28,6 +30,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build()); this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, eliminateArraysOptionName, false, "If set, transforms the model such that array variables/expressions are eliminated.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build()); } bool JaniExportSettings::isExportAsStandardJaniSet() const { @@ -66,6 +70,14 @@ namespace storm { return this->getOption(compactJsonOptionName).getHasOptionBeenSet(); } + bool JaniExportSettings::isEliminateArraysSet() const { + return this->getOption(eliminateArraysOptionName).getHasOptionBeenSet(); + } + + bool JaniExportSettings::isEliminateFunctionsSet() const { + return this->getOption(eliminateFunctionsOptionName).getHasOptionBeenSet(); + } + void JaniExportSettings::finalize() { } diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h index 99e00ea9b..985eabe4a 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.h +++ b/src/storm-conv/settings/modules/JaniExportSettings.h @@ -23,6 +23,10 @@ namespace storm { bool isGlobalVarsSet() const; bool isCompactJsonSet() const; + + bool isEliminateArraysSet() const; + + bool isEliminateFunctionsSet() const; std::vector> getLocationVariables() const; @@ -38,6 +42,8 @@ namespace storm { static const std::string locationVariablesOptionName; static const std::string globalVariablesOptionName; static const std::string compactJsonOptionName; + static const std::string eliminateArraysOptionName; + static const std::string eliminateFunctionsOptionName; }; } diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index 63da78250..e9f23fe48 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/src/storm-gspn/api/storm-gspn.cpp @@ -66,12 +66,13 @@ namespace storm { storm::builder::JaniGSPNBuilder builder(gspn); storm::jani::Model* model = builder.build("gspn_automaton", exportSettings.isAddJaniPropertiesSet()); - storm::api::postprocessJani(*model, options); - auto properties = janiProperyGetter(builder); if (exportSettings.isAddJaniPropertiesSet()) { properties.insert(properties.end(), builder.getStandardProperties().begin(), builder.getStandardProperties().end()); } + + storm::api::transformJani(*model, properties, options); + storm::api::exportJaniToFile(*model, properties, exportSettings.getWriteToJaniFilename(), jani.isCompactJsonSet()); delete model; } diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index fe4585023..2c81dc945 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -41,7 +41,7 @@ void initializeSettings() { void handleJani(storm::jani::Model& model) { auto const& jani = storm::settings::getModule(); storm::converter::JaniConversionOptions options(jani); - storm::api::postprocessJani(model, options); + storm::api::transformJani(model, {}, options); if (storm::settings::getModule().isToJaniSet()) { storm::api::exportJaniToFile(model, {}, storm::settings::getModule().getWriteToJaniFilename(), jani.isCompactJsonSet()); } else { diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index c326e7314..c59eb5a34 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -959,8 +959,11 @@ namespace storm { return arrayEliminator.eliminate(*this, keepNonTrivialArrayAccess); } - void Model::eliminateArrays() { - eliminateArrays(false); + void Model::eliminateArrays(std::vector& properties) { + auto data = eliminateArrays(false); + for (auto& p : properties) { + data.transformProperty(p); + } } void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) { diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 3224c0353..6bce3603d 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -35,6 +35,7 @@ namespace storm { class Exporter; class SynchronizationVector; class ArrayEliminatorData; + class Property; class Model { public: @@ -380,7 +381,12 @@ namespace storm { * @return data from the elimination. If non-trivial array accesses are kept, pointers to remaining array variables point to this data. */ ArrayEliminatorData eliminateArrays(bool keepNonTrivialArrayAccess); - void eliminateArrays(); + + /*! + * Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables. + * @param properties also eliminates array expressions in the given properties + */ + void eliminateArrays(std::vector& properties); /*! * Retrieves whether there is an expression restricting the legal initial values of the global variables.