From 92ee6187fa41695068ad7746ca4ad7830c3b645e Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 6 May 2014 17:20:00 +0200 Subject: [PATCH] Added more query methods to expressions. SparseMatrix now keeps track of non zero entries and models show correct number of transitions by referring to nonzero entries rather than all entries in the matrix. Former-commit-id: 48180be2fe33c7f12ad0ef20b1b7800910a73935 --- src/models/AbstractModel.h | 2 +- src/storage/SparseMatrix.cpp | 29 ++++++++++++---- src/storage/SparseMatrix.h | 10 ++++++ src/storage/expressions/BaseExpression.cpp | 8 +++++ src/storage/expressions/BaseExpression.h | 16 +++++++++ .../BinaryBooleanFunctionExpression.cpp | 10 ++++++ .../BinaryBooleanFunctionExpression.h | 1 + src/storage/expressions/BinaryExpression.cpp | 6 +++- src/storage/expressions/BinaryExpression.h | 1 + .../BinaryNumericalFunctionExpression.cpp | 11 +++++++ .../BinaryNumericalFunctionExpression.h | 1 + .../expressions/BinaryRelationExpression.cpp | 13 +++++++- .../expressions/BinaryRelationExpression.h | 1 + src/storage/expressions/Expression.cpp | 8 +++++ src/storage/expressions/Expression.h | 15 +++++++++ .../expressions/IfThenElseExpression.cpp | 30 +++++++++++++++++ .../expressions/IfThenElseExpression.h | 5 +++ src/storage/expressions/OperatorType.h | 33 +++++++++++++++++++ .../UnaryBooleanFunctionExpression.cpp | 6 ++++ .../UnaryBooleanFunctionExpression.h | 1 + src/storage/expressions/UnaryExpression.cpp | 4 +++ src/storage/expressions/UnaryExpression.h | 1 + .../UnaryNumericalFunctionExpression.cpp | 8 +++++ .../UnaryNumericalFunctionExpression.h | 1 + .../GmmxxDtmcPrctlModelCheckerTest.cpp | 6 ++-- test/functional/parser/AutoParserTest.cpp | 12 +++---- .../parser/DeterministicModelParserTest.cpp | 4 +-- .../GmmxxDtmcPrctModelCheckerTest.cpp | 4 +-- 28 files changed, 224 insertions(+), 23 deletions(-) create mode 100644 src/storage/expressions/OperatorType.h diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 301c806d3..05296c584 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -220,7 +220,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return The number of (non-zero) transitions of the model. */ virtual uint_fast64_t getNumberOfTransitions() const { - return this->getTransitionMatrix().getEntryCount(); + return this->getTransitionMatrix().getNonzeroEntryCount(); } /*! diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 6955ec053..e4d719006 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -218,17 +218,17 @@ namespace storm { } template - SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() { + SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) { + SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), rowGroupIndices(std::move(other.rowGroupIndices)) { + SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), rowGroupIndices(std::move(other.rowGroupIndices)) { // Now update the source matrix other.rowCount = 0; other.columnCount = 0; @@ -236,13 +236,21 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { - // Intentionally left empty. + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { + for (auto const& element : *this) { + if (element.second != storm::utility::constantZero()) { + ++this->nonzeroEntryCount; + } + } } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { - // Intentionally left empty. + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { + for (auto const& element : *this) { + if (element.second != storm::utility::constantZero()) { + ++this->nonzeroEntryCount; + } + } } template @@ -252,6 +260,7 @@ namespace storm { rowCount = other.rowCount; columnCount = other.columnCount; entryCount = other.entryCount; + nonzeroEntryCount = other.nonzeroEntryCount; columnsAndValues = other.columnsAndValues; rowIndications = other.rowIndications; @@ -268,6 +277,7 @@ namespace storm { rowCount = other.rowCount; columnCount = other.columnCount; entryCount = other.entryCount; + nonzeroEntryCount = other.nonzeroEntryCount; columnsAndValues = std::move(other.columnsAndValues); rowIndications = std::move(other.rowIndications); @@ -330,6 +340,11 @@ namespace storm { return entryCount; } + template + uint_fast64_t SparseMatrix::getNonzeroEntryCount() const { + return nonzeroEntryCount; + } + template uint_fast64_t SparseMatrix::getRowGroupCount() const { return rowGroupIndices.size() - 1; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index f85dfdd52..b8b8b80d3 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -339,6 +339,13 @@ namespace storm { */ uint_fast64_t getEntryCount() const; + /*! + * Returns the number of nonzero entries in the matrix. + * + * @return The number of nonzero entries in the matrix. + */ + uint_fast64_t getNonzeroEntryCount() const; + /*! * Returns the number of row groups in the matrix. * @@ -651,6 +658,9 @@ namespace storm { // The number of entries in the matrix. uint_fast64_t entryCount; + // The number of nonzero entries in the matrix. + uint_fast64_t nonzeroEntryCount; + // The storage for the columns and values of all entries in the matrix. std::vector> columnsAndValues; diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index 2aef5ab6e..c2f4a5ac3 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -49,6 +49,10 @@ namespace storm { LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access identifier of non-constant, non-variable expression."); } + OperatorType BaseExpression::getOperator() const { + LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access operator of non-function application expression."); + } + bool BaseExpression::containsVariables() const { return false; } @@ -69,6 +73,10 @@ namespace storm { return false; } + bool BaseExpression::isFunctionApplication() const { + return false; + } + std::shared_ptr BaseExpression::getSharedPointer() const { return this->shared_from_this(); } diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index 79dc09c1d..6a02b35ab 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/src/storage/expressions/BaseExpression.h @@ -8,6 +8,7 @@ #include "src/storage/expressions/Valuation.h" #include "src/storage/expressions/ExpressionVisitor.h" +#include "src/storage/expressions/OperatorType.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/utility/OsDetection.h" @@ -96,6 +97,14 @@ namespace storm { */ virtual std::string const& getIdentifier() const; + /*! + * Retrieves the operator of a function application. This is only legal to call if the expression is + * function application. + * + * @return The operator associated with the function application. + */ + virtual OperatorType getOperator() const; + /*! * Retrieves whether the expression contains a variable. * @@ -131,6 +140,13 @@ namespace storm { */ virtual bool isFalse() const; + /*! + * Checks if the expression is a function application (of any sort). + * + * @return True iff the expression is a function application. + */ + virtual bool isFunctionApplication() const; + /*! * Retrieves the set of all variables that appear in the expression. * diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index e270293a8..061c231af 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -13,6 +13,16 @@ namespace storm { return this->operatorType; } + storm::expressions::OperatorType BinaryBooleanFunctionExpression::getOperator() const { + switch (this->getOperatorType()) { + case OperatorType::And: return storm::expressions::OperatorType::And; break; + case OperatorType::Or: return storm::expressions::OperatorType::Or; break; + case OperatorType::Xor: return storm::expressions::OperatorType::Xor; break; + case OperatorType::Implies: return storm::expressions::OperatorType::Implies; break; + case OperatorType::Iff: return storm::expressions::OperatorType::Iff; break; + } + } + bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const { LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h index 8b1bb7437..2a1d2417d 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h @@ -33,6 +33,7 @@ namespace storm { virtual ~BinaryBooleanFunctionExpression() = default; // Override base class methods. + virtual storm::expressions::OperatorType getOperator() const override; virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/BinaryExpression.cpp b/src/storage/expressions/BinaryExpression.cpp index 0ca77aa0c..4d3c4be81 100644 --- a/src/storage/expressions/BinaryExpression.cpp +++ b/src/storage/expressions/BinaryExpression.cpp @@ -9,6 +9,10 @@ namespace storm { // Intentionally left empty. } + bool BinaryExpression::isFunctionApplication() const { + return true; + } + bool BinaryExpression::containsVariables() const { return this->getFirstOperand()->containsVariables() || this->getSecondOperand()->containsVariables(); } @@ -34,7 +38,7 @@ namespace storm { std::shared_ptr BinaryExpression::getOperand(uint_fast64_t operandIndex) const { LOG_THROW(operandIndex < 2, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2."); - if (operandIndex == 1) { + if (operandIndex == 0) { return this->getFirstOperand(); } else { return this->getSecondOperand(); diff --git a/src/storage/expressions/BinaryExpression.h b/src/storage/expressions/BinaryExpression.h index dd81343ac..75c9283cb 100644 --- a/src/storage/expressions/BinaryExpression.h +++ b/src/storage/expressions/BinaryExpression.h @@ -30,6 +30,7 @@ namespace storm { virtual ~BinaryExpression() = default; // Override base class methods. + virtual bool isFunctionApplication() const override; virtual bool containsVariables() const override; virtual uint_fast64_t getArity() const override; virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp index 225bea963..f6172821d 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -14,6 +14,17 @@ namespace storm { return this->operatorType; } + storm::expressions::OperatorType BinaryNumericalFunctionExpression::getOperator() const { + switch (this->getOperatorType()) { + case OperatorType::Plus: return storm::expressions::OperatorType::Plus; break; + case OperatorType::Minus: return storm::expressions::OperatorType::Minus; break; + case OperatorType::Times: return storm::expressions::OperatorType::Times; break; + case OperatorType::Divide: return storm::expressions::OperatorType::Divide; break; + case OperatorType::Min: return storm::expressions::OperatorType::Min; break; + case OperatorType::Max: return storm::expressions::OperatorType::Max; break; + } + } + int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const { LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storage/expressions/BinaryNumericalFunctionExpression.h index 4e8573a4c..13ee489df 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.h +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.h @@ -33,6 +33,7 @@ namespace storm { virtual ~BinaryNumericalFunctionExpression() = default; // Override base class methods. + virtual storm::expressions::OperatorType getOperator() const override; virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override; virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp index 7e48c2286..f31f97fce 100644 --- a/src/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storage/expressions/BinaryRelationExpression.cpp @@ -8,7 +8,18 @@ namespace storm { BinaryRelationExpression::BinaryRelationExpression(ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand, RelationType relationType) : BinaryExpression(returnType, firstOperand, secondOperand), relationType(relationType) { // Intentionally left empty. } - + + storm::expressions::OperatorType BinaryRelationExpression::getOperator() const { + switch (this->getRelationType()) { + case RelationType::Equal: return storm::expressions::OperatorType::Equal; break; + case RelationType::NotEqual: return storm::expressions::OperatorType::NotEqual; break; + case RelationType::Less: return storm::expressions::OperatorType::Less; break; + case RelationType::LessOrEqual: return storm::expressions::OperatorType::LessOrEqual; break; + case RelationType::Greater: return storm::expressions::OperatorType::Greater; break; + case RelationType::GreaterOrEqual: return storm::expressions::OperatorType::GreaterOrEqual; break; + } + } + bool BinaryRelationExpression::evaluateAsBool(Valuation const* valuation) const { LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); diff --git a/src/storage/expressions/BinaryRelationExpression.h b/src/storage/expressions/BinaryRelationExpression.h index b88ef71f9..4e03a598e 100644 --- a/src/storage/expressions/BinaryRelationExpression.h +++ b/src/storage/expressions/BinaryRelationExpression.h @@ -33,6 +33,7 @@ namespace storm { virtual ~BinaryRelationExpression() = default; // Override base class methods. + virtual storm::expressions::OperatorType getOperator() const override; virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 863d630f3..e30b53927 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -55,6 +55,14 @@ namespace storm { return Expression(this->getBaseExpression().simplify()); } + OperatorType Expression::getOperator() const { + return this->getBaseExpression().getOperator(); + } + + bool Expression::isFunctionApplication() const { + return this->getBaseExpression().isFunctionApplication(); + } + uint_fast64_t Expression::getArity() const { return this->getBaseExpression().getArity(); } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 44f3e5728..0c55408dc 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -157,6 +157,21 @@ namespace storm { */ Expression simplify(); + /*! + * Retrieves the operator of a function application. This is only legal to call if the expression is + * function application. + * + * @return The operator associated with the function application. + */ + OperatorType getOperator() const; + + /*! + * Checks if the expression is a function application (of any sort). + * + * @return True iff the expression is a function application. + */ + bool isFunctionApplication() const; + /*! * Retrieves the arity of the expression. * diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp index 4cc028b3c..bbd0b28d2 100644 --- a/src/storage/expressions/IfThenElseExpression.cpp +++ b/src/storage/expressions/IfThenElseExpression.cpp @@ -1,11 +1,41 @@ #include "src/storage/expressions/IfThenElseExpression.h" +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/InvalidAccessException.h" + namespace storm { namespace expressions { IfThenElseExpression::IfThenElseExpression(ExpressionReturnType returnType, std::shared_ptr const& condition, std::shared_ptr const& thenExpression, std::shared_ptr const& elseExpression) : BaseExpression(returnType), condition(condition), thenExpression(thenExpression), elseExpression(elseExpression) { // Intentionally left empty. } + std::shared_ptr IfThenElseExpression::getOperand(uint_fast64_t operandIndex) const { + LOG_THROW(operandIndex < 3, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 3."); + if (operandIndex == 0) { + return this->getCondition(); + } else if (operandIndex == 1) { + return this->getThenExpression(); + } else { + return this->getElseExpression(); + } + } + + OperatorType IfThenElseExpression::getOperator() const { + return OperatorType::Ite; + } + + bool IfThenElseExpression::isFunctionApplication() const { + return true; + } + + bool IfThenElseExpression::containsVariables() const { + return this->getCondition()->containsVariables() || this->getThenExpression()->containsVariables() || this->getElseExpression()->containsVariables(); + } + + uint_fast64_t IfThenElseExpression::getArity() const { + return 3; + } + bool IfThenElseExpression::evaluateAsBool(Valuation const* valuation) const { bool conditionValue = this->condition->evaluateAsBool(valuation); if (conditionValue) { diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h index b44de20be..425633850 100644 --- a/src/storage/expressions/IfThenElseExpression.h +++ b/src/storage/expressions/IfThenElseExpression.h @@ -27,6 +27,11 @@ namespace storm { virtual ~IfThenElseExpression() = default; // Override base class methods. + virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; + virtual OperatorType getOperator() const override; + virtual bool isFunctionApplication() const override; + virtual bool containsVariables() const override; + virtual uint_fast64_t getArity() const override; virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override; virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; diff --git a/src/storage/expressions/OperatorType.h b/src/storage/expressions/OperatorType.h new file mode 100644 index 000000000..8a4f199aa --- /dev/null +++ b/src/storage/expressions/OperatorType.h @@ -0,0 +1,33 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_OPERATORTYPE_H_ +#define STORM_STORAGE_EXPRESSIONS_OPERATORTYPE_H_ + +namespace storm { + namespace expressions { + // An enum representing all possible operator types. + enum class OperatorType { + And, + Or, + Xor, + Implies, + Iff, + Plus, + Minus, + Times, + Divide, + Min, + Max, + Equal, + NotEqual, + Less, + LessOrEqual, + Greater, + GreaterOrEqual, + Not, + Floor, + Ceil, + Ite + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_OPERATORTYPE_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp index 7e405bb29..1d9e59119 100644 --- a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp @@ -13,6 +13,12 @@ namespace storm { return this->operatorType; } + storm::expressions::OperatorType UnaryBooleanFunctionExpression::getOperator() const { + switch (this->getOperatorType()) { + case OperatorType::Not: return storm::expressions::OperatorType::Not; + } + } + bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const { LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storage/expressions/UnaryBooleanFunctionExpression.h index 1f2800d8e..c69c6f886 100644 --- a/src/storage/expressions/UnaryBooleanFunctionExpression.h +++ b/src/storage/expressions/UnaryBooleanFunctionExpression.h @@ -32,6 +32,7 @@ namespace storm { virtual ~UnaryBooleanFunctionExpression() = default; // Override base class methods. + virtual storm::expressions::OperatorType getOperator() const override; virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp index 62ff442ed..5d8262766 100644 --- a/src/storage/expressions/UnaryExpression.cpp +++ b/src/storage/expressions/UnaryExpression.cpp @@ -9,6 +9,10 @@ namespace storm { // Intentionally left empty. } + bool UnaryExpression::isFunctionApplication() const { + return true; + } + bool UnaryExpression::containsVariables() const { return this->getOperand()->containsVariables(); } diff --git a/src/storage/expressions/UnaryExpression.h b/src/storage/expressions/UnaryExpression.h index 8ad304ce1..a387ad8d5 100644 --- a/src/storage/expressions/UnaryExpression.h +++ b/src/storage/expressions/UnaryExpression.h @@ -26,6 +26,7 @@ namespace storm { virtual ~UnaryExpression() = default; // Override base class methods. + virtual bool isFunctionApplication() const override; virtual bool containsVariables() const override; virtual uint_fast64_t getArity() const override; virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp index 02a4bee30..972f2a24a 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -14,6 +14,14 @@ namespace storm { return this->operatorType; } + storm::expressions::OperatorType UnaryNumericalFunctionExpression::getOperator() const { + switch (this->getOperatorType()) { + case OperatorType::Minus: return storm::expressions::OperatorType::Minus; break; + case OperatorType::Floor: return storm::expressions::OperatorType::Floor; break; + case OperatorType::Ceil: return storm::expressions::OperatorType::Ceil; break; + } + } + int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const { LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storage/expressions/UnaryNumericalFunctionExpression.h index daa0df40f..10b85e63e 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.h +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.h @@ -32,6 +32,7 @@ namespace storm { virtual ~UnaryNumericalFunctionExpression() = default; // Override base class methods. + virtual storm::expressions::OperatorType getOperator() const override; virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override; virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index fdff14a66..dc2d6d703 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -18,7 +18,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 27ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -74,7 +74,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(dtmc->getNumberOfStates(), 8607ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 15113ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -119,7 +119,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 16495ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); diff --git a/test/functional/parser/AutoParserTest.cpp b/test/functional/parser/AutoParserTest.cpp index 3c4927ecd..7c3fcb483 100644 --- a/test/functional/parser/AutoParserTest.cpp +++ b/test/functional/parser/AutoParserTest.cpp @@ -24,7 +24,7 @@ TEST(AutoParserTest, BasicParsing) { // Test if parsed correctly. ASSERT_EQ(storm::models::DTMC, modelPtr->getType()); ASSERT_EQ(12, modelPtr->getNumberOfStates()); - ASSERT_EQ(32, modelPtr->getNumberOfTransitions()); + ASSERT_EQ(26, modelPtr->getNumberOfTransitions()); ASSERT_EQ(1, modelPtr->getInitialStates().getNumberOfSetBits()); ASSERT_TRUE(modelPtr->hasAtomicProposition("three")); ASSERT_FALSE(modelPtr->hasStateRewards()); @@ -56,21 +56,21 @@ TEST(AutoParserTest, Decision) { std::shared_ptr> modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/dtmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"); ASSERT_EQ(storm::models::DTMC, modelPtr->getType()); ASSERT_EQ(12, modelPtr->getNumberOfStates()); - ASSERT_EQ(32, modelPtr->getNumberOfTransitions()); + ASSERT_EQ(26, modelPtr->getNumberOfTransitions()); // Ctmc modelPtr.reset(); modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ctmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"); ASSERT_EQ(storm::models::CTMC, modelPtr->getType()); ASSERT_EQ(12, modelPtr->getNumberOfStates()); - ASSERT_EQ(31, modelPtr->getNumberOfTransitions()); + ASSERT_EQ(26, modelPtr->getNumberOfTransitions()); // Mdp modelPtr.reset(); modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/mdp.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"); ASSERT_EQ(storm::models::MDP, modelPtr->getType()); ASSERT_EQ(12, modelPtr->getNumberOfStates()); - ASSERT_EQ(36, modelPtr->getNumberOfTransitions()); + ASSERT_EQ(28, modelPtr->getNumberOfTransitions()); // Ctmdp // Note: For now we use the Mdp from above just given the ctmdp hint, since the implementation of the Ctmdp model seems not Quite right yet. @@ -80,12 +80,12 @@ TEST(AutoParserTest, Decision) { modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ctmdp.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"); ASSERT_EQ(storm::models::CTMDP, modelPtr->getType()); ASSERT_EQ(12, modelPtr->getNumberOfStates()); - ASSERT_EQ(36, modelPtr->getNumberOfTransitions()); + ASSERT_EQ(28, modelPtr->getNumberOfTransitions()); // MA modelPtr.reset(); modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ma.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"); ASSERT_EQ(storm::models::MA, modelPtr->getType()); ASSERT_EQ(12, modelPtr->getNumberOfStates()); - ASSERT_EQ(35, modelPtr->getNumberOfTransitions()); + ASSERT_EQ(27, modelPtr->getNumberOfTransitions()); } diff --git a/test/functional/parser/DeterministicModelParserTest.cpp b/test/functional/parser/DeterministicModelParserTest.cpp index 4a62e5e6e..1b6fe71db 100644 --- a/test/functional/parser/DeterministicModelParserTest.cpp +++ b/test/functional/parser/DeterministicModelParserTest.cpp @@ -26,7 +26,7 @@ TEST(DeterministicModelParserTest, BasicDtmcParsing) { storm::models::Dtmc dtmc(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew")); ASSERT_EQ(8, dtmc.getNumberOfStates()); - ASSERT_EQ(21, dtmc.getNumberOfTransitions()); + ASSERT_EQ(16, dtmc.getNumberOfTransitions()); ASSERT_EQ(2, dtmc.getInitialStates().getNumberOfSetBits()); ASSERT_TRUE(dtmc.getInitialStates().get(0)); @@ -58,7 +58,7 @@ TEST(DeterministicModelParserTest, BasicCtmcParsing) { storm::models::Ctmc ctmc(storm::parser::DeterministicModelParser::parseCtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew")); ASSERT_EQ(8, ctmc.getNumberOfStates()); - ASSERT_EQ(21, ctmc.getNumberOfTransitions()); + ASSERT_EQ(16, ctmc.getNumberOfTransitions()); ASSERT_EQ(2, ctmc.getInitialStates().getNumberOfSetBits()); ASSERT_TRUE(ctmc.getInitialStates().get(0)); diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 809f602fb..2fddf8702 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(dtmc->getNumberOfStates(), 2036647ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 7362293ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -71,7 +71,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 1574477ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver());