Merge branch 'master' into janiTests

src/storm-cli-utilities/model-handling.h

@@ -65,27 +65,20 @@ namespace storm {
                     input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule<storm::settings::modules::BuildSettings>().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<std::vector<std::string>> 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<std::string>();
+                    }
+                    auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), supportedFeatures, propertyFilter);
+                    input.model = std::move(janiInput.first);
+                    if (ioSettings.isJaniPropertiesSet()) {
+                        input.properties = std::move(janiInput.second);
                     }
                 }
             }

src/storm-conv-cli/storm-conv.cpp

@@ -209,18 +209,31 @@ namespace storm {
 
             auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
 
-            // 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<storm::jani::Property> properties;
-            if (input.isPropertyInputSet()) {
-                boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter());
-                properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), janiModelProperties.first, propertyFilter);
+            // Parse the jani model and selected properties
+            boost::optional<std::vector<std::string>> 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<std::string>();
+                } 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<storm::jani::Property> properties = std::move(janiModelProperties.second);
+            if (input.isPropertyInputSet()) {
+                boost::optional<std::set<std::string>> 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);
             

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<std::string> ConversionInputSettings::getSelectedJaniProperties() const {
+                return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString());
+            }
+
 			void ConversionInputSettings::finalize() {
                 // Intentionally left empty.
             }

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<std::string> 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;
             };
             
                 

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<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures) {
-            std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(filename);
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional<std::vector<std::string>> const& propertyFilter) {
+            
+            bool parseProperties = !propertyFilter.is_initialized() || !propertyFilter.get().empty();
+            std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(filename, parseProperties);
+            
+            // eliminate unselected properties.
+            if (propertyFilter.is_initialized()) {
+                std::vector<storm::jani::Property> 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);

src/storm-parsers/api/model_descriptions.h

@@ -2,7 +2,8 @@
 
 #include <string>
 #include <map>
-#include <storm/storage/jani/ModelFeatures.h>
+#include <vector>
+#include <boost/optional.hpp>
 
 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<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename);
-        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures);
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional<std::vector<std::string>> const& propertyFilter = boost::none);
     }
 }

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)];

src/storm-parsers/parser/JaniParser.cpp

@@ -68,10 +68,10 @@ namespace storm {
             return static_cast<int64_t>(num);
         }
 
-        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parse(std::string const& path) {
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> 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) {

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<storm::jani::Model, std::vector<storm::jani::Property>> parse(std::string const& path);
+            static std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parse(std::string const& path, bool parseProperties = true);
 
         protected:
             void readFile(std::string const& path);

src/storm/storage/expressions/ToRationalNumberVisitor.cpp

@@ -133,7 +133,7 @@ namespace storm {
         
         template<typename RationalNumberType>
         boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IntegerLiteralExpression const& expression, boost::any const&) {
-            return RationalNumberType(carl::rationalize<storm::RationalNumber>(static_cast<carl::uint>(expression.getValue())));
+            return RationalNumberType(carl::rationalize<storm::RationalNumber>(static_cast<carl::sint>(expression.getValue())));
         }
         
         template<typename RationalNumberType>