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: 48180be2fe

src/models/AbstractModel.h

@@ -220,7 +220,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * @return The number of (non-zero) transitions of the model.
 		 */
 		virtual uint_fast64_t getNumberOfTransitions() const {
-			return this->getTransitionMatrix().getEntryCount();
+			return this->getTransitionMatrix().getNonzeroEntryCount();
 		}
 
         /*!

src/storage/SparseMatrix.cpp

@@ -218,17 +218,17 @@ namespace storm {
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() {
+        SparseMatrix<T>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() {
             // Intentionally left empty.
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix(SparseMatrix<T> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) {
+        SparseMatrix<T>::SparseMatrix(SparseMatrix<T> 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<typename T>
-        SparseMatrix<T>::SparseMatrix(SparseMatrix<T>&& 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<T>::SparseMatrix(SparseMatrix<T>&& 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<typename T>
-        SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) {
-            // Intentionally left empty.
+        SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues, std::vector<uint_fast64_t> 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<T>()) {
+                    ++this->nonzeroEntryCount;
+                }
+            }
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues, std::vector<uint_fast64_t>&& 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<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues, std::vector<uint_fast64_t>&& 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<T>()) {
+                    ++this->nonzeroEntryCount;
+                }
+            }
         }
                 
         template<typename T>
@@ -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<typename T>
+        uint_fast64_t SparseMatrix<T>::getNonzeroEntryCount() const {
+            return nonzeroEntryCount;
+        }
+        
         template<typename T>
         uint_fast64_t SparseMatrix<T>::getRowGroupCount() const {
             return rowGroupIndices.size() - 1;

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<std::pair<uint_fast64_t, T>> columnsAndValues;
             

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 const> BaseExpression::getSharedPointer() const {
             return this->shared_from_this();
         }

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.
              *

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.");
             

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<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;

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

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<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;

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.");
             

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<BaseExpression const> simplify() const override;

src/storage/expressions/BinaryRelationExpression.cpp

@@ -8,7 +8,18 @@ namespace storm {
         BinaryRelationExpression::BinaryRelationExpression(ExpressionReturnType returnType, std::shared_ptr<BaseExpression const> const& firstOperand, std::shared_ptr<BaseExpression const> 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.");
 

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<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;

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

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.
              *

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<BaseExpression const> const& condition, std::shared_ptr<BaseExpression const> const& thenExpression, std::shared_ptr<BaseExpression const> const& elseExpression) : BaseExpression(returnType), condition(condition), thenExpression(thenExpression), elseExpression(elseExpression) {
             // Intentionally left empty.
         }
         
+        std::shared_ptr<BaseExpression const> 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) {

src/storage/expressions/IfThenElseExpression.h

@@ -27,6 +27,11 @@ namespace storm {
             virtual ~IfThenElseExpression() = default;
             
             // Override base class methods.
+            virtual std::shared_ptr<BaseExpression const> 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;

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_ */

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.");
 

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<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;

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

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<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;

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.");
 

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<BaseExpression const> simplify() const override;

test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp

@@ -18,7 +18,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
 
 	ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 27ull);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
 
 	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
 
@@ -74,7 +74,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
 
 	ASSERT_EQ(dtmc->getNumberOfStates(), 8607ull);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460ull);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 15113ull);
 
 	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
 
@@ -119,7 +119,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
 
 	ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894ull);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 16495ull);
 
 	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
 

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<storm::models::AbstractModel<double>> 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());
 }

test/functional/parser/DeterministicModelParserTest.cpp

@@ -26,7 +26,7 @@ TEST(DeterministicModelParserTest, BasicDtmcParsing) {
 	storm::models::Dtmc<double> 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<double> 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));

test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp

@@ -17,7 +17,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
 
 	ASSERT_EQ(dtmc->getNumberOfStates(), 2036647ull);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900ull);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 7362293ull);
 
 	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
 
@@ -71,7 +71,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
 
 	ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810ull);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 1574477ull);
 
 	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());