From 8fc0033bb223dc79ef0e437a877987132e071f2d Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 6 Feb 2017 19:33:23 +0100 Subject: [PATCH] fix dft-to-gspn regarding properties, now compiles again, and changed settings: Properties are now in IOSettings (should not change usage) --- src/storm-dft-cli/storm-dyftee.cpp | 11 +++--- src/storm-gspn-cli/storm-gspn.cpp | 4 +-- src/storm/cli/cli.cpp | 14 ++++---- .../settings/modules/GeneralSettings.cpp | 18 ---------- src/storm/settings/modules/GeneralSettings.h | 23 ------------- src/storm/settings/modules/IOSettings.cpp | 19 ++++++++++- src/storm/settings/modules/IOSettings.h | 34 +++++++++++++++++-- 7 files changed, 65 insertions(+), 58 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index fdc4a4d5e..308037d77 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -127,6 +127,7 @@ int main(const int argc, const char** argv) { storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule(); + storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } @@ -147,9 +148,9 @@ int main(const int argc, const char** argv) { uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); storm::handleGSPNExportSettings(*gspn); - - std::shared_ptr exprManager(new storm::expressions::ExpressionManager()); - storm::builder::JaniGSPNBuilder builder(*gspn, exprManager); + + std::shared_ptr const& exprManager = gspn->getExpressionManager(); + storm::builder::JaniGSPNBuilder builder(*gspn); storm::jani::Model* model = builder.build(); storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); @@ -203,9 +204,9 @@ int main(const int argc, const char** argv) { std::string operatorType = ""; std::string targetFormula = ""; - if (generalSettings.isPropertySet()) { + if (ioSettings.isPropertySet()) { STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - pctlFormula = generalSettings.getProperty(); + pctlFormula = ioSettings.getProperty(); } else if (dftSettings.usePropExpectedTime()) { STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); operatorType = "T"; diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index b01824c50..5ea31f30c 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -92,8 +92,8 @@ int main(const int argc, const char **argv) { auto gspn = parser.parse(storm::settings::getModule().getGspnFilename()); std::string formulaString = ""; - if (!storm::settings::getModule().isPropertySet()) { - formulaString = storm::settings::getModule().getProperty(); + if (!storm::settings::getModule().isPropertySet()) { + formulaString = storm::settings::getModule().getProperty(); } boost::optional> propertyFilter; storm::parser::FormulaParser formulaParser(gspn->getExpressionManager()); diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index a8e02dd46..c5fb7ef8b 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -198,9 +198,9 @@ namespace storm { } boost::optional> propertyFilter; - std::string propertyFilterString = storm::settings::getModule().getPropertyFilter(); + std::string propertyFilterString = storm::settings::getModule().getPropertyFilter(); if (propertyFilterString != "all") { - propertyFilter = storm::parsePropertyFilter(storm::settings::getModule().getPropertyFilter()); + propertyFilter = storm::parsePropertyFilter(storm::settings::getModule().getPropertyFilter()); } auto coreSettings = storm::settings::getModule(); @@ -245,9 +245,9 @@ namespace storm { // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. STORM_LOG_TRACE("Parsing properties."); - if (generalSettings.isPropertySet()) { + if (ioSettings.isPropertySet()) { if (model.isJaniModel()) { - properties = storm::parsePropertiesForJaniModel(generalSettings.getProperty(), model.asJaniModel(), propertyFilter); + properties = storm::parsePropertiesForJaniModel(ioSettings.getProperty(), model.asJaniModel(), propertyFilter); if (labelRenaming) { std::vector amendedProperties; @@ -257,7 +257,7 @@ namespace storm { properties = std::move(amendedProperties); } } else { - properties = storm::parsePropertiesForPrismProgram(generalSettings.getProperty(), model.asPrismProgram(), propertyFilter); + properties = storm::parsePropertiesForPrismProgram(ioSettings.getProperty(), model.asPrismProgram(), propertyFilter); } constantDefinitions = model.parseConstantDefinitions(constantDefinitionString); @@ -297,8 +297,8 @@ namespace storm { // If the model is given in an explicit format, we parse the properties without allowing expressions // in formulas. std::vector properties; - if (generalSettings.isPropertySet()) { - properties = storm::parsePropertiesForExplicit(generalSettings.getProperty(), propertyFilter); + if (ioSettings.isPropertySet()) { + properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter); } buildAndCheckExplicitModel(properties, true); diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp index 373d20175..036eadeaa 100644 --- a/src/storm/settings/modules/GeneralSettings.cpp +++ b/src/storm/settings/modules/GeneralSettings.cpp @@ -26,8 +26,6 @@ namespace storm { const std::string GeneralSettings::precisionOptionShortName = "eps"; const std::string GeneralSettings::configOptionName = "config"; const std::string GeneralSettings::configOptionShortName = "c"; - const std::string GeneralSettings::propertyOptionName = "prop"; - const std::string GeneralSettings::propertyOptionShortName = "prop"; const std::string GeneralSettings::bisimulationOptionName = "bisimulation"; const std::string GeneralSettings::bisimulationOptionShortName = "bisim"; const std::string GeneralSettings::parametricOptionName = "parametric"; @@ -43,11 +41,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - - this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) - .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, parametricRegionOptionName, false, "Sets whether to use the parametric Region engine.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").build()); @@ -81,18 +74,7 @@ namespace storm { std::string GeneralSettings::getConfigFilename() const { return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString(); } - - bool GeneralSettings::isPropertySet() const { - return this->getOption(propertyOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getProperty() const { - return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString(); - } - std::string GeneralSettings::getPropertyFilter() const { - return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); - } bool GeneralSettings::isBisimulationSet() const { return this->getOption(bisimulationOptionName).getHasOptionBeenSet(); diff --git a/src/storm/settings/modules/GeneralSettings.h b/src/storm/settings/modules/GeneralSettings.h index 23ccfef2f..cac1c7ea0 100644 --- a/src/storm/settings/modules/GeneralSettings.h +++ b/src/storm/settings/modules/GeneralSettings.h @@ -70,27 +70,6 @@ namespace storm { * @return The name of the file that is to be scanned for settings. */ std::string getConfigFilename() const; - - /*! - * Retrieves whether the property option was set. - * - * @return True if the property option was set. - */ - bool isPropertySet() const; - - /*! - * Retrieves the property specified with the property option. - * - * @return The property specified with the property option. - */ - std::string getProperty() const; - - /*! - * Retrieves the property filter. - * - * @return The property filter. - */ - std::string getPropertyFilter() const; /*! * Retrieves whether the option to perform bisimulation minimization is set. @@ -146,8 +125,6 @@ namespace storm { static const std::string precisionOptionShortName; static const std::string configOptionName; static const std::string configOptionShortName; - static const std::string propertyOptionName; - static const std::string propertyOptionShortName; static const std::string bisimulationOptionName; static const std::string bisimulationOptionShortName; static const std::string parametricOptionName; diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index bf8055c31..9f07c0219 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -40,6 +40,8 @@ namespace storm { const std::string IOSettings::fullModelBuildOptionName = "buildfull"; const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; + const std::string IOSettings::propertyOptionName = "prop"; + const std::string IOSettings::propertyOptionShortName = "prop"; IOSettings::IOSettings() : ModuleSettings(moduleName) { @@ -59,7 +61,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); - + this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) + .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()); std::vector explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); @@ -207,6 +212,18 @@ namespace storm { return this->getOption(noBuildOptionName).getHasOptionBeenSet(); } + bool IOSettings::isPropertySet() const { + return this->getOption(propertyOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getProperty() const { + return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString(); + } + + std::string IOSettings::getPropertyFilter() const { + return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); + } + void IOSettings::finalize() { } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 3c34f94f7..711ec2d97 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -211,11 +211,39 @@ namespace storm { * @return The string that defines the constants of a symbolic model. */ std::string getConstantDefinitionString() const; - + + /*! + * Retrieves whether the jani-property option was set + * @return + */ bool isJaniPropertiesSet() const; - + + /*! + * @return The names of the jani properties to check + */ std::vector getJaniProperties() const; + /*! + * Retrieves whether the property option was set. + * + * @return True if the property option was set. + */ + bool isPropertySet() const; + + /*! + * Retrieves the property specified with the property option. + * + * @return The property specified with the property option. + */ + std::string getProperty() const; + + /*! + * Retrieves the property filter. + * + * @return The property filter. + */ + std::string getPropertyFilter() const; + /*! * Retrieves whether the PRISM compatibility mode was enabled. * @@ -266,6 +294,8 @@ namespace storm { static const std::string noBuildOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; + static const std::string propertyOptionName; + static const std::string propertyOptionShortName; }; } // namespace modules