formula parser now directly emits properties with names; name filtering of properties from cli

src/storm/cli/cli.cpp

@@ -221,6 +221,12 @@ namespace storm {
                 storm::utility::initializeFileLogging();
             }
 
+            boost::optional<std::set<std::string>> propertyFilter;
+            std::string propertyFilterString = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter();
+            if (propertyFilterString != "all") {
+                propertyFilter = storm::parsePropertyFilter(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter());
+            }
+            
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             if (ioSettings.isPrismOrJaniInputSet()) {
                 storm::storage::SymbolicModelDescription model;
@@ -244,29 +250,21 @@ 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.");
-                uint64_t i = 0;
-
                 // Get the string that assigns values to the unknown currently undefined constants in the model and formula.
                 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
                 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
 
+                // 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 (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
-                    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
                     if (model.isJaniModel()) {
-                        formulas = storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel());
+                        properties = storm::parsePropertiesForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel(), propertyFilter);
                     } else {
-                        formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram());
+                        properties = storm::parsePropertiesForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram(), propertyFilter);
                     }
                     
                     constantDefinitions = model.parseConstantDefinitions(constantDefinitionString);
-                    formulas = substituteConstantsInFormulas(formulas, constantDefinitions);
-
-                    for (auto const& formula : formulas) {
-                        properties.emplace_back(std::to_string(i), formula);
-                        ++i;
-                    }
+                    properties = substituteConstantsInProperties(properties, constantDefinitions);
                 } else {
                     constantDefinitions = model.parseConstantDefinitions(constantDefinitionString);
                 }
@@ -303,12 +301,7 @@ namespace storm {
                 // in formulas.
                 std::vector<storm::jani::Property> properties;
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
-                    uint64_t i = 0;
-                    for(auto const& formula : storm::parseFormulasForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty())) {
-                        properties.emplace_back(std::to_string(i), formula);
-                        ++i;
-                        
-                    }
+                    properties = storm::parsePropertiesForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), propertyFilter);
                 }
 
                 buildAndCheckExplicitModel<double>(properties, true);

src/storm/cli/entrypoints.h

@@ -267,7 +267,7 @@ namespace storm {
         template<storm::dd::DdType LibraryType>
         void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
             // Start by building the model.
-            auto markovModel = buildSymbolicModel<double, LibraryType>(model, formulasInProperties(properties));
+            auto markovModel = buildSymbolicModel<double, LibraryType>(model, extractFormulasFromProperties(properties));
             
             // Print some information about the model.
             markovModel->printModelInformationToStream(std::cout);
@@ -282,7 +282,7 @@ namespace storm {
         
         template<typename ValueType>
         void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
-            auto formulas = formulasInProperties(properties);
+            auto formulas = extractFormulasFromProperties(properties);
             // Start by building the model.
             std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas);
 
@@ -362,7 +362,7 @@ namespace storm {
             std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional<std::string>(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional<std::string>(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional<std::string>(settings.getChoiceLabelingFilename()) : boost::none);
             
             // Preprocess the model if needed.
-            BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulasInProperties(properties));
+            BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties));
 
             // Print some information about the model.
             model->printModelInformationToStream(std::cout);

src/storm/parser/FormulaParser.cpp

@@ -7,6 +7,8 @@
 #include "storm/storage/prism/Program.h"
 #include "storm/storage/jani/Model.h"
 
+#include "storm/logic/Formulas.h"
+
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "storm/exceptions/WrongFormatException.h"
 
@@ -48,22 +50,22 @@ namespace storm {
         }
         
         std::shared_ptr<storm::logic::Formula const> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const {
-            std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = parseFromString(formulaString);
-            STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead.");
-            return formulas.front();
+            std::vector<storm::jani::Property> property = parseFromString(formulaString);
+            STORM_LOG_THROW(property.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << property.size() << " instead.");
+            return property.front().getRawFormula();
         }
         
-        std::vector<std::shared_ptr<storm::logic::Formula const>> FormulaParser::parseFromFile(std::string const& filename) const {
+        std::vector<storm::jani::Property> FormulaParser::parseFromFile(std::string const& filename) const {
             // Open file and initialize result.
             std::ifstream inputFileStream(filename, std::ios::in);
             STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
             
-            std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+            std::vector<storm::jani::Property> properties;
             
             // Now try to parse the contents of the file.
             try {
                 std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
-                formulas = parseFromString(fileContent);
+                properties = parseFromString(fileContent);
             } catch(std::exception& e) {
                 // In case of an exception properly close the file before passing exception.
                 inputFileStream.close();
@@ -72,16 +74,16 @@ namespace storm {
             
             // Close the stream in case everything went smoothly and return result.
             inputFileStream.close();
-            return formulas;
+            return properties;
         }
         
-        std::vector<std::shared_ptr<storm::logic::Formula const>> FormulaParser::parseFromString(std::string const& formulaString) const {
+        std::vector<storm::jani::Property> FormulaParser::parseFromString(std::string const& formulaString) const {
             PositionIteratorType first(formulaString.begin());
             PositionIteratorType iter = first;
             PositionIteratorType last(formulaString.end());
             
             // Create empty result;
-            std::vector<std::shared_ptr<storm::logic::Formula const>> result;
+            std::vector<storm::jani::Property> result;
             
             // Create grammar.
             try {

src/storm/parser/FormulaParser.h

@@ -5,7 +5,7 @@
 
 #include "storm/parser/SpiritParserDefinitions.h"
 #include "storm/parser/ExpressionParser.h"
-#include "storm/logic/Formulas.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/storage/expressions/Expression.h"
 #include "storm/utility/macros.h"
 
@@ -14,6 +14,10 @@ namespace storm {
         class Program;
     }
     
+    namespace logic {
+        class Formula;
+    }
+    
     namespace parser {
         
         // Forward-declare grammar.
@@ -38,20 +42,20 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula const> parseSingleFormulaFromString(std::string const& formulaString) const;
             
             /*!
-             * Parses the formula given by the provided string.
+             * Parses the property given by the provided string.
              *
-             * @param formulaString The formula as a string.
-             * @return The contained formulas.
+             * @param propertyString The formula as a string.
+             * @return The contained properties.
              */
-            std::vector<std::shared_ptr<storm::logic::Formula const>> parseFromString(std::string const& formulaString) const;
+            std::vector<storm::jani::Property> parseFromString(std::string const& propertyString) const;
             
             /*!
-             * Parses the formulas in the given file.
+             * Parses the properties in the given file.
              *
              * @param filename The name of the file to parse.
-             * @return The contained formulas.
+             * @return The contained properties.
              */
-            std::vector<std::shared_ptr<storm::logic::Formula const>> parseFromFile(std::string const& filename) const;
+            std::vector<storm::jani::Property> parseFromFile(std::string const& filename) const;
             
             /*!
              * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used

src/storm/parser/FormulaParserGrammar.cpp

@@ -4,11 +4,11 @@
 namespace storm {
     namespace parser {
         
-        FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(nullptr), expressionParser(*manager, keywords_, true, true) {
+        FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(nullptr), expressionParser(*manager, keywords_, true, true), propertyCount(0) {
             initialize();
         }
 
-        FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager> const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(manager), expressionParser(*manager, keywords_, true, true) {
+        FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager> const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(manager), expressionParser(*manager, keywords_, true, true), propertyCount(0) {
             initialize();
         }
 
@@ -116,10 +116,13 @@ namespace storm {
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]];
             identifier.name("identifier");
             
+            formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
+            formulaName.name("formula name");
+            
             constantDefinition = (qi::lit("const") > qi::eps[qi::_a = true] > -(qi::lit("int") | qi::lit("double")[qi::_a = false]) >> identifier)[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a)];
             constantDefinition.name("constant definition");
             
-            start = qi::eps > ((stateFormula[phoenix::push_back(qi::_val, qi::_1)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
+            start = qi::eps > (((-formulaName >> stateFormula)[phoenix::bind(&FormulaParserGrammar::addProperty, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
             start.name("start");
             
             // Enable the following lines to print debug output for most the rules.
@@ -193,6 +196,15 @@ namespace storm {
             addIdentifierExpression(name, newVariable);
         }
         
+        void FormulaParserGrammar::addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula) {
+            if (name) {
+                properties.emplace_back(name.get(), formula);
+            } else {
+                properties.emplace_back(std::to_string(propertyCount), formula);
+            }
+            ++propertyCount;
+        }
+        
         bool FormulaParserGrammar::areConstantDefinitionsAllowed() const {
             return static_cast<bool>(manager);
         }

src/storm/parser/FormulaParserGrammar.h

@@ -5,6 +5,7 @@
 
 #include "storm/parser/SpiritErrorHandler.h"
 #include "storm/exceptions/WrongFormatException.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/logic/Formulas.h"
 #include "storm/parser/ExpressionParser.h"
 
@@ -17,7 +18,7 @@ namespace storm {
     
     namespace parser {
         
-        class FormulaParserGrammar : public qi::grammar<Iterator, std::vector<std::shared_ptr<storm::logic::Formula const>>(), Skipper> {
+        class FormulaParserGrammar : public qi::grammar<Iterator, std::vector<storm::jani::Property>(), Skipper> {
         public:
             FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
             FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager> const& manager);
@@ -121,10 +122,11 @@ namespace storm {
             // they are to be replaced with.
             qi::symbols<char, storm::expressions::Expression> identifiers_;
             
-            qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula const>>(), Skipper> start;
+            qi::rule<Iterator, std::vector<storm::jani::Property>(), Skipper> start;
             
             qi::rule<Iterator, qi::unused_type(), qi::locals<bool>, Skipper> constantDefinition;
             qi::rule<Iterator, std::string(), Skipper> identifier;
+            qi::rule<Iterator, std::string(), Skipper> formulaName;
             
             qi::rule<Iterator, storm::logic::OperatorInformation(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<storm::expressions::Expression>>, Skipper> operatorInformation;
             qi::rule<Iterator, storm::logic::RewardMeasureType(), Skipper> rewardMeasureType;
@@ -171,6 +173,7 @@ namespace storm {
 
             bool areConstantDefinitionsAllowed() const;
             void addConstant(std::string const& name, bool integer);
+            void addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula);
             
             std::pair<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const;
             std::pair<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const;
@@ -199,6 +202,8 @@ namespace storm {
             
             // An error handler function.
             phoenix::function<SpiritErrorHandler> handler;
+            
+            uint64_t propertyCount;
         };
 
     }

src/storm/settings/modules/GeneralSettings.cpp

@@ -44,8 +44,10 @@ namespace storm {
                 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 formulas to be checked on the model.").setShortName(propertyOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula or filename", "The formula or the file containing the formulas.").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());
@@ -85,9 +87,13 @@ namespace storm {
             }
             
             std::string GeneralSettings::getProperty() const {
-                return this->getOption(propertyOptionName).getArgumentByName("formula or filename").getValueAsString();
+                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();
             }

src/storm/settings/modules/GeneralSettings.h

@@ -85,6 +85,13 @@ namespace storm {
                  */
                 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.
                  *

src/storm/storage/jani/Property.cpp

@@ -28,10 +28,18 @@ namespace storm {
             return this->comment;
         }
         
+        Property Property::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+            return Property(name, filterExpression.substitute(substitution), comment);
+        }
+        
         FilterExpression const& Property::getFilter() const {
             return this->filterExpression;
         }
         
+        std::shared_ptr<storm::logic::Formula const> Property::getRawFormula() const {
+            return this->filterExpression.getFormula();
+        }
+        
         std::ostream& operator<<(std::ostream& os, Property const& p) {
             return os << "(" << p.getName() << ") : " << p.getFilter();
         }

src/storm/storage/jani/Property.h

@@ -28,19 +28,23 @@ namespace storm {
         
         class FilterExpression {
         public:
-            explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : values(formula), ft(ft) {}
+            explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
             
             
             std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
-                return values;
+                return formula;
             }
             
             storm::modelchecker::FilterType getFilterType() const {
                 return ft;
             }
+            
+            FilterExpression substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+                return FilterExpression(formula->substitute(substitution), ft);
+            }
         private:
             // For now, we assume that the states are always the initial states.
-            std::shared_ptr<storm::logic::Formula const> values;
+            std::shared_ptr<storm::logic::Formula const> formula;
             storm::modelchecker::FilterType ft;
         };
         
@@ -58,6 +62,7 @@ namespace storm {
              * @param comment An optional comment
              */
             Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment = "");
+            
             /**
              * Constructs the property
              * @param name the name
@@ -65,18 +70,24 @@ namespace storm {
              * @param comment An optional comment
              */
             Property(std::string const& name, FilterExpression const& fe, std::string const& comment = "");
+            
             /**
              * Get the provided name
              * @return the name
              */
             std::string const& getName() const;
+            
             /**
              * Get the provided comment, if any
              * @return the comment
              */
             std::string const& getComment() const;
             
+            Property substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+            
             FilterExpression const& getFilter() const;
+            
+            std::shared_ptr<storm::logic::Formula const> getRawFormula() const;
         private:
             std::string name;
             std::string comment;

src/storm/utility/cli.cpp

@@ -59,6 +59,17 @@ namespace storm {
                 
                 return constantDefinitions;
             }
+         
+            std::vector<std::string> parseCommaSeparatedStrings(std::string const& input) {
+                std::vector<std::string> result;
+                if (!input.empty()) {
+                    boost::split(result, input, boost::is_any_of(","));
+                    for (auto& entry : result) {
+                        boost::trim(entry);
+                    }
+                }
+                return result;
+            }
             
         }
     }

src/storm/utility/cli.h

@@ -11,6 +11,7 @@ namespace storm {
         
             std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, std::string const& constantDefinitionString);
             
+            std::vector<std::string> parseCommaSeparatedStrings(std::string const& input);
         }
     }
 }

src/storm/utility/storm.cpp

@@ -10,11 +10,10 @@
 
 namespace storm{
     
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulasInProperties(std::vector<storm::jani::Property> const& properties) {
-        
+    std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties) {
         std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
         for (auto const& prop : properties) {
-            formulas.push_back(prop.getFilter().getFormula());
+            formulas.push_back(prop.getRawFormula());
         }
         return formulas;
     }
@@ -42,45 +41,72 @@ namespace storm{
         }
     }
 
-    /**
-     * Helper
-     * @param FormulaParser
-     * @return The formulas.
-     */
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulas(storm::parser::FormulaParser& formulaParser, std::string const& inputString) {
+    std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none) {
         // If the given property looks like a file (containing a dot and there exists a file with that name),
         // we try to parse it as a file, otherwise we assume it's a property.
+        std::vector<storm::jani::Property> properties;
         if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) {
-            return formulaParser.parseFromFile(inputString);
+            properties = formulaParser.parseFromFile(inputString);
         } else {
-            return formulaParser.parseFromString(inputString);
+            properties = formulaParser.parseFromString(inputString);
         }
+        
+        return filterProperties(properties, propertyFilter);
     }
 
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString) {
+    std::vector<storm::jani::Property> parsePropertiesForExplicit(std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter) {
         auto exprManager = std::make_shared<storm::expressions::ExpressionManager>();
         storm::parser::FormulaParser formulaParser(exprManager);
-        return parseFormulas(formulaParser, inputString);
+        return parseProperties(formulaParser, inputString, propertyFilter);
     }
 
-    std::vector<std::shared_ptr<storm::logic::Formula const>> substituteConstantsInFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-        std::vector<std::shared_ptr<storm::logic::Formula const>> preprocessedFormulas;
-        
-        for (auto const& formula : formulas) {
-            preprocessedFormulas.emplace_back(formula->substitute(substitution));
+    std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+        std::vector<storm::jani::Property> preprocessedProperties;
+        for (auto const& property : properties) {
+            preprocessedProperties.emplace_back(property.substitute(substitution));
         }
-        return preprocessedFormulas;
+        return preprocessedProperties;
     }
     
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model) {
+    std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional<std::set<std::string>> const& propertyFilter) {
         storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer());
-        auto formulas = parseFormulas(formulaParser, inputString);
-        return substituteConstantsInFormulas(formulas, model.getConstantsSubstitution());
+        auto formulas = parseProperties(formulaParser, inputString, propertyFilter);
+        return substituteConstantsInProperties(formulas, model.getConstantsSubstitution());
     }
     
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program) {
+    std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> const& propertyFilter) {
         storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-        auto formulas = parseFormulas(formulaParser, inputString);
-        return substituteConstantsInFormulas(formulas, program.getConstantsSubstitution());
-    } 
+        auto formulas = parseProperties(formulaParser, inputString, propertyFilter);
+        return substituteConstantsInProperties(formulas, program.getConstantsSubstitution());
+    }
+    
+    boost::optional<std::set<std::string>> parsePropertyFilter(boost::optional<std::string> const& propertyFilter) {
+        std::vector<std::string> propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter.get());
+        std::set<std::string> propertyNameSet(propertyNames.begin(), propertyNames.end());
+        return propertyNameSet;
+    }
+    
+    std::vector<storm::jani::Property> filterProperties(std::vector<storm::jani::Property> const& properties, boost::optional<std::set<std::string>> const& propertyFilter) {
+        if (propertyFilter) {
+            std::set<std::string> const& propertyNameSet = propertyFilter.get();
+            std::vector<storm::jani::Property> result;
+            std::set<std::string> reducedPropertyNames;
+            for (auto const& property : properties) {
+                if (propertyNameSet.find(property.getName()) != propertyNameSet.end()) {
+                    result.push_back(property);
+                    reducedPropertyNames.insert(property.getName());
+                }
+            }
+            
+            if (reducedPropertyNames.size() < propertyNameSet.size()) {
+                std::set<std::string> missingProperties;
+                std::set_difference(propertyNameSet.begin(), propertyNameSet.end(), reducedPropertyNames.begin(), reducedPropertyNames.end(), std::inserter(missingProperties, missingProperties.begin()));
+                STORM_LOG_WARN("Filtering unknown properties " << boost::join(missingProperties, ", ") << ".");
+            }
+            
+            return result;
+        } else {
+            return properties;
+        }
+    }
 }

src/storm/utility/storm.h

@@ -105,13 +105,15 @@ namespace storm {
         return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
     }
 
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulasInProperties(std::vector<storm::jani::Property> const& properties);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties);
     std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path);
     storm::prism::Program parseProgram(std::string const& path);
-    std::vector<std::shared_ptr<storm::logic::Formula const>> substituteConstantsInFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString);
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program);
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model);
+    std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+    std::vector<storm::jani::Property> parsePropertiesForExplicit(std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
+    std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
+    std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
+    boost::optional<std::set<std::string>> parsePropertyFilter(boost::optional<std::string> const& propertyFilter);
+    std::vector<storm::jani::Property> filterProperties(std::vector<storm::jani::Property> const& properties, boost::optional<std::set<std::string>> const& propertyFilter);
 
     template<typename ValueType>
     std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
@@ -466,7 +468,7 @@ namespace storm {
         // Program and formula
         storm::prism::Program program = parseProgram(programFilePath);
         program = storm::utility::prism::preprocess(program, constantsString);
-        std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = parseFormulasForPrismProgram(formulaString, program);
+        std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = extractFormulasFromProperties(parsePropertiesForPrismProgram(formulaString, program));
         if(formulas.size()!=1) {
             STORM_LOG_ERROR("The given formulaString does not specify exactly one formula");
             return false;

src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp

@@ -24,7 +24,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -95,7 +95,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
     
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -184,7 +184,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
     carl::VariablePool::getInstance().clear();
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -228,7 +228,7 @@ TEST(SparseDtmcRegionModelCheckerTest, DISABLED_Brp_Rew_4Par) {
     carl::VariablePool::getInstance().clear();
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -292,7 +292,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
 
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -384,7 +384,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
     
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -450,7 +450,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
     
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());

src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp

@@ -23,7 +23,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
     carl::VariablePool::getInstance().clear();
 
     storm::prism::Program program = storm::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaFile, program);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program));
     std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -91,7 +91,7 @@ TEST(SparseMdpRegionModelCheckerTest, DISABLED_coin_Prob) {
     carl::VariablePool::getInstance().clear();
 
     storm::prism::Program program = storm::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());

src/test/parser/FormulaParserTest.cpp

@@ -154,11 +154,10 @@ TEST(FormulaParserTest, MultiObjectiveFormulaTest) {
     storm::parser::FormulaParser formulaParser;
     
     std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])";
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
-    ASSERT_NO_THROW(formulas = formulaParser.parseFromString(input));
-    ASSERT_EQ(1ull, formulas.size());
-    ASSERT_TRUE(formulas[0]->isMultiObjectiveFormula());
-    storm::logic::MultiObjectiveFormula mof = formulas[0]->asMultiObjectiveFormula();
+    std::shared_ptr<storm::logic::Formula const> formula;
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+    ASSERT_TRUE(formula->isMultiObjectiveFormula());
+    storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula();
     ASSERT_EQ(3ull, mof.getNumberOfSubformulas());
     
     ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula());

src/test/utility/ModelInstantiatorTest.cpp

@@ -26,7 +26,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     ASSERT_TRUE(formulas.size()==1);
     // Parametric model
     storm::generator::NextStateGeneratorOptions options(*formulas.front());
@@ -144,7 +144,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     ASSERT_TRUE(formulas.size()==1);
     // Parametric model
     storm::generator::NextStateGeneratorOptions options(*formulas.front());
@@ -214,7 +214,7 @@ TEST(ModelInstantiatorTest, Consensus) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     ASSERT_TRUE(formulas.size()==1);
     // Parametric model
     storm::generator::NextStateGeneratorOptions options(*formulas.front());