From 41199ea5c7b14868568deb4dbffbf20487d65294 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 30 Mar 2020 14:55:21 +0200 Subject: [PATCH 1/4] Append in dot output for DDs --- src/storm/storage/dd/cudd/InternalCuddBdd.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index a850d6329..647c6b7ce 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -196,7 +196,7 @@ namespace storm { // Open the file, dump the DD and close it again. std::vector cuddBddVector = { this->getCuddBdd() }; - FILE* filePointer = fopen(filename.c_str() , "w"); + FILE* filePointer = fopen(filename.c_str() , "a+"); if (showVariablesIfPossible) { ddManager->getCuddManager().DumpDot(cuddBddVector, ddVariableNames.data(), &ddNames[0], filePointer); } else { From b8ac41f561b175c8469f85d75c6cb9148253112b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 30 Mar 2020 18:11:13 +0200 Subject: [PATCH 2/4] Fixed problem with stormpy by changing boost::optional arguments to const& in GSPNs --- src/storm-gspn/storage/gspn/GspnBuilder.cpp | 4 ++-- src/storm-gspn/storage/gspn/GspnBuilder.h | 4 ++-- src/storm-gspn/storage/gspn/Place.cpp | 2 +- src/storm-gspn/storage/gspn/Place.h | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp index c39b5c0f7..41ef64f96 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -13,7 +13,7 @@ namespace storm { gspnName = name; } - uint_fast64_t GspnBuilder::addPlace(boost::optional capacity, uint_fast64_t const& initialTokens, std::string const& name) { + uint_fast64_t GspnBuilder::addPlace(boost::optional const& capacity, uint_fast64_t const& initialTokens, std::string const& name) { auto newId = places.size(); auto place = storm::gspn::Place(newId); place.setCapacity(capacity); @@ -70,7 +70,7 @@ namespace storm { return addTimedTransition(priority, rate, 1, name); } - uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate, boost::optional numServers, std::string const& name) { + uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate, boost::optional const& numServers, std::string const& name) { auto trans = storm::gspn::TimedTransition(); auto newId = GSPN::timedTransitionIdToTransitionId(timedTransitions.size()); trans.setName(name); diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h index 5e4db4a34..fb4cd2ad7 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.h +++ b/src/storm-gspn/storage/gspn/GspnBuilder.h @@ -25,7 +25,7 @@ namespace storm { * A capacity of -1 indicates an unbounded place. * @param initialTokens The number of inital tokens in the place. */ - uint_fast64_t addPlace(boost::optional capacity = 1, uint_fast64_t const& initialTokens = 0, std::string const& name = ""); + uint_fast64_t addPlace(boost::optional const& capacity = 1, uint_fast64_t const& initialTokens = 0, std::string const& name = ""); void setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layoutInfo); @@ -51,7 +51,7 @@ namespace storm { * @param rate The rate for the transition. * @param numServers The number of servers this transition has (in case of K-Server semantics) or boost::none (in case of Infinite-Server-Semantics). */ - uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, boost::optional numServers, std::string const& name = ""); + uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, boost::optional const& numServers, std::string const& name = ""); void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo); diff --git a/src/storm-gspn/storage/gspn/Place.cpp b/src/storm-gspn/storage/gspn/Place.cpp index ca9a4a9e1..8d7347936 100644 --- a/src/storm-gspn/storage/gspn/Place.cpp +++ b/src/storm-gspn/storage/gspn/Place.cpp @@ -29,7 +29,7 @@ namespace storm { return this->numberOfInitialTokens; } - void Place::setCapacity(boost::optional cap) { + void Place::setCapacity(boost::optional const& cap) { this->capacity = cap; } diff --git a/src/storm-gspn/storage/gspn/Place.h b/src/storm-gspn/storage/gspn/Place.h index 55c9da6fb..b6a8b4ca1 100644 --- a/src/storm-gspn/storage/gspn/Place.h +++ b/src/storm-gspn/storage/gspn/Place.h @@ -56,7 +56,7 @@ namespace storm { * @param capacity The capacity of this place. A non-negative number represents the capacity. * boost::none indicates that the flag is not set. */ - void setCapacity(boost::optional capacity); + void setCapacity(boost::optional const& capacity); /*! * Returns the capacity of tokens of this place. From 94d08d73fb740bf38c747d74f49eeaa1310338c0 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 31 Mar 2020 14:42:38 +0200 Subject: [PATCH 3/4] Capitalized GUROBI in FindGUROBI.cmake file because it was not found on linux. --- .../cmake/find_modules/{FindGurobi.cmake => FindGUROBI.cmake} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename resources/cmake/find_modules/{FindGurobi.cmake => FindGUROBI.cmake} (100%) diff --git a/resources/cmake/find_modules/FindGurobi.cmake b/resources/cmake/find_modules/FindGUROBI.cmake similarity index 100% rename from resources/cmake/find_modules/FindGurobi.cmake rename to resources/cmake/find_modules/FindGUROBI.cmake From a80553a700df59d89709427d16ebfffe72342b0c Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 31 Mar 2020 14:43:35 +0200 Subject: [PATCH 4/4] Removed a duplicated method in StandardRewardModel (setStateActionRewardValue did the same as setStateActionReward) --- src/storm/models/sparse/StandardRewardModel.cpp | 5 ----- src/storm/models/sparse/StandardRewardModel.h | 9 --------- 2 files changed, 14 deletions(-) diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index 159c39446..b017ae58a 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -349,11 +349,6 @@ namespace storm { return result; } - template - void StandardRewardModel::setStateActionRewardValue(uint_fast64_t row, ValueType const& value) { - this->optionalStateActionRewardVector.get()[row] = value; - } - template template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitions) { diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index 2bfed8143..aedd7c535 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -287,15 +287,6 @@ namespace storm { template storm::storage::BitVector getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; - /*! - * Sets the given value in the state-action reward vector at the given row. This assumes that the reward - * model has state-action rewards. - * - * @param row The row at which to set the given value. - * @param value The value to set. - */ - void setStateActionRewardValue(uint_fast64_t row, ValueType const& value); - /*! * Retrieves whether the reward model is empty, i.e. contains no state-, state-action- or transition-based * rewards.