From 488aaeaa580063577aca3ea3e89dc89bd4951814 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 6 Feb 2017 18:41:14 +0100 Subject: [PATCH] properties in storm-gspn --- src/storm-gspn-cli/storm-gspn.cpp | 13 ++++++++++++- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 4 ++-- src/storm-gspn/builder/JaniGSPNBuilder.h | 7 +++---- src/storm-gspn/storage/gspn/GSPN.cpp | 4 ++-- src/storm-gspn/storage/gspn/GspnBuilder.cpp | 9 +++++---- src/storm/utility/storm.cpp | 2 +- src/storm/utility/storm.h | 5 +++++ 7 files changed, 30 insertions(+), 14 deletions(-) diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index fdf2594fc..b01824c50 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -14,6 +14,8 @@ #include "utility/storm.h" #include "storm/cli/cli.h" +#include "storm/parser/FormulaParser.h" + #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/JSONExporter.h" @@ -33,6 +35,7 @@ #include "storm/settings/modules/JaniExportSettings.h" #include "storm/settings/modules/ResourceSettings.h" + /*! * Initialize the settings manager. */ @@ -88,6 +91,14 @@ int main(const int argc, const char **argv) { auto parser = storm::parser::GspnParser(); auto gspn = parser.parse(storm::settings::getModule().getGspnFilename()); + std::string formulaString = ""; + if (!storm::settings::getModule().isPropertySet()) { + formulaString = storm::settings::getModule().getProperty(); + } + boost::optional> propertyFilter; + storm::parser::FormulaParser formulaParser(gspn->getExpressionManager()); + std::vector properties = storm::parseProperties(formulaParser, formulaString, propertyFilter); + if (!gspn->isValid()) { STORM_LOG_ERROR("The gspn is not valid."); } @@ -101,7 +112,7 @@ int main(const int argc, const char **argv) { if(storm::settings::getModule().isJaniFileSet()) { storm::jani::Model* model = storm::buildJani(*gspn); - storm::exportJaniModel(*model, {}, storm::settings::getModule().getJaniFilename()); + storm::exportJaniModel(*model, properties, storm::settings::getModule().getJaniFilename()); delete model; } diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 386d2b0a2..d5e8846ea 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -19,10 +19,10 @@ 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())); + janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->getVariable(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())); + janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->getVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity())); } assert(janiVar != nullptr); assert(vars.count(place.getID()) == 0); diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 791989009..474d04807 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -2,14 +2,15 @@ #include "storm-gspn/storage/gspn/GSPN.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" #include "storm/storage/expressions/ExpressionManager.h" namespace storm { namespace builder { class JaniGSPNBuilder { public: - JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr const& expManager) - : gspn(gspn), expressionManager(expManager) { + JaniGSPNBuilder(storm::gspn::GSPN const& gspn) + : gspn(gspn), expressionManager(gspn.getExpressionManager()) { } @@ -26,8 +27,6 @@ namespace storm { private: - - void addVariables(storm::jani::Model* model); uint64_t addLocation(storm::jani::Automaton& automaton); diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 34967daee..4a093b30e 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -28,7 +28,7 @@ namespace storm { } 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); + : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager) { } @@ -136,7 +136,7 @@ namespace storm { } - std::shared_ptr const& GSPN::getExpressionManager() { + std::shared_ptr const& GSPN::getExpressionManager() const { return exprManager; } diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp index 52833419a..5303a89c6 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -4,7 +4,6 @@ #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/utility/macros.h" -#include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "Place.h" @@ -165,7 +164,6 @@ namespace storm { storm::gspn::GSPN* GspnBuilder::buildGspn() const { std::shared_ptr exprManager(new storm::expressions::ExpressionManager()); - exprManager-> std::vector orderedPartitions; for(auto const& priorityPartitions : partitions) { @@ -180,8 +178,11 @@ namespace storm { } std::reverse(orderedPartitions.begin(), orderedPartitions.end()); - - GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions); + for(auto const& placeEntry : placeNames) { + exprManager->declareIntegerVariable(placeEntry.first, false); + } + + GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions, exprManager); result->setTransitionLayoutInfo(transitionLayout); result->setPlaceLayoutInfo(placeLayout); return result; diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp index 1023d6aa6..f4d04bdcd 100644 --- a/src/storm/utility/storm.cpp +++ b/src/storm/utility/storm.cpp @@ -41,7 +41,7 @@ namespace storm{ } } - std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter = boost::none) { + std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter) { // If the given property looks like a file (containing a dot and there exists a file with that name), // we try to parse it as a file, otherwise we assume it's a property. std::vector properties; diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 7e81f2a36..ef4785c1a 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -100,6 +100,10 @@ namespace storm { + namespace parser { + class FormulaParser; + } + template std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::none, boost::optional const& transitionRewardsFile = boost::none, boost::optional const& choiceLabelingFile = boost::none) { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); @@ -109,6 +113,7 @@ namespace storm { std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution); + std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter = boost::none); std::vector parsePropertiesForExplicit(std::string const& inputString, boost::optional> const& propertyFilter = boost::none); std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter = boost::none); std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter = boost::none);