From a44eed65e8d5e8d7324ccc42df462c73cdf89c1f Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 Aug 2018 10:39:49 +0200 Subject: [PATCH] allowing constant definitions for gspns via cli --- src/storm-gspn-cli/storm-gspn.cpp | 7 ++++- .../parser/GreatSpnEditorProjectParser.cpp | 29 ++++++++++++++++--- .../parser/GreatSpnEditorProjectParser.h | 4 +-- src/storm-gspn/parser/GspnParser.cpp | 5 ++-- src/storm-gspn/parser/GspnParser.h | 2 +- .../settings/modules/GSPNSettings.cpp | 12 ++++++++ .../settings/modules/GSPNSettings.h | 13 ++++++++- 7 files changed, 61 insertions(+), 11 deletions(-) diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 6b9c5e2ee..1dda8938e 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/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().isPropertySet()) { diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp index 17d49e6f1..9bee3d085 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp +++ b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp @@ -23,8 +23,15 @@ namespace { namespace storm { namespace parser { - GreatSpnEditorProjectParser::GreatSpnEditorProjectParser() : manager(std::make_shared()), expressionParser(*manager) { - // Intentionally left empty + GreatSpnEditorProjectParser::GreatSpnEditorProjectParser(std::string const& constantDefinitionString) : manager(std::make_shared()), expressionParser(*manager) { + std::vector constDefs; + boost::split( constDefs, constantDefinitionString, boost::is_any_of(",")); + for (auto const& pair : constDefs) { + std::vector 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 { diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.h b/src/storm-gspn/parser/GreatSpnEditorProjectParser.h index ba6f67a6a..693422af7 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.h +++ b/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 manager; storm::parser::ExpressionParser expressionParser; - + std::unordered_map constantDefinitions; }; } } diff --git a/src/storm-gspn/parser/GspnParser.cpp b/src/storm-gspn/parser/GspnParser.cpp index b92b6f006..89a2f57e9 100644 --- a/src/storm-gspn/parser/GspnParser.cpp +++ b/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. diff --git a/src/storm-gspn/parser/GspnParser.h b/src/storm-gspn/parser/GspnParser.h index 862dfc757..512f0ddd6 100644 --- a/src/storm-gspn/parser/GspnParser.h +++ b/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 = ""); }; } } diff --git a/src/storm-gspn/settings/modules/GSPNSettings.cpp b/src/storm-gspn/settings/modules/GSPNSettings.cpp index fd274726f..b114559a5 100644 --- a/src/storm-gspn/settings/modules/GSPNSettings.cpp +++ b/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() { } diff --git a/src/storm-gspn/settings/modules/GSPNSettings.h b/src/storm-gspn/settings/modules/GSPNSettings.h index 665e588fb..78586cf9c 100644 --- a/src/storm-gspn/settings/modules/GSPNSettings.h +++ b/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; }; } }