diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 737c80ba1..1229eef8f 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -65,27 +65,20 @@ namespace storm { input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule().isPrismCompatibilityEnabled()); } else { 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; - + boost::optional> propertyFilter; if (ioSettings.isJaniPropertiesSet()) { if (ioSettings.areJaniPropertiesSelected()) { - // Make sure to preserve the provided order - for (auto const& propName : ioSettings.getSelectedJaniProperties()) { - bool found = false; - for (auto const& property : janiPropertyInput) { - if (property.getName() == propName) { - input.properties.emplace_back(property); - found = true; - break; - } - } - STORM_LOG_THROW(found, storm::exceptions::InvalidArgumentException, "No JANI property with name '" << propName << "' is known."); - } + propertyFilter = ioSettings.getSelectedJaniProperties(); } else { - input.properties = janiPropertyInput; + propertyFilter = boost::none; } + } else { + propertyFilter = std::vector(); + } + auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), supportedFeatures, propertyFilter); + input.model = std::move(janiInput.first); + if (ioSettings.isJaniPropertiesSet()) { + input.properties = std::move(janiInput.second); } } } diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index 12d4a11d8..d60895eff 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -209,18 +209,31 @@ namespace storm { auto const& input = storm::settings::getModule(); - // Parse the jani model - auto janiModelProperties = storm::api::parseJaniModel(input.getJaniInputFilename(), storm::jani::getAllKnownModelFeatures()); - // 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(), janiModelProperties.first, propertyFilter); + // Parse the jani model and selected properties + boost::optional> janiPropertyFilter; + if (input.isJaniPropertiesSet()) { + if (input.areJaniPropertiesSelected()) { + janiPropertyFilter = input.getSelectedJaniProperties(); + } else { + janiPropertyFilter = boost::none; + } } else { - for (auto const& p : janiModelProperties.second) { - properties.push_back(p.second); + if (input.isPropertyInputSet()) { + janiPropertyFilter = std::vector(); + } else { + // If no properties are selected, take the ones from the jani file. + janiPropertyFilter = boost::none; } } + auto janiModelProperties = storm::api::parseJaniModel(input.getJaniInputFilename(), storm::jani::getAllKnownModelFeatures(), janiPropertyFilter); + + // Parse additional properties given from command line + std::vector properties = std::move(janiModelProperties.second); + if (input.isPropertyInputSet()) { + boost::optional> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter()); + auto additionalProperties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), janiModelProperties.first, propertyFilter); + properties.insert(properties.end(), additionalProperties.begin(), additionalProperties.end()); + } storm::storage::SymbolicModelDescription symbDescr(janiModelProperties.first); diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.cpp b/src/storm-conv/settings/modules/ConversionInputSettings.cpp index 090efe901..b1522ab4f 100644 --- a/src/storm-conv/settings/modules/ConversionInputSettings.cpp +++ b/src/storm-conv/settings/modules/ConversionInputSettings.cpp @@ -5,6 +5,7 @@ #include "storm/settings/OptionBuilder.h" #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" +#include "storm/parser/CSVParser.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -21,20 +22,30 @@ namespace storm { const std::string ConversionInputSettings::prismCompatibilityOptionName = "prismcompat"; const std::string ConversionInputSettings::prismCompatibilityOptionShortName = "pc"; const std::string ConversionInputSettings::janiInputOptionName = "jani"; - + const std::string ConversionInputSettings::janiPropertyOptionName = "janiproperty"; + const std::string ConversionInputSettings::janiPropertyOptionShortName = "jprop"; + ConversionInputSettings::ConversionInputSettings() : ModuleSettings(moduleName) { + // General 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, 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()); + + // Prism related 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, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + + // Jani related 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()); + this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build()); + } bool ConversionInputSettings::isPrismInputSet() const { @@ -77,6 +88,18 @@ namespace storm { return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); } + bool ConversionInputSettings::isJaniPropertiesSet() const { + return this->getOption(janiPropertyOptionName).getHasOptionBeenSet(); + } + + bool ConversionInputSettings::areJaniPropertiesSelected() const { + return this->getOption(janiPropertyOptionName).getHasOptionBeenSet() && (this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString() != ""); + } + + std::vector ConversionInputSettings::getSelectedJaniProperties() const { + return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString()); + } + void ConversionInputSettings::finalize() { // Intentionally left empty. } diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.h b/src/storm-conv/settings/modules/ConversionInputSettings.h index 27e0b4795..2ca110a20 100644 --- a/src/storm-conv/settings/modules/ConversionInputSettings.h +++ b/src/storm-conv/settings/modules/ConversionInputSettings.h @@ -31,7 +31,7 @@ namespace storm { */ std::string getPropertyInputFilter() const; - /*! + /*! * Retrieves whether constant definition option was set. * * @return True if the constant definition option was set. @@ -73,6 +73,25 @@ namespace storm { */ std::string getJaniInputFilename() const; + /*! + * Retrieves whether the jani-property option was set + * @return + */ + bool isJaniPropertiesSet() const; + + /*! + * Retrieves whether one or more jani-properties have been selected + * @return + */ + bool areJaniPropertiesSelected() const; + + /*! + * @return The names of the jani properties to check + */ + std::vector getSelectedJaniProperties() const; + + + bool check() const override; void finalize() override; @@ -89,6 +108,8 @@ namespace storm { static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; static const std::string janiInputOptionName; + static const std::string janiPropertyOptionName; + static const std::string janiPropertyOptionShortName; }; diff --git a/src/storm-parsers/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp index 1173651c0..983156279 100644 --- a/src/storm-parsers/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -35,8 +35,28 @@ namespace storm { return std::make_pair(std::move(parsedResult.first), std::move(propertyMap)); } - std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures) { - std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename); + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional> const& propertyFilter) { + + bool parseProperties = !propertyFilter.is_initialized() || !propertyFilter.get().empty(); + std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename, parseProperties); + + // eliminate unselected properties. + if (propertyFilter.is_initialized()) { + std::vector newProperties; + // Make sure to preserve the provided order + for (auto const& propName : propertyFilter.get()) { + bool found = false; + for (auto const& property : modelAndFormulae.second) { + if (property.getName() == propName) { + newProperties.push_back(std::move(property)); + found = true; + break; + } + } + STORM_LOG_ERROR_COND(found, "No JANI property with name '" << propName << "' is known."); + } + modelAndFormulae.second = std::move(newProperties); + } modelAndFormulae.first.checkValid(); auto nonEliminatedFeatures = modelAndFormulae.first.restrictToFeatures(allowedFeatures, modelAndFormulae.second); diff --git a/src/storm-parsers/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h index 32bf7aba9..8e45304c3 100644 --- a/src/storm-parsers/api/model_descriptions.h +++ b/src/storm-parsers/api/model_descriptions.h @@ -2,7 +2,8 @@ #include #include -#include +#include +#include namespace storm { namespace prism { @@ -10,6 +11,7 @@ namespace storm { } namespace jani { class Model; + class ModelFeatures; class Property; } @@ -18,6 +20,6 @@ namespace storm { storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false, bool simplify = true); std::pair> parseJaniModel(std::string const& filename); - std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures); + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional> const& propertyFilter = boost::none); } } diff --git a/src/storm-parsers/parser/ExpressionParser.cpp b/src/storm-parsers/parser/ExpressionParser.cpp index c5eff3de0..deaaa93bc 100644 --- a/src/storm-parsers/parser/ExpressionParser.cpp +++ b/src/storm-parsers/parser/ExpressionParser.cpp @@ -64,7 +64,7 @@ namespace storm { prefixPowerModuloExpression = ((prefixPowerModuloOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)] | ((qi::lit("func") >> qi::lit("(")) > prefixPowerModuloOperator_ > qi::lit(",") > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)]; } - prefixPowerModuloExpression.name("power/modulo expression"); + prefixPowerModuloExpression.name("(prefix) power/modulo expression"); identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionCreator::getIdentifierExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)]; identifierExpression.name("identifier expression"); @@ -86,7 +86,7 @@ namespace storm { } else { infixPowerModuloExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerModuloOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } - infixPowerModuloExpression.name("power/modulo expression"); + infixPowerModuloExpression.name("(infix) power/modulo expression"); if (allowBacktracking) { multiplicationExpression = infixPowerModuloExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerModuloExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index c7683ee4e..eba57d0dd 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -68,10 +68,10 @@ namespace storm { return static_cast(num); } - std::pair> JaniParser::parse(std::string const& path) { + std::pair> JaniParser::parse(std::string const& path, bool parseProperties) { JaniParser parser; parser.readFile(path); - return parser.parseModel(); + return parser.parseModel(parseProperties); } JaniParser::JaniParser(std::string const& jsonstring) { diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index 56174bd44..93e1a5790 100644 --- a/src/storm-parsers/parser/JaniParser.h +++ b/src/storm-parsers/parser/JaniParser.h @@ -44,7 +44,7 @@ namespace storm { JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); - static std::pair> parse(std::string const& path); + static std::pair> parse(std::string const& path, bool parseProperties = true); protected: void readFile(std::string const& path); diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 89408f9d3..c54758b12 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -133,7 +133,7 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { - return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); + return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); } template