allowing constant definitions for gspns via cli

src/storm-gspn-cli/storm-gspn.cpp

@@ -94,8 +94,13 @@ int main(const int argc, const char **argv) {
             return -1;
         }
         
+        std::string constantDefinitionString = "";
+        if (gspnSettings.isConstantsSet()) {
+            constantDefinitionString = gspnSettings.getConstantDefinitionString();
+        }
+        
         auto parser = storm::parser::GspnParser();
-        auto gspn = parser.parse(gspnSettings.getGspnFilename());
+        auto gspn = parser.parse(gspnSettings.getGspnFilename(), constantDefinitionString);
 
         std::string formulaString = "";
         if (storm::settings::getModule<storm::settings::modules::IOSettings>().isPropertySet()) {

src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp

@@ -23,8 +23,15 @@ namespace {
 namespace storm {
     namespace parser {
 
-        GreatSpnEditorProjectParser::GreatSpnEditorProjectParser() : manager(std::make_shared<storm::expressions::ExpressionManager>()), expressionParser(*manager) {
-            // Intentionally left empty
+        GreatSpnEditorProjectParser::GreatSpnEditorProjectParser(std::string const& constantDefinitionString) : manager(std::make_shared<storm::expressions::ExpressionManager>()), expressionParser(*manager) {
+            std::vector<std::string> constDefs;
+            boost::split( constDefs, constantDefinitionString, boost::is_any_of(","));
+            for (auto const& pair : constDefs) {
+                std::vector<std::string> keyvaluepair;
+                boost::split( keyvaluepair, pair, boost::is_any_of("="));
+                STORM_LOG_THROW(keyvaluepair.size() == 2, storm::exceptions::WrongFormatException, "Expected a constant definition of the form N=42 but got " << pair);
+                constantDefinitions.emplace(keyvaluepair.at(0), keyvaluepair.at(1));
+            }
         }
         
         storm::gspn::GSPN* GreatSpnEditorProjectParser::parse(xercesc::DOMElement const*  elementRoot) {
@@ -168,6 +175,8 @@ namespace storm {
                 } else if (name.compare("consttype") == 0) {
                     if (storm::adapters::XMLtoString(attr->getNodeValue()).compare("REAL") == 0) {
                         type = manager->getRationalType();
+                    } else if (storm::adapters::XMLtoString(attr->getNodeValue()).compare("INTEGER") == 0) {
+                        type = manager->getIntegerType();
                     } else {
                         STORM_PRINT_AND_LOG("Unknown consttype: " << storm::adapters::XMLtoString(attr->getNodeValue()) << std::endl);
                     }
@@ -182,10 +191,20 @@ namespace storm {
                 }
             }
             
+            STORM_LOG_THROW(constantDefinitions.count(identifier) == 0, storm::exceptions::NotSupportedException, "Multiple definitions of constant '" << identifier << "' were found.");
+            
             storm::expressions::Expression valueExpression;
+            if (valueStr == "") {
+                auto constDef = constantDefinitions.find(identifier);
+                STORM_LOG_THROW(constDef != constantDefinitions.end(), storm::exceptions::NotSupportedException, "Constant '" << identifier << "' has no value defined.");
+                valueStr = constDef->second;
+            }
             if (type.isRationalType()) {
                 expressionParser.setAcceptDoubleLiterals(true);
                 valueExpression = manager->rational(expressionParser.parseFromString(valueStr).evaluateAsRational());
+            } else if (type.isIntegerType()) {
+                expressionParser.setAcceptDoubleLiterals(false);
+                valueExpression = manager->integer(expressionParser.parseFromString(valueStr).evaluateAsInt());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unknown type of constant" << type << ".");
             }
@@ -257,7 +276,8 @@ namespace storm {
                 if (name.compare("name") == 0) {
                     placeName = storm::adapters::XMLtoString(attr->getNodeValue());
                 } else if (name.compare("marking") == 0) {
-                    initialTokens = std::stoull(storm::adapters::XMLtoString(attr->getNodeValue()));
+                    expressionParser.setAcceptDoubleLiterals(false);
+                    initialTokens = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsInt();
                 } else if (ignorePlaceAttribute(name)) {
                     // ignore node
                 } else {
@@ -388,7 +408,8 @@ namespace storm {
                 } else if (name.compare("kind") == 0) {
                     kind = storm::adapters::XMLtoString(attr->getNodeValue());
                 } else if (name.compare("mult") == 0) {
-                    mult = std::stoull(storm::adapters::XMLtoString(attr->getNodeValue()));
+                    expressionParser.setAcceptDoubleLiterals(false);
+                    mult = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsInt();
                 } else if (ignoreArcAttribute(name)) {
                     // ignore node
                 } else {

src/storm-gspn/parser/GreatSpnEditorProjectParser.h

@@ -20,7 +20,7 @@ namespace storm {
             
         public:
             
-            GreatSpnEditorProjectParser();
+            GreatSpnEditorProjectParser(std::string const& constantDefinitionString);
             
             /*!
              * Parses the given file into the GSPN.
@@ -46,7 +46,7 @@ namespace storm {
             storm::gspn::GspnBuilder builder;
             std::shared_ptr<storm::expressions::ExpressionManager> manager;
             storm::parser::ExpressionParser expressionParser;
-
+            std::unordered_map<std::string, std::string> constantDefinitions;
         };
     }
 }

src/storm-gspn/parser/GspnParser.cpp

@@ -12,7 +12,7 @@
 namespace storm {
     namespace parser {
         
-        storm::gspn::GSPN* GspnParser::parse(std::string const& filename) {
+        storm::gspn::GSPN* GspnParser::parse(std::string const& filename, std::string const& constantDefinitions) {
 #ifdef STORM_HAVE_XERCES
                         // initialize xercesc
             try {
@@ -62,10 +62,11 @@ namespace storm {
             xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement();
             
             if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "pnml") {
+                STORM_LOG_WARN_COND(constantDefinitions == "", "Constant definitions for pnml files are currently not supported.");
                 PnmlParser p;
                 return p.parse(elementRoot);
             } else if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "project") {
-                GreatSpnEditorProjectParser p;
+                GreatSpnEditorProjectParser p(constantDefinitions);
                 return p.parse(elementRoot);
             } else {
                 // If the top-level node is not a "pnml" or "" node, then throw an exception.

src/storm-gspn/parser/GspnParser.h

@@ -4,7 +4,7 @@ namespace storm {
     namespace parser {
         class GspnParser {
         public:
-            static storm::gspn::GSPN* parse(std::string const& filename);
+            static storm::gspn::GSPN* parse(std::string const& filename, std::string const& constantDefinitions = "");
         };
     }
 }

src/storm-gspn/settings/modules/GSPNSettings.cpp

@@ -19,12 +19,16 @@ namespace storm {
             const std::string GSPNSettings::capacitiesFileOptionName = "capacitiesfile";
             const std::string GSPNSettings::capacitiesFileOptionShortName = "capacities";
             const std::string GSPNSettings::capacityOptionName = "capacity";
+            const std::string GSPNSettings::constantsOptionName = "constants";
+            const std::string GSPNSettings::constantsOptionShortName = "const";
+
             
             
             GSPNSettings::GSPNSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, gspnFileOptionName, false, "Parses the GSPN.").setShortName(gspnFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, capacitiesFileOptionName, false, "Capacaties as invariants for places.").setShortName(capacitiesFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, capacityOptionName, false, "Global capacity as invariants for all places.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "capacity").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use.").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());
             }
             
             bool GSPNSettings::isGspnFileSet() const {
@@ -51,6 +55,14 @@ namespace storm {
                 return this->getOption(capacityOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
             }
             
+            bool GSPNSettings::isConstantsSet() const {
+                return this->getOption(constantsOptionName).getHasOptionBeenSet();
+            }
+
+            std::string GSPNSettings::getConstantDefinitionString() const {
+                return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString();
+            }
+            
             void GSPNSettings::finalize() {
                 
             }

src/storm-gspn/settings/modules/GSPNSettings.h

@@ -44,6 +44,16 @@ namespace storm {
                  */
                 uint64_t getCapacity() const;
                 
+                /*!
+                 * Retrieves whether the constants ption was set.
+                 */
+                bool isConstantsSet() const;
+
+                /*!
+                 * Retrieves the string that defines the constants of a gspn
+                 */
+                std::string getConstantDefinitionString() const;
+
                 
                 bool check() const override;
                 void finalize() override;
@@ -56,7 +66,8 @@ namespace storm {
                 static const std::string capacitiesFileOptionName;
                 static const std::string capacitiesFileOptionShortName;
                 static const std::string capacityOptionName;
-                
+                static const std::string constantsOptionName;
+                static const std::string constantsOptionShortName;
             };
         }
     }