diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 2a25a7dff..e7fd5a988 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/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();
diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp
index 4815b5b2b..695beb683 100644
--- a/src/solver/GmmxxLinearEquationSolver.cpp
+++ b/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() {
diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h
index 63f97a9cb..ac3adfdb2 100644
--- a/src/solver/GmmxxLinearEquationSolver.h
+++ b/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;
};
diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h
index 6a5a0d6b6..0a853c1eb 100644
--- a/src/storage/expressions/BaseExpression.h
+++ b/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.
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h
index 6eaefcbb6..d49658c7e 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.h
+++ b/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;
diff --git a/src/storage/expressions/BinaryExpression.h b/src/storage/expressions/BinaryExpression.h
index 344a50182..39800c730 100644
--- a/src/storage/expressions/BinaryExpression.h
+++ b/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;
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storage/expressions/BinaryNumericalFunctionExpression.h
index bf69016d0..e3c7d227a 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.h
+++ b/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;
diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h
index cb8f694e6..f5dcb78a1 100644
--- a/src/storage/expressions/BooleanLiteralExpression.h
+++ b/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;
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h
index cb3114e2d..676291a77 100644
--- a/src/storage/expressions/DoubleLiteralExpression.h
+++ b/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;
diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h
index 45c6b7e21..d2503116b 100644
--- a/src/storage/expressions/IfThenElseExpression.h
+++ b/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;
diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h
index 61cbd351c..b4f732b83 100644
--- a/src/storage/expressions/IntegerLiteralExpression.h
+++ b/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;
diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storage/expressions/UnaryBooleanFunctionExpression.h
index 7502521e0..d13761c26 100644
--- a/src/storage/expressions/UnaryBooleanFunctionExpression.h
+++ b/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;
diff --git a/src/storage/expressions/UnaryExpression.h b/src/storage/expressions/UnaryExpression.h
index 793077545..8c79eda31 100644
--- a/src/storage/expressions/UnaryExpression.h
+++ b/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;
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storage/expressions/UnaryNumericalFunctionExpression.h
index 3b79d223d..f9e2ab148 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.h
+++ b/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;
diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h
index 35cc6efab..cfc65fd31 100644
--- a/src/storage/expressions/VariableExpression.h
+++ b/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;
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 9463560d8..0b2d1bf78 100644
--- a/src/utility/cli.h
+++ b/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);
diff --git a/src/utility/vector.h b/src/utility/vector.h
index 811e561be..d7e62787d 100644
--- a/src/utility/vector.h
+++ b/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)) {