More robust parsing of capacities and allowing constants in GSPN properties

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

@@ -5,9 +5,6 @@
 #include "storm-gspn/builder/JaniGSPNBuilder.h"
 #include "storm-gspn/api/storm-gspn.h"
 
-#include "storm/exceptions/BaseException.h"
-#include "storm/exceptions/WrongFormatException.h"
-
 #include "storm/utility/macros.h"
 #include "storm/utility/initialize.h"
 
@@ -57,25 +54,6 @@ void initializeSettings() {
 }
 
 
-std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const& filename) {
-    std::unordered_map<std::string, uint64_t> map;
-    
-    std::ifstream stream;
-    storm::utility::openFile(filename, stream);
-    
-    std::string line;
-    while ( std::getline(stream, line) ) {
-        std::vector<std::string> strs;
-        boost::split(strs, line, boost::is_any_of("\t "));
-        STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs");
-        std::cout << std::stoll(strs[1]) << std::endl;
-        map[strs[0]] = std::stoll(strs[1]);
-    }
-    storm::utility::closeFile(stream);
-    return map;
-}
-
-
 int main(const int argc, const char **argv) {
     try {
         storm::utility::setUp();
@@ -109,13 +87,14 @@ int main(const int argc, const char **argv) {
         boost::optional<std::set<std::string>> propertyFilter;
         storm::parser::FormulaParser formulaParser(gspn->getExpressionManager());
         std::vector<storm::jani::Property> properties  = storm::api::parseProperties(formulaParser, formulaString, propertyFilter);
-
+        properties = storm::api::substituteConstantsInProperties(properties, gspn->getConstantsSubstitution());
+        
         if (!gspn->isValid()) {
             STORM_LOG_ERROR("The gspn is not valid.");
         }
         
         if(gspnSettings.isCapacitiesFileSet()) {
-            auto capacities = parseCapacitiesList(gspnSettings.getCapacitiesFilename());
+            auto capacities = storm::api::parseCapacitiesList(gspnSettings.getCapacitiesFilename(), *gspn);
             gspn->setCapacities(capacities);
         } else if (gspnSettings.isCapacitySet()) {
             uint64_t capacity = gspnSettings.getCapacity();
@@ -131,7 +110,6 @@ int main(const int argc, const char **argv) {
         delete gspn;
         return 0;
         
-//
 //        // construct ma
 //        auto builder = storm::builder::ExplicitGspnModelBuilder<>();
 //        auto ma = builder.translateGspn(gspn, formula);

src/storm-gspn/api/storm-gspn.cpp

@@ -5,7 +5,8 @@
 #include "storm-gspn/settings/modules/GSPNExportSettings.h"
 #include "storm-conv/settings/modules/JaniExportSettings.h"
 #include "storm-conv/api/storm-conv.h"
-
+#include "storm-parsers/parser/ExpressionParser.h"
+#include "storm/exceptions/WrongFormatException.h"
 
 namespace storm {
     namespace api {
@@ -75,5 +76,36 @@ namespace storm {
                 delete model;
             }
         }
+        
+        std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const& filename, storm::gspn::GSPN const& gspn) {
+            storm::parser::ExpressionParser expressionParser(*gspn.getExpressionManager());
+            std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
+            for (auto const& var : gspn.getExpressionManager()->getVariables()) {
+                identifierMapping.emplace(var.getName(), var.getExpression());
+            }
+            expressionParser.setIdentifierMapping(identifierMapping);
+            expressionParser.setAcceptDoubleLiterals(false);
+            
+            std::unordered_map<std::string, uint64_t> map;
+            
+            std::ifstream stream;
+            storm::utility::openFile(filename, stream);
+            
+            std::string line;
+            while ( std::getline(stream, line) ) {
+                std::vector<std::string> strs;
+                boost::split(strs, line, boost::is_any_of("\t "));
+                STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs");
+                storm::expressions::Expression expr = expressionParser.parseFromString(strs[1]);
+                if (!gspn.getConstantsSubstitution().empty()) {
+                    expr = expr.substitute(gspn.getConstantsSubstitution());
+                }
+                STORM_LOG_THROW(!expr.containsVariables(), storm::exceptions::WrongFormatException, "The capacity expression '" << strs[1] << "' still contains undefined constants.");
+                map[strs[0]] = expr.evaluateAsInt();
+            }
+            storm::utility::closeFile(stream);
+            return map;
+        }
     }
 }
+

src/storm-gspn/api/storm-gspn.h

@@ -1,5 +1,7 @@
 #pragma once
 
+#include <unordered_map>
+
 #include "storm/storage/jani/Model.h"
 #include "storm-gspn/storage/gspn/GSPN.h"
 #include "storm-gspn/builder/JaniGSPNBuilder.h"
@@ -14,6 +16,8 @@ namespace storm {
 
         void handleGSPNExportSettings(storm::gspn::GSPN const& gspn,
                                       std::function<std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const&)> const& janiProperyGetter = [](storm::builder::JaniGSPNBuilder const&) { return std::vector<storm::jani::Property>(); });
-                                      
+        
+        std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const& filename, storm::gspn::GSPN const& gspn);
+        
     }
 }

src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp

@@ -23,7 +23,7 @@ namespace {
 namespace storm {
     namespace parser {
 
-        GreatSpnEditorProjectParser::GreatSpnEditorProjectParser(std::string const& constantDefinitionString) : manager(std::make_shared<storm::expressions::ExpressionManager>()), expressionParser(*manager) {
+        GreatSpnEditorProjectParser::GreatSpnEditorProjectParser(std::string const& constantDefinitionString) : manager(std::make_shared<storm::expressions::ExpressionManager>()) {
             if (constantDefinitionString != "") {
                 std::vector<std::string> constDefs;
                 boost::split( constDefs, constantDefinitionString, boost::is_any_of(","));
@@ -39,7 +39,7 @@ namespace storm {
         storm::gspn::GSPN* GreatSpnEditorProjectParser::parse(xercesc::DOMElement const*  elementRoot) {
             if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "project") {
                 traverseProjectElement(elementRoot);
-                return builder.buildGspn();
+                return builder.buildGspn(manager, constantsSubstitution);
             } else {
                 // If the top-level node is not a "pnml" or "" node, then throw an exception.
                 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n");
@@ -130,17 +130,23 @@ namespace storm {
 
             // traverse children
             // First pass: find constant definitions
+            constantsSubstitution.clear();
+            expressionParser = std::make_shared<storm::parser::ExpressionParser>(*manager);
             std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
-            expressionParser.setIdentifierMapping(identifierMapping);
+            expressionParser->setIdentifierMapping(identifierMapping);
             for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
                 auto child = node->getChildNodes()->item(i);
                 auto name = storm::adapters::getName(child);
                 if (name.compare("constant") == 0 || name.compare("template") == 0) {
-                    traverseConstantOrTemplateElement(child, identifierMapping);
+                    traverseConstantOrTemplateElement(child);
                 }
             }
-            expressionParser.setIdentifierMapping(identifierMapping);
-            
+            // Update the expression parser to make the newly created variables known to it
+            expressionParser = std::make_shared<storm::parser::ExpressionParser>(*manager);
+            for (auto const& var : manager->getVariables()) {
+                identifierMapping.emplace(var.getName(), var.getExpression());
+            }
+            expressionParser->setIdentifierMapping(identifierMapping);
             // Second pass: traverse other children
             for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
                 auto child = node->getChildNodes()->item(i);
@@ -162,7 +168,7 @@ namespace storm {
             }
         }
 
-        void GreatSpnEditorProjectParser::traverseConstantOrTemplateElement(xercesc::DOMNode const* const node, std::unordered_map<std::string, storm::expressions::Expression>& identifierMapping) {
+        void GreatSpnEditorProjectParser::traverseConstantOrTemplateElement(xercesc::DOMNode const* const node) {
             std::string identifier;
             storm::expressions::Type type;
             std::string valueStr = "";
@@ -193,24 +199,24 @@ namespace storm {
                 }
             }
             
-            STORM_LOG_THROW(identifierMapping.count(identifier) == 0, storm::exceptions::NotSupportedException, "Multiple definitions of constant '" << identifier << "' were found.");
-            storm::expressions::Expression valueExpression;
+            STORM_LOG_THROW(!manager->hasVariable(identifier), storm::exceptions::NotSupportedException, "Multiple definitions of constant '" << identifier << "' were found.");
             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;
             }
+            storm::expressions::Variable var;
             if (type.isRationalType()) {
-                expressionParser.setAcceptDoubleLiterals(true);
-                valueExpression = manager->rational(expressionParser.parseFromString(valueStr).evaluateAsRational());
+                var = manager->declareRationalVariable(identifier);
+                expressionParser->setAcceptDoubleLiterals(true);
             } else if (type.isIntegerType()) {
-                expressionParser.setAcceptDoubleLiterals(false);
-                valueExpression = manager->integer(expressionParser.parseFromString(valueStr).evaluateAsInt());
+                var = manager->declareIntegerVariable(identifier);
+                expressionParser->setAcceptDoubleLiterals(false);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unknown type of constant" << type << ".");
             }
-            identifierMapping.emplace(identifier, valueExpression);
-
+            constantsSubstitution.emplace(var, expressionParser->parseFromString(valueStr));
+            
             // traverse children
             for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
                 auto child = node->getChildNodes()->item(i);
@@ -277,8 +283,7 @@ namespace storm {
                 if (name.compare("name") == 0) {
                     placeName = storm::adapters::XMLtoString(attr->getNodeValue());
                 } else if (name.compare("marking") == 0) {
-                    expressionParser.setAcceptDoubleLiterals(false);
-                    initialTokens = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsInt();
+                    initialTokens = parseInt(storm::adapters::XMLtoString(attr->getNodeValue()));
                 } else if (ignorePlaceAttribute(name)) {
                     // ignore node
                 } else {
@@ -338,14 +343,11 @@ namespace storm {
                         STORM_PRINT_AND_LOG("unknown transition type: " << storm::adapters::XMLtoString(attr->getNodeValue()));
                     }
                 } else if(name.compare("delay") == 0) {
-                    expressionParser.setAcceptDoubleLiterals(true);
-                    rate = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsDouble();
+                    rate = parseReal(storm::adapters::XMLtoString(attr->getNodeValue()));
                 } else if(name.compare("weight") == 0) {
-                    expressionParser.setAcceptDoubleLiterals(true);
-                    weight = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsDouble();
+                    weight = parseReal(storm::adapters::XMLtoString(attr->getNodeValue()));
                 } else if(name.compare("priority") == 0) {
-                    expressionParser.setAcceptDoubleLiterals(false);
-                    priority = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsInt();
+                    priority = parseInt(storm::adapters::XMLtoString(attr->getNodeValue()));
                 } else if (name.compare("nservers") == 0) {
                     std::string nservers = storm::adapters::XMLtoString(attr->getNodeValue());
                     if (nservers == "Single") {
@@ -353,8 +355,7 @@ namespace storm {
                     } else if (nservers == "Infinite") {
                         // Ignore this case as we assume infinite by default (similar to GreatSpn)
                     } else {
-                        expressionParser.setAcceptDoubleLiterals(false);
-                        numServers = expressionParser.parseFromString(nservers).evaluateAsInt();
+                        numServers = parseInt(nservers);
                     }
                 } else if (ignoreTransitionAttribute(name)) {
                     // ignore node
@@ -419,8 +420,7 @@ namespace storm {
                 } else if (name.compare("kind") == 0 || name.compare("type") == 0) {
                     kind = storm::adapters::XMLtoString(attr->getNodeValue());
                 } else if (name.compare("mult") == 0) {
-                    expressionParser.setAcceptDoubleLiterals(false);
-                    mult = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsInt();
+                    mult = parseInt(storm::adapters::XMLtoString(attr->getNodeValue()));
                 } else if (ignoreArcAttribute(name)) {
                     // ignore node
                 } else {
@@ -463,6 +463,21 @@ namespace storm {
             }
         }
         
+        int64_t GreatSpnEditorProjectParser::parseInt(std::string str) {
+            expressionParser->setAcceptDoubleLiterals(false);
+            auto expr = expressionParser->parseFromString(str).substitute(constantsSubstitution);
+            STORM_LOG_ASSERT(!expr.containsVariables(), "Can not evaluate expression " << str << " as it contains undefined variables.");
+            return expr.evaluateAsInt();
+        }
+        
+        double GreatSpnEditorProjectParser::parseReal(std::string str) {
+            expressionParser->setAcceptDoubleLiterals(true);
+            auto expr = expressionParser->parseFromString(str).substitute(constantsSubstitution);
+            STORM_LOG_ASSERT(!expr.containsVariables(), "Can not evaluate expression " << str << " as it contains undefined variables.");
+            return expr.evaluateAsDouble();
+        }
+        
+        
     }
 }
 #endif

src/storm-gspn/parser/GreatSpnEditorProjectParser.h

@@ -36,17 +36,20 @@ namespace storm {
             void traverseNodesElement(xercesc::DOMNode const* const node);
             void traverseEdgesElement(xercesc::DOMNode const* const node);
             
-            void traverseConstantOrTemplateElement(xercesc::DOMNode const* const node, std::unordered_map<std::string, storm::expressions::Expression>& identifierMapping);
+            void traverseConstantOrTemplateElement(xercesc::DOMNode const* const node);
             void traversePlaceElement(xercesc::DOMNode const* const node);
             void traverseTransitionElement(xercesc::DOMNode const* const node);
             void traverseArcElement(xercesc::DOMNode const* const node);
             
+            int64_t parseInt(std::string str);
+            double parseReal(std::string str);
             
             // the constructed gspn
             storm::gspn::GspnBuilder builder;
             std::shared_ptr<storm::expressions::ExpressionManager> manager;
-            storm::parser::ExpressionParser expressionParser;
+            std::shared_ptr<storm::parser::ExpressionParser> expressionParser;
             std::unordered_map<std::string, std::string> constantDefinitions;
+            std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution;
         };
     }
 }

src/storm-gspn/storage/gspn/GSPN.cpp

@@ -26,8 +26,8 @@ namespace storm {
             return tId;
         }
         
-        GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager)
-        : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager)
+        GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution)
+        : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager), constantsSubstitution(constantsSubstitution)
         {
             
         }
@@ -134,12 +134,16 @@ namespace storm {
             return getImmediateTransition(id);
         }
 
+    
+        std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() const {
+            return exprManager;
+        }
+        
+        std::map<storm::expressions::Variable, storm::expressions::Expression> const& GSPN::getConstantsSubstitution() const {
+            return constantsSubstitution;
+        }
 
-    std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() const {
-        return exprManager;
-    }
-
-    void GSPN::setCapacities(std::unordered_map<std::string, uint64_t> const& mapping) {
+        void GSPN::setCapacities(std::unordered_map<std::string, uint64_t> const& mapping) {
             for(auto const& entry : mapping) {
                 storm::gspn::Place* place = getPlace(entry.first);
                 STORM_LOG_THROW(place != nullptr, storm::exceptions::InvalidArgumentException, "No place with name " << entry.first);

src/storm-gspn/storage/gspn/GSPN.h

@@ -32,7 +32,7 @@ namespace storm {
             
             
             GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions,
-                 std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager);
+                 std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution = std::map<storm::expressions::Variable, storm::expressions::Expression>());
             
             /*!
              * Returns the number of places in this gspn.
@@ -145,8 +145,13 @@ namespace storm {
              */
             std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const;
             
+            /*!
+             * Gets an assignment of occurring constants of the GSPN to their value
+             */
+            std::map<storm::expressions::Variable, storm::expressions::Expression> const& getConstantsSubstitution() const;
+            
             /**
-             *  Set Capacities according to name->capacity map.
+             *  Set Capacities of places according to name->capacity map.
              */
             void setCapacities(std::unordered_map<std::string, uint64_t> const& mapping);
             
@@ -217,6 +222,8 @@ namespace storm {
             std::vector<storm::gspn::TransitionPartition> partitions;
 
             std::shared_ptr<storm::expressions::ExpressionManager> exprManager;
+            
+            std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution;
 
             // Layout information
             mutable std::map<uint64_t, LayoutInfo> placeLayout;

src/storm-gspn/storage/gspn/GspnBuilder.cpp

@@ -171,8 +171,13 @@ namespace storm {
         
         
 
-        storm::gspn::GSPN* GspnBuilder::buildGspn() const {
-            std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
+        storm::gspn::GSPN* GspnBuilder::buildGspn(std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution) const {
+            std::shared_ptr<storm::expressions::ExpressionManager> actualExprManager;
+            if (exprManager) {
+                actualExprManager = exprManager;
+            } else {
+                actualExprManager = std::make_shared<storm::expressions::ExpressionManager>();
+            }
 
             std::vector<TransitionPartition> orderedPartitions;
             for(auto const& priorityPartitions : partitions) {
@@ -188,10 +193,10 @@ namespace storm {
             }
             std::reverse(orderedPartitions.begin(), orderedPartitions.end());
             for(auto const& placeEntry : placeNames) {
-                exprManager->declareIntegerVariable(placeEntry.first, false);
+                actualExprManager->declareIntegerVariable(placeEntry.first, false);
             }
 
-            GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions, exprManager);
+            GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions, actualExprManager, constantsSubstitution);
             result->setTransitionLayoutInfo(transitionLayout);
             result->setPlaceLayoutInfo(placeLayout);
             return result;

src/storm-gspn/storage/gspn/GspnBuilder.h

@@ -100,10 +100,10 @@ namespace storm {
             
             
             /**
-             *
+             * @param exprManager The expression manager that will be associated with the new gspn. If this is nullptr, a new expressionmanager will be created.
              * @return The gspn which is constructed by the builder.
              */
-            storm::gspn::GSPN* buildGspn() const;
+            storm::gspn::GSPN* buildGspn(std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = nullptr, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution = std::map<storm::expressions::Variable, storm::expressions::Expression>()) const;
         private:
             bool isImmediateTransitionId(uint64_t) const;
             bool isTimedTransitionId(uint64_t) const;