diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 1dda8938e..4308a1de8 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/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 parseCapacitiesList(std::string const& filename) { - std::unordered_map map; - - std::ifstream stream; - storm::utility::openFile(filename, stream); - - std::string line; - while ( std::getline(stream, line) ) { - std::vector 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> propertyFilter; storm::parser::FormulaParser formulaParser(gspn->getExpressionManager()); std::vector 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); diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index b972b474c..7b18bc010 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/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 parseCapacitiesList(std::string const& filename, storm::gspn::GSPN const& gspn) { + storm::parser::ExpressionParser expressionParser(*gspn.getExpressionManager()); + std::unordered_map identifierMapping; + for (auto const& var : gspn.getExpressionManager()->getVariables()) { + identifierMapping.emplace(var.getName(), var.getExpression()); + } + expressionParser.setIdentifierMapping(identifierMapping); + expressionParser.setAcceptDoubleLiterals(false); + + std::unordered_map map; + + std::ifstream stream; + storm::utility::openFile(filename, stream); + + std::string line; + while ( std::getline(stream, line) ) { + std::vector 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; + } } } + diff --git a/src/storm-gspn/api/storm-gspn.h b/src/storm-gspn/api/storm-gspn.h index 7d2360946..a54bd6e28 100644 --- a/src/storm-gspn/api/storm-gspn.h +++ b/src/storm-gspn/api/storm-gspn.h @@ -1,5 +1,7 @@ #pragma once +#include + #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(storm::builder::JaniGSPNBuilder const&)> const& janiProperyGetter = [](storm::builder::JaniGSPNBuilder const&) { return std::vector(); }); - + + std::unordered_map parseCapacitiesList(std::string const& filename, storm::gspn::GSPN const& gspn); + } } diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp index 44fcb8bf8..4c77bc3a2 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp +++ b/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()), expressionParser(*manager) { + GreatSpnEditorProjectParser::GreatSpnEditorProjectParser(std::string const& constantDefinitionString) : manager(std::make_shared()) { if (constantDefinitionString != "") { std::vector 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(*manager); std::unordered_map 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(*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& 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 diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.h b/src/storm-gspn/parser/GreatSpnEditorProjectParser.h index 41606bd98..7663d2a23 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.h +++ b/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& 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 manager; - storm::parser::ExpressionParser expressionParser; + std::shared_ptr expressionParser; std::unordered_map constantDefinitions; + std::map constantsSubstitution; }; } } diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 5278b3b30..903425735 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -26,8 +26,8 @@ namespace storm { return tId; } - GSPN::GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, std::vector> const& ttransitions, std::vector const& partitions, std::shared_ptr const& exprManager) - : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager) + GSPN::GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, std::vector> const& ttransitions, std::vector const& partitions, std::shared_ptr const& exprManager, std::map 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 const& GSPN::getExpressionManager() const { + return exprManager; + } + + std::map const& GSPN::getConstantsSubstitution() const { + return constantsSubstitution; + } - std::shared_ptr const& GSPN::getExpressionManager() const { - return exprManager; - } - - void GSPN::setCapacities(std::unordered_map const& mapping) { + void GSPN::setCapacities(std::unordered_map 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); diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h index 7b37ed5cb..343dcd887 100644 --- a/src/storm-gspn/storage/gspn/GSPN.h +++ b/src/storm-gspn/storage/gspn/GSPN.h @@ -32,7 +32,7 @@ namespace storm { GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, - std::vector> const& ttransitions, std::vector const& partitions, std::shared_ptr const& exprManager); + std::vector> const& ttransitions, std::vector const& partitions, std::shared_ptr const& exprManager, std::map const& constantsSubstitution = std::map()); /*! * Returns the number of places in this gspn. @@ -145,8 +145,13 @@ namespace storm { */ std::shared_ptr const& getExpressionManager() const; + /*! + * Gets an assignment of occurring constants of the GSPN to their value + */ + std::map const& getConstantsSubstitution() const; + /** - * Set Capacities according to name->capacity map. + * Set Capacities of places according to name->capacity map. */ void setCapacities(std::unordered_map const& mapping); @@ -217,6 +222,8 @@ namespace storm { std::vector partitions; std::shared_ptr exprManager; + + std::map constantsSubstitution; // Layout information mutable std::map placeLayout; diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp index 6920680ed..c39b5c0f7 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -171,8 +171,13 @@ namespace storm { - storm::gspn::GSPN* GspnBuilder::buildGspn() const { - std::shared_ptr exprManager(new storm::expressions::ExpressionManager()); + storm::gspn::GSPN* GspnBuilder::buildGspn(std::shared_ptr const& exprManager, std::map const& constantsSubstitution) const { + std::shared_ptr actualExprManager; + if (exprManager) { + actualExprManager = exprManager; + } else { + actualExprManager = std::make_shared(); + } std::vector 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; diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h index 35c5ed220..5e4db4a34 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.h +++ b/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 const& exprManager = nullptr, std::map const& constantsSubstitution = std::map()) const; private: bool isImmediateTransitionId(uint64_t) const; bool isTimedTransitionId(uint64_t) const;