From a734423e6e7fcf53621a9ec6bce0c4d3fa82d599 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 18 Nov 2016 17:44:14 +0100 Subject: [PATCH 1/5] gspn builder: name based construction of arcs now passes multiplicities --- src/storm/storage/gspn/GspnBuilder.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/gspn/GspnBuilder.cpp b/src/storm/storage/gspn/GspnBuilder.cpp index f5257456d..1800f02d5 100644 --- a/src/storm/storage/gspn/GspnBuilder.cpp +++ b/src/storm/storage/gspn/GspnBuilder.cpp @@ -56,7 +56,7 @@ namespace storm { void GspnBuilder::addInputArc(std::string const& from, std::string const& to, uint64_t multiplicity) { STORM_LOG_THROW(placeNames.count(from) != 0, storm::exceptions::InvalidArgumentException, "Could not find a place with name '" << from << "'"); STORM_LOG_THROW(transitionNames.count(to) != 0, storm::exceptions::InvalidArgumentException, "Could not find a transition with name << '" << to << "'"); - addInputArc(placeNames.at(from), transitionNames.at(to)); + addInputArc(placeNames.at(from), transitionNames.at(to), multiplicity); } void GspnBuilder::addInhibitionArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity) { @@ -69,7 +69,7 @@ namespace storm { void GspnBuilder::addInhibitionArc(std::string const& from, std::string const& to, uint64_t multiplicity) { STORM_LOG_THROW(placeNames.count(from) != 0, storm::exceptions::InvalidArgumentException, "Could not find a place with name '" << from << "'"); STORM_LOG_THROW(transitionNames.count(to) != 0, storm::exceptions::InvalidArgumentException, "Could not find a transition with name << '" << to << "'"); - addInhibitionArc(placeNames.at(from), transitionNames.at(to)); + addInhibitionArc(placeNames.at(from), transitionNames.at(to), multiplicity); } void GspnBuilder::addOutputArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity) { @@ -81,7 +81,7 @@ namespace storm { void GspnBuilder::addOutputArc(std::string const& from, std::string const& to, uint64_t multiplicity) { STORM_LOG_THROW(placeNames.count(to) != 0, storm::exceptions::InvalidArgumentException, "Could not find a place with name '" << to << "'"); STORM_LOG_THROW(transitionNames.count(from) != 0, storm::exceptions::InvalidArgumentException, "Could not find a transition with name << '" << from << "'"); - addOutputArc(transitionNames.at(from), placeNames.at(to)); + addOutputArc(transitionNames.at(from), placeNames.at(to), multiplicity); } Transition& GspnBuilder::getTransition(uint64_t id) { From 04003de85469bc3451ac11f500cba3ce3fa20a43 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 18 Nov 2016 17:45:19 +0100 Subject: [PATCH 2/5] transient unbounded variables must have iniatial value --- src/storm/builder/JaniGSPNBuilder.h | 2 +- src/storm/parser/JaniParser.cpp | 3 ++- src/storm/storage/jani/UnboundedIntegerVariable.cpp | 2 +- src/storm/storage/jani/UnboundedIntegerVariable.h | 2 +- 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/storm/builder/JaniGSPNBuilder.h b/src/storm/builder/JaniGSPNBuilder.h index bab976433..46c0fb095 100644 --- a/src/storm/builder/JaniGSPNBuilder.h +++ b/src/storm/builder/JaniGSPNBuilder.h @@ -39,7 +39,7 @@ namespace storm { storm::jani::Variable* janiVar = nullptr; if (!place.hasRestrictedCapacity()) { // Effectively no capacity limit known - janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), false); + janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens())); } else { assert(place.hasRestrictedCapacity()); janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity())); diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 30dd1fc70..4e1bf346d 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -609,7 +609,8 @@ namespace storm { } return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar); + assert(!transientVar); // Checked earlier. + return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName)); } else if(variableStructure.at("type") == "clock") { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'clock' for variable '" << name << "' (scope: " << scopeDescription << ")"); } else if(variableStructure.at("type") == "continuous") { diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.cpp b/src/storm/storage/jani/UnboundedIntegerVariable.cpp index 913d54af4..8cc8ede9f 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storm/storage/jani/UnboundedIntegerVariable.cpp @@ -7,7 +7,7 @@ namespace storm { // Intentionally left empty. } - UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable) { + UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.h b/src/storm/storage/jani/UnboundedIntegerVariable.h index f1b857469..16f54b723 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.h +++ b/src/storm/storage/jani/UnboundedIntegerVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates an unbounded integer variable without initial value. */ - UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates an unbounded integer variable with initial value. */ From dcaa83d9989a04ac8ebd33dcfd08033cbcf955d0 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 18 Nov 2016 17:46:32 +0100 Subject: [PATCH 3/5] fixed a series of spurious unused parameter warnings --- src/storm/generator/CompressedState.h | 2 +- src/storm/modelchecker/results/QualitativeCheckResult.cpp | 4 ++-- src/storm/parser/GspnParser.cpp | 2 +- src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm/generator/CompressedState.h b/src/storm/generator/CompressedState.h index 4ad89b604..1a785dbaa 100644 --- a/src/storm/generator/CompressedState.h +++ b/src/storm/generator/CompressedState.h @@ -15,7 +15,7 @@ namespace storm { typedef storm::storage::BitVector CompressedState; - class VariableInformation; + struct VariableInformation; /*! * Unpacks the compressed state into the evaluator. diff --git a/src/storm/modelchecker/results/QualitativeCheckResult.cpp b/src/storm/modelchecker/results/QualitativeCheckResult.cpp index a4122153b..d9b837493 100644 --- a/src/storm/modelchecker/results/QualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/QualitativeCheckResult.cpp @@ -5,11 +5,11 @@ namespace storm { namespace modelchecker { - QualitativeCheckResult& QualitativeCheckResult::operator&=(QualitativeCheckResult const& other) { + QualitativeCheckResult& QualitativeCheckResult::operator&=(QualitativeCheckResult const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'and' on the two check results."); } - QualitativeCheckResult& QualitativeCheckResult::operator|=(QualitativeCheckResult const& other) { + QualitativeCheckResult& QualitativeCheckResult::operator|=(QualitativeCheckResult const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'or' on the two check results."); } diff --git a/src/storm/parser/GspnParser.cpp b/src/storm/parser/GspnParser.cpp index 9a0eedd91..6f5b3c731 100644 --- a/src/storm/parser/GspnParser.cpp +++ b/src/storm/parser/GspnParser.cpp @@ -81,7 +81,7 @@ namespace storm { delete errHandler; xercesc::XMLPlatformUtils::Terminate(); #else - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Storm is not compiled with XML support"); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Storm is not compiled with XML support: " << filename << " can not be parsed"); #endif } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index e7f64c9a9..9efc0d34b 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -103,7 +103,7 @@ namespace storm { return std::make_pair(first, second); } - void InternalDdManager::allowDynamicReordering(bool value) { + void InternalDdManager::allowDynamicReordering(bool) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); } From ae3394ff5c8a15c9cb7f2946e8ca6febdca2928b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 18 Nov 2016 17:46:58 +0100 Subject: [PATCH 4/5] extended gspn export settigns --- .../settings/modules/GSPNExportSettings.cpp | 23 +++++++++++++++++++ .../settings/modules/GSPNExportSettings.h | 16 +++++++++++++ 2 files changed, 39 insertions(+) diff --git a/src/storm/settings/modules/GSPNExportSettings.cpp b/src/storm/settings/modules/GSPNExportSettings.cpp index ca00a6ec3..9be15c75e 100644 --- a/src/storm/settings/modules/GSPNExportSettings.cpp +++ b/src/storm/settings/modules/GSPNExportSettings.cpp @@ -16,11 +16,17 @@ namespace storm { const std::string GSPNExportSettings::moduleName = "exportGspn"; const std::string GSPNExportSettings::writeToDotOptionName = "gspn-dot-output"; + + const std::string GSPNExportSettings::writeToPnmlOptionName = "to-pnml"; + const std::string GSPNExportSettings::writeToPnproOptionName = "to-pnpro"; + //const std::string GSPNExportSettings::janiFileOptionShortName = "dotoutput"; GSPNExportSettings::GSPNExportSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, writeToDotOptionName, false, "Destination for the dot output.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnmlOptionName, false, "Destination for the pnml output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnproOptionName, false, "Destination for the pnpro output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); } bool GSPNExportSettings::isWriteToDotSet() const { @@ -31,6 +37,23 @@ namespace storm { return this->getOption(writeToDotOptionName).getArgumentByName("filename").getValueAsString(); } + bool GSPNExportSettings::isWriteToPnmlSet() const { + return this->getOption(writeToPnmlOptionName).getHasOptionBeenSet(); + } + + std::string GSPNExportSettings::getWriteToPnmlFilename() const { + return this->getOption(writeToPnmlOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GSPNExportSettings::isWriteToPnproSet() const { + return this->getOption(writeToPnproOptionName).getHasOptionBeenSet(); + } + + std::string GSPNExportSettings::getWriteToPnproFilename() const { + return this->getOption(writeToPnproOptionName).getArgumentByName("filename").getValueAsString(); + } + + void GSPNExportSettings::finalize() { } diff --git a/src/storm/settings/modules/GSPNExportSettings.h b/src/storm/settings/modules/GSPNExportSettings.h index 4a86428e5..3db836cf7 100644 --- a/src/storm/settings/modules/GSPNExportSettings.h +++ b/src/storm/settings/modules/GSPNExportSettings.h @@ -24,6 +24,20 @@ namespace storm { */ std::string getWriteToDotFilename() const; + bool isWriteToPnmlSet() const; + + /** + * + */ + std::string getWriteToPnmlFilename() const; + + bool isWriteToPnproSet() const; + + /** + * + */ + std::string getWriteToPnproFilename() const; + bool check() const override; void finalize() override; @@ -32,6 +46,8 @@ namespace storm { private: static const std::string writeToDotOptionName; + static const std::string writeToPnmlOptionName; + static const std::string writeToPnproOptionName; //static const std::string writeToDotOptionShortName; }; From ce988940d0b8aac70e3b9e8d575aeff908e7012f Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 18 Nov 2016 18:42:49 +0100 Subject: [PATCH 5/5] cmake fix for cpptemplate --- resources/3rdparty/include_cpptemplate.cmake | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/resources/3rdparty/include_cpptemplate.cmake b/resources/3rdparty/include_cpptemplate.cmake index 51426e755..138965f15 100644 --- a/resources/3rdparty/include_cpptemplate.cmake +++ b/resources/3rdparty/include_cpptemplate.cmake @@ -1,8 +1,10 @@ string(REPLACE " " ";" CMAKE_CXX_FLAGS_AS_LIST ${CMAKE_CXX_FLAGS}) if(CMAKE_BUILD_TYPE MATCHES DEBUG) - list(APPEND CMAKE_CXX_FLAGS_AS_LIST ${CMAKE_CXX_FLAGS_DEBUG}) + string(REPLACE " " ";" CMAKE_CXX_FLAGS_DEBUG_AS_LIST ${CMAKE_CXX_FLAGS_DEBUG}) + list(APPEND CMAKE_CXX_FLAGS_AS_LIST ${CMAKE_CXX_FLAGS_DEBUG_AS_LIST}) else() - list(APPEND CMAKE_CXX_FLAGS_AS_LIST ${CMAKE_CXX_FLAGS_RELEASE}) + string(REPLACE " " ";" CMAKE_CXX_FLAGS_RELEASE_AS_LIST ${CMAKE_CXX_FLAGS_RELEASE}) + list(APPEND CMAKE_CXX_FLAGS_AS_LIST ${CMAKE_CXX_FLAGS_RELEASE_AS_LIST}) endif() set(CPPTEMPLATE_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/cpptemplate) ExternalProject_Add(