From cab08525f82209b24b396c19666b7ee912f743c1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 16 Feb 2017 08:37:48 +0100 Subject: [PATCH 1/2] fix in SymbolicToSparseTransformer --- src/storm/models/sparse/StateLabeling.cpp | 4 ++-- src/storm/transformer/SymbolicToSparseTransformer.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index 55eaa76d5..df289d439 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -61,14 +61,14 @@ namespace storm { void StateLabeling::addLabel(std::string const& label, storage::BitVector const& labeling) { STORM_LOG_THROW(!this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' already exists."); - STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size."); + STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size. Expected: " << stateCount << " Actual: " << labeling.size()); nameToLabelingIndexMap.emplace(label, labelings.size()); labelings.push_back(labeling); } void StateLabeling::addLabel(std::string const& label, storage::BitVector&& labeling) { STORM_LOG_THROW(!this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' already exists."); - STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size."); + STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size. Expected: " << stateCount << " Actual: " << labeling.size()); nameToLabelingIndexMap.emplace(label, labelings.size()); labelings.emplace_back(std::move(labeling)); } diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp index a8b82133f..5dfbd2b4a 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.cpp +++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp @@ -32,7 +32,7 @@ namespace storm { } rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards)); } - storm::models::sparse::StateLabeling labelling; + storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount()); labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd)); labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd)); From 5181c0014986e3df7f789e82b723b1a67004fe1a Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Feb 2017 22:24:36 +0100 Subject: [PATCH 2/2] fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before. --- .../expressions/BinaryBooleanFunctionExpression.cpp | 6 +++++- .../storage/expressions/BinaryBooleanFunctionExpression.h | 1 + .../expressions/BinaryNumericalFunctionExpression.cpp | 6 +++++- .../expressions/BinaryNumericalFunctionExpression.h | 1 + src/storm/storage/expressions/BinaryRelationExpression.cpp | 6 +++++- src/storm/storage/expressions/BinaryRelationExpression.h | 1 + src/storm/storage/expressions/BooleanLiteralExpression.cpp | 6 +++++- src/storm/storage/expressions/BooleanLiteralExpression.h | 2 +- src/storm/storage/expressions/IfThenElseExpression.cpp | 4 ++++ src/storm/storage/expressions/IfThenElseExpression.h | 3 ++- src/storm/storage/expressions/IntegerLiteralExpression.cpp | 7 ++++++- src/storm/storage/expressions/IntegerLiteralExpression.h | 3 ++- .../storage/expressions/RationalLiteralExpression.cpp | 4 ++++ src/storm/storage/expressions/RationalLiteralExpression.h | 1 + .../storage/expressions/UnaryBooleanFunctionExpression.cpp | 6 +++++- .../storage/expressions/UnaryBooleanFunctionExpression.h | 1 + .../expressions/UnaryNumericalFunctionExpression.cpp | 6 +++++- .../storage/expressions/UnaryNumericalFunctionExpression.h | 3 ++- src/storm/storage/expressions/VariableExpression.cpp | 6 +++++- src/storm/storage/expressions/VariableExpression.h | 1 + 20 files changed, 62 insertions(+), 12 deletions(-) diff --git a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp index ea25593a2..32aed361e 100644 --- a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -122,7 +122,11 @@ namespace storm { boost::any BinaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BinaryBooleanFunctionExpression::isBinaryBooleanFunctionExpression() const { + return true; + } + void BinaryBooleanFunctionExpression::printToStream(std::ostream& stream) const { stream << "(" << *this->getFirstOperand(); switch (this->getOperatorType()) { diff --git a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h index f0dc1ea51..eb1344262 100644 --- a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h @@ -38,6 +38,7 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isBinaryBooleanFunctionExpression() const override; /*! * Retrieves the operator associated with the expression. diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 3d2e09153..0ed3dc746 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -122,7 +122,11 @@ namespace storm { boost::any BinaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BinaryNumericalFunctionExpression::isBinaryNumericalFunctionExpression() const { + return true; + } + void BinaryNumericalFunctionExpression::printToStream(std::ostream& stream) const { stream << "("; switch (this->getOperatorType()) { diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h index 7cc27fda1..b69c3b8c5 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h @@ -39,6 +39,7 @@ namespace storm { virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isBinaryNumericalFunctionExpression() const override; /*! * Retrieves the operator associated with the expression. diff --git a/src/storm/storage/expressions/BinaryRelationExpression.cpp b/src/storm/storage/expressions/BinaryRelationExpression.cpp index a610802e8..331c8b85e 100644 --- a/src/storm/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storm/storage/expressions/BinaryRelationExpression.cpp @@ -85,7 +85,11 @@ namespace storm { boost::any BinaryRelationExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BinaryRelationExpression::isBinaryRelationExpression() const { + return true; + } + BinaryRelationExpression::RelationType BinaryRelationExpression::getRelationType() const { return this->relationType; } diff --git a/src/storm/storage/expressions/BinaryRelationExpression.h b/src/storm/storage/expressions/BinaryRelationExpression.h index dc9c1e080..a9ed11924 100644 --- a/src/storm/storage/expressions/BinaryRelationExpression.h +++ b/src/storm/storage/expressions/BinaryRelationExpression.h @@ -38,6 +38,7 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isBinaryRelationExpression() const override; /*! * Retrieves the relation associated with the expression. diff --git a/src/storm/storage/expressions/BooleanLiteralExpression.cpp b/src/storm/storage/expressions/BooleanLiteralExpression.cpp index 409cd4b19..c09e5c894 100644 --- a/src/storm/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storm/storage/expressions/BooleanLiteralExpression.cpp @@ -35,7 +35,11 @@ namespace storm { boost::any BooleanLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BooleanLiteralExpression::isBooleanLiteralExpression() const { + return true; + } + bool BooleanLiteralExpression::getValue() const { return this->value; } diff --git a/src/storm/storage/expressions/BooleanLiteralExpression.h b/src/storm/storage/expressions/BooleanLiteralExpression.h index 944b47708..b989493d0 100644 --- a/src/storm/storage/expressions/BooleanLiteralExpression.h +++ b/src/storm/storage/expressions/BooleanLiteralExpression.h @@ -33,7 +33,7 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isBooleanLiteralExpression() const override; /*! * Retrieves the value of the boolean literal. * diff --git a/src/storm/storage/expressions/IfThenElseExpression.cpp b/src/storm/storage/expressions/IfThenElseExpression.cpp index f965a9d6e..535b828e9 100644 --- a/src/storm/storage/expressions/IfThenElseExpression.cpp +++ b/src/storm/storage/expressions/IfThenElseExpression.cpp @@ -91,6 +91,10 @@ namespace storm { boost::any IfThenElseExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } + + bool IfThenElseExpression::isIfThenElseExpression() const { + return true; + } std::shared_ptr IfThenElseExpression::getCondition() const { return this->condition; diff --git a/src/storm/storage/expressions/IfThenElseExpression.h b/src/storm/storage/expressions/IfThenElseExpression.h index ba9ab9f7b..0d1be1d4b 100644 --- a/src/storm/storage/expressions/IfThenElseExpression.h +++ b/src/storm/storage/expressions/IfThenElseExpression.h @@ -39,7 +39,8 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isIfThenElseExpression() const override; + /*! * Retrieves the condition expression of the if-then-else expression. * diff --git a/src/storm/storage/expressions/IntegerLiteralExpression.cpp b/src/storm/storage/expressions/IntegerLiteralExpression.cpp index 1e8a56f23..6fcecfd80 100644 --- a/src/storm/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storm/storage/expressions/IntegerLiteralExpression.cpp @@ -32,7 +32,12 @@ namespace storm { boost::any IntegerLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool IntegerLiteralExpression::isIntegerLiteralExpression() const { + return true; + } + + int_fast64_t IntegerLiteralExpression::getValue() const { return this->value; } diff --git a/src/storm/storage/expressions/IntegerLiteralExpression.h b/src/storm/storage/expressions/IntegerLiteralExpression.h index 8d9dfda63..9266ea968 100644 --- a/src/storm/storage/expressions/IntegerLiteralExpression.h +++ b/src/storm/storage/expressions/IntegerLiteralExpression.h @@ -32,7 +32,8 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isIntegerLiteralExpression() const override; + /*! * Retrieves the value of the integer literal. * diff --git a/src/storm/storage/expressions/RationalLiteralExpression.cpp b/src/storm/storage/expressions/RationalLiteralExpression.cpp index 242489c0a..6215a5df5 100644 --- a/src/storm/storage/expressions/RationalLiteralExpression.cpp +++ b/src/storm/storage/expressions/RationalLiteralExpression.cpp @@ -37,6 +37,10 @@ namespace storm { boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } + + bool RationalLiteralExpression::isRationalLiteralExpression() const { + return true; + } double RationalLiteralExpression::getValueAsDouble() const { return storm::utility::convertNumber(this->value); diff --git a/src/storm/storage/expressions/RationalLiteralExpression.h b/src/storm/storage/expressions/RationalLiteralExpression.h index 9b4025794..77d8f3703 100644 --- a/src/storm/storage/expressions/RationalLiteralExpression.h +++ b/src/storm/storage/expressions/RationalLiteralExpression.h @@ -49,6 +49,7 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isRationalLiteralExpression() const override; /*! * Retrieves the value of the double literal. diff --git a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp index 40dc3a919..e0afd87e4 100644 --- a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp @@ -52,7 +52,11 @@ namespace storm { boost::any UnaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool UnaryBooleanFunctionExpression::isUnaryBooleanFunctionExpression() const { + return true; + } + void UnaryBooleanFunctionExpression::printToStream(std::ostream& stream) const { stream << "!(" << *this->getOperand() << ")"; } diff --git a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h index 7fc978034..918300d93 100644 --- a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h +++ b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h @@ -37,6 +37,7 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isUnaryBooleanFunctionExpression() const override; /*! * Retrieves the operator associated with this expression. diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp index 9fc2c5639..9e8290c02 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -103,7 +103,11 @@ namespace storm { boost::any UnaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool UnaryNumericalFunctionExpression::isUnaryNumericalFunctionExpression() const { + return true; + } + void UnaryNumericalFunctionExpression::printToStream(std::ostream& stream) const { switch (this->getOperatorType()) { case OperatorType::Minus: stream << "-("; break; diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h index bd863abcf..fe8fbaf45 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h @@ -38,7 +38,8 @@ namespace storm { virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isUnaryNumericalFunctionExpression() const override; + /*! * Retrieves the operator associated with this expression. * diff --git a/src/storm/storage/expressions/VariableExpression.cpp b/src/storm/storage/expressions/VariableExpression.cpp index 8a94f6194..f68837f2f 100644 --- a/src/storm/storage/expressions/VariableExpression.cpp +++ b/src/storm/storage/expressions/VariableExpression.cpp @@ -66,7 +66,11 @@ namespace storm { boost::any VariableExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool VariableExpression::isVariableExpression() const { + return true; + } + void VariableExpression::printToStream(std::ostream& stream) const { stream << this->getVariableName(); } diff --git a/src/storm/storage/expressions/VariableExpression.h b/src/storm/storage/expressions/VariableExpression.h index f1a3bf1ce..708ec35fc 100644 --- a/src/storm/storage/expressions/VariableExpression.h +++ b/src/storm/storage/expressions/VariableExpression.h @@ -36,6 +36,7 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isVariableExpression() const override; /*! * Retrieves the name of the variable associated with this expression.