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());