Fixed use of uninitialized value. Deleted assignment operators for classes derived from BaseExpression.

Former-commit-id: 3d6250b393

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -201,7 +201,7 @@ namespace storm {
             storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
             
             // Do some sanity checks to establish some required properties.
-            STORM_LOG_WARN_COND(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination.");
+            // STORM_LOG_WARN_COND(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination.");
             STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
             storm::storage::sparse::state_type initialState = *model.getInitialStates().begin();
             

src/solver/GmmxxLinearEquationSolver.cpp

@@ -16,10 +16,9 @@ namespace storm {
     namespace solver {
         
         template<typename ValueType>
-        GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, Preconditioner preconditioner, bool relative, uint_fast64_t restart) : method(method), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), preconditioner(preconditioner), restart(restart) {
+        GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, Preconditioner preconditioner, bool relative, uint_fast64_t restart) : method(method), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), preconditioner(preconditioner), relative(relative), restart(restart) {
             // Intentionally left empty.
         }
-        
 
         template<typename ValueType>
         GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver() {

src/solver/GmmxxLinearEquationSolver.h

@@ -82,16 +82,16 @@ namespace storm {
             // The required precision for the iterative methods.
             double precision;
 
-            // Sets whether the relative or absolute error is to be considered for convergence detection. Not that this
-            // only applies to the Jacobi method for this solver.
-            bool relative;
-
             // The maximal number of iterations to do before iteration is aborted.
             uint_fast64_t maximalNumberOfIterations;
 
             // The preconditioner to use when solving the linear equation system.
             Preconditioner preconditioner;
 
+            // Sets whether the relative or absolute error is to be considered for convergence detection. Not that this
+            // only applies to the Jacobi method for this solver.
+            bool relative;
+
             // A restart value that determines when restarted methods shall do so.
             uint_fast64_t restart;
         };

src/storage/expressions/BaseExpression.h

@@ -34,10 +34,10 @@ namespace storm {
             
             // Create default versions of constructors and assignments.
             BaseExpression(BaseExpression const&) = default;
-            BaseExpression& operator=(BaseExpression const&) = default;
+            BaseExpression& operator=(BaseExpression const&) = delete;
 #ifndef WINDOWS
             BaseExpression(BaseExpression&&) = default;
-            BaseExpression& operator=(BaseExpression&&) = default;
+            BaseExpression& operator=(BaseExpression&&) = delete;
 #endif
             
             // Make the destructor virtual (to allow destruction via base class pointer) and default it.

src/storage/expressions/BinaryBooleanFunctionExpression.h

@@ -26,10 +26,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) = default;
-            BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other) = default;
+            BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other) = delete;
 #ifndef WINDOWS
             BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression&&) = default;
-            BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression&&) = default;
+            BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression&&) = delete;
 #endif
             virtual ~BinaryBooleanFunctionExpression() = default;
             

src/storage/expressions/BinaryExpression.h

@@ -23,10 +23,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             BinaryExpression(BinaryExpression const& other) = default;
-            BinaryExpression& operator=(BinaryExpression const& other) = default;
+            BinaryExpression& operator=(BinaryExpression const& other) = delete;
 #ifndef WINDOWS
             BinaryExpression(BinaryExpression&&) = default;
-            BinaryExpression& operator=(BinaryExpression&&) = default;
+            BinaryExpression& operator=(BinaryExpression&&) = delete;
 #endif
             virtual ~BinaryExpression() = default;
 

src/storage/expressions/BinaryNumericalFunctionExpression.h

@@ -26,10 +26,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) = default;
-            BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other) = default;
+            BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other) = delete;
 #ifndef WINDOWS
             BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression&&) = default;
-            BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression&&) = default;
+            BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression&&) = delete;
 #endif
             virtual ~BinaryNumericalFunctionExpression() = default;
             

src/storage/expressions/BooleanLiteralExpression.h

@@ -18,10 +18,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             BooleanLiteralExpression(BooleanLiteralExpression const& other) = default;
-            BooleanLiteralExpression& operator=(BooleanLiteralExpression const& other) = default;
+            BooleanLiteralExpression& operator=(BooleanLiteralExpression const& other) = delete;
 #ifndef WINDOWS
             BooleanLiteralExpression(BooleanLiteralExpression&&) = default;
-            BooleanLiteralExpression& operator=(BooleanLiteralExpression&&) = default;
+            BooleanLiteralExpression& operator=(BooleanLiteralExpression&&) = delete;
 #endif
             virtual ~BooleanLiteralExpression() = default;
 

src/storage/expressions/DoubleLiteralExpression.h

@@ -18,10 +18,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             DoubleLiteralExpression(DoubleLiteralExpression const& other) = default;
-            DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = default;
+            DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete;
 #ifndef WINDOWS
             DoubleLiteralExpression(DoubleLiteralExpression&&) = default;
-            DoubleLiteralExpression& operator=(DoubleLiteralExpression&&) = default;
+            DoubleLiteralExpression& operator=(DoubleLiteralExpression&&) = delete;
 #endif
             virtual ~DoubleLiteralExpression() = default;
             

src/storage/expressions/IfThenElseExpression.h

@@ -20,10 +20,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             IfThenElseExpression(IfThenElseExpression const& other) = default;
-            IfThenElseExpression& operator=(IfThenElseExpression const& other) = default;
+            IfThenElseExpression& operator=(IfThenElseExpression const& other) = delete;
 #ifndef WINDOWS
             IfThenElseExpression(IfThenElseExpression&&) = default;
-            IfThenElseExpression& operator=(IfThenElseExpression&&) = default;
+            IfThenElseExpression& operator=(IfThenElseExpression&&) = delete;
 #endif
             virtual ~IfThenElseExpression() = default;
             

src/storage/expressions/IntegerLiteralExpression.h

@@ -18,10 +18,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             IntegerLiteralExpression(IntegerLiteralExpression const& other) = default;
-            IntegerLiteralExpression& operator=(IntegerLiteralExpression const& other) = default;
+            IntegerLiteralExpression& operator=(IntegerLiteralExpression const& other) = delete;
 #ifndef WINDOWS
             IntegerLiteralExpression(IntegerLiteralExpression&&) = default;
-            IntegerLiteralExpression& operator=(IntegerLiteralExpression&&) = default;
+            IntegerLiteralExpression& operator=(IntegerLiteralExpression&&) = delete;
 #endif
             virtual ~IntegerLiteralExpression() = default;
             

src/storage/expressions/UnaryBooleanFunctionExpression.h

@@ -25,10 +25,10 @@ namespace storm {
 
             // Instantiate constructors and assignments with their default implementations.
             UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& other) = default;
-            UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression const& other) = default;
+            UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression const& other) = delete;
 #ifndef WINDOWS
             UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression&&) = default;
-            UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression&&) = default;
+            UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression&&) = delete;
 #endif
             virtual ~UnaryBooleanFunctionExpression() = default;
             

src/storage/expressions/UnaryExpression.h

@@ -18,11 +18,11 @@ namespace storm {
             UnaryExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr<BaseExpression const> const& operand);
 
             // Instantiate constructors and assignments with their default implementations.
-            UnaryExpression(UnaryExpression const& other);
-            UnaryExpression& operator=(UnaryExpression const& other);
+            UnaryExpression(UnaryExpression const& other) = default;
+            UnaryExpression& operator=(UnaryExpression const& other) = delete;
 #ifndef WINDOWS
             UnaryExpression(UnaryExpression&&) = default;
-            UnaryExpression& operator=(UnaryExpression&&) = default;
+            UnaryExpression& operator=(UnaryExpression&&) = delete;
 #endif
             virtual ~UnaryExpression() = default;
             

src/storage/expressions/UnaryNumericalFunctionExpression.h

@@ -25,10 +25,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& other) = default;
-            UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression const& other) = default;
+            UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression const& other) = delete;
 #ifndef WINDOWS
             UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression&&) = default;
-            UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression&&) = default;
+            UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression&&) = delete;
 #endif
             virtual ~UnaryNumericalFunctionExpression() = default;
             

src/storage/expressions/VariableExpression.h

@@ -19,10 +19,10 @@ namespace storm {
             
             // Instantiate constructors and assignments with their default implementations.
             VariableExpression(VariableExpression const&) = default;
-            VariableExpression& operator=(VariableExpression const&) = default;
+            VariableExpression& operator=(VariableExpression const&) = delete;
 #ifndef WINDOWS
             VariableExpression(VariableExpression&&) = default;
-            VariableExpression& operator=(VariableExpression&&) = default;
+            VariableExpression& operator=(VariableExpression&&) = delete;
 #endif
             virtual ~VariableExpression() = default;
 

src/utility/cli.h

@@ -385,9 +385,15 @@ namespace storm {
                     std::unique_ptr<storm::modelchecker::CheckResult> result;
                     if (model->getType() == storm::models::DTMC) {
                         std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
-//                        storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
                         storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
-                        result = modelchecker.check(*formula.get());
+                        if (modelchecker.canHandle(*formula.get())) {
+                            result = modelchecker.check(*formula.get());
+                        } else {
+                            storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker2(*dtmc);
+                            if (modelchecker2.canHandle(*formula.get())) {
+                                modelchecker2.check(*formula.get());
+                            }
+                        }
                     } else if (model->getType() == storm::models::MDP) {
                         std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
                         storm::modelchecker::SparseMdpPrctlModelChecker<double> modelchecker(*mdp);

src/utility/vector.h

@@ -347,10 +347,7 @@ namespace storm {
              */
             template<class T>
             bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T precision, bool relativeError) {
-                if (vectorLeft.size() != vectorRight.size()) {
-                    LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible.");
-                    throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible.";
-                }
+                STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
                 
                 for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) {
                     if (!equalModuloPrecision(vectorLeft[i], vectorRight[i], precision, relativeError)) {
@@ -374,10 +371,7 @@ namespace storm {
              */
             template<class T>
             bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T precision, bool relativeError) {
-                if (vectorLeft.size() != vectorRight.size()) {
-                    LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible.");
-                    throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible.";
-                }
+                STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
                 
                 for (uint_fast64_t position : positions) {
                     if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {