From d655621ea1a44aa54dcb82ff9779963c99b303ab Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 11 May 2017 13:13:13 +0200 Subject: [PATCH] Fixed seg fault when building model valuations --- src/storm/builder/ExplicitModelBuilder.h | 2 +- src/storm/storage/expressions/SimpleValuation.cpp | 8 ++++---- src/storm/storage/expressions/Valuation.cpp | 4 ++++ src/storm/storage/expressions/Valuation.h | 8 ++++++++ 4 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 25acb684c..0141b2d68 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -79,7 +79,7 @@ namespace storm { // A flag that indicates whether or not to store the state information after successfully building the // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful - // call to translateProgram. + // call to build. bool buildStateValuations; }; diff --git a/src/storm/storage/expressions/SimpleValuation.cpp b/src/storm/storage/expressions/SimpleValuation.cpp index f0dd7deef..e60556305 100644 --- a/src/storm/storage/expressions/SimpleValuation.cpp +++ b/src/storm/storage/expressions/SimpleValuation.cpp @@ -19,7 +19,7 @@ namespace storm { // Intentionally left empty. } - SimpleValuation::SimpleValuation(SimpleValuation const& other) : Valuation(other.getManager().getSharedPointer()) { + SimpleValuation::SimpleValuation(SimpleValuation const& other) : Valuation(other.getManagerAsSharedPtr()) { if (this != &other) { booleanValues = other.booleanValues; integerValues = other.integerValues; @@ -29,7 +29,7 @@ namespace storm { SimpleValuation& SimpleValuation::operator=(SimpleValuation const& other) { if (this != &other) { - this->setManager(other.getManager().getSharedPointer()); + this->setManager(other.getManagerAsSharedPtr()); booleanValues = other.booleanValues; integerValues = other.integerValues; rationalValues = other.rationalValues; @@ -37,7 +37,7 @@ namespace storm { return *this; } - SimpleValuation::SimpleValuation(SimpleValuation&& other) : Valuation(other.getManager().getSharedPointer()) { + SimpleValuation::SimpleValuation(SimpleValuation&& other) : Valuation(other.getManagerAsSharedPtr()) { if (this != &other) { booleanValues = std::move(other.booleanValues); integerValues = std::move(other.integerValues); @@ -47,7 +47,7 @@ namespace storm { SimpleValuation& SimpleValuation::operator=(SimpleValuation&& other) { if (this != &other) { - this->setManager(other.getManager().getSharedPointer()); + this->setManager(other.getManagerAsSharedPtr()); booleanValues = std::move(other.booleanValues); integerValues = std::move(other.integerValues); rationalValues = std::move(other.rationalValues); diff --git a/src/storm/storage/expressions/Valuation.cpp b/src/storm/storage/expressions/Valuation.cpp index 81ab20467..912617a18 100644 --- a/src/storm/storage/expressions/Valuation.cpp +++ b/src/storm/storage/expressions/Valuation.cpp @@ -15,6 +15,10 @@ namespace storm { return *manager; } + std::shared_ptr const& Valuation::getManagerAsSharedPtr() const { + return manager; + } + void Valuation::setManager(std::shared_ptr const& manager) { this->manager = manager; } diff --git a/src/storm/storage/expressions/Valuation.h b/src/storm/storage/expressions/Valuation.h index 0ce691db4..fbe6e4470 100644 --- a/src/storm/storage/expressions/Valuation.h +++ b/src/storm/storage/expressions/Valuation.h @@ -101,6 +101,14 @@ namespace storm { ExpressionManager const& getManager() const; protected: + + /*! + * Retrieves the manager responsible for the variables of this valuation. + * + * @return The manager. + */ + std::shared_ptr const& getManagerAsSharedPtr() const; + /*! * Sets the manager responsible for the variables in this valuation. *