diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index f7cc0a274..4769ba873 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/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 6426f0e16..3db49eb16 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -343,7 +343,11 @@ namespace storm {
storm::prism::TransitionReward PrismParser::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const {
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
STORM_LOG_THROW(actionName.empty() || nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'.");
- return storm::prism::TransitionReward(nameIndexPair->second, actionName, statePredicateExpression, rewardValueExpression, this->getFilename());
+ if (nameIndexPair == globalProgramInformation.actionIndices.end() && actionName.empty()) {
+ return storm::prism::TransitionReward(0, actionName, statePredicateExpression, rewardValueExpression, this->getFilename());
+ } else {
+ return storm::prism::TransitionReward(nameIndexPair->second, actionName, statePredicateExpression, rewardValueExpression, this->getFilename());
+ }
}
storm::prism::Assignment PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const {
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/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
index eae63f442..4199d39e5 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -275,10 +275,26 @@ namespace storm {
Partition() = default;
Partition(Partition const& other) = default;
Partition& operator=(Partition const& other) = default;
-#ifndef WINDOWS
- Partition(Partition&& other) = default;
- Partition& operator=(Partition&& other) = default;
-#endif
+
+ // Define move-construct and move-assignment explicitly to make sure they exist (as they are vital to
+ // keep validity of pointers.
+ Partition(Partition&& other) : blocks(std::move(other.blocks)), numberOfBlocks(other.numberOfBlocks), stateToBlockMapping(std::move(other.stateToBlockMapping)), statesAndValues(std::move(other.statesAndValues)), positions(std::move(other.positions)), keepSilentProbabilities(other.keepSilentProbabilities), silentProbabilities(std::move(other.silentProbabilities)) {
+ // Intentionally left empty.
+ }
+
+ Partition& operator=(Partition&& other) {
+ if (this != &other) {
+ blocks = std::move(other.blocks);
+ numberOfBlocks = other.numberOfBlocks;
+ stateToBlockMapping = std::move(other.stateToBlockMapping);
+ statesAndValues = std::move(other.statesAndValues);
+ positions = std::move(other.positions);
+ keepSilentProbabilities = other.keepSilentProbabilities;
+ silentProbabilities = std::move(other.silentProbabilities);
+ }
+
+ return *this;
+ }
/*!
* Splits all blocks of the partition such that afterwards all blocks contain only states with the label
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/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp
index 4f26d7e1a..c736de156 100644
--- a/src/storage/expressions/SubstitutionVisitor.cpp
+++ b/src/storage/expressions/SubstitutionVisitor.cpp
@@ -27,7 +27,7 @@ namespace storm {
if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) {
return expression.getSharedPointer();
} else {
- return static_cast<std::shared_ptr<BaseExpression const>>(std::shared_ptr<BaseExpression>(new IfThenElseExpression(expression.getManager(), expression.getType(), conditionExpression, thenExpression, elseExpression)));
+ return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new IfThenElseExpression(expression.getManager(), expression.getType(), conditionExpression, thenExpression, elseExpression)));
}
}
@@ -40,7 +40,7 @@ namespace storm {
if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
return expression.getSharedPointer();
} else {
- return static_cast<std::shared_ptr<BaseExpression const>>(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
+ return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
}
}
@@ -53,7 +53,7 @@ namespace storm {
if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
return expression.getSharedPointer();
} else {
- return static_cast<std::shared_ptr<BaseExpression const>>(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
+ return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
}
}
@@ -66,7 +66,7 @@ namespace storm {
if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
return expression.getSharedPointer();
} else {
- return static_cast<std::shared_ptr<BaseExpression const>>(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getRelationType())));
+ return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getRelationType())));
}
}
@@ -89,7 +89,7 @@ namespace storm {
if (operandExpression.get() == expression.getOperand().get()) {
return expression.getSharedPointer();
} else {
- return static_cast<std::shared_ptr<BaseExpression const>>(std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
+ return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
}
}
@@ -101,7 +101,7 @@ namespace storm {
if (operandExpression.get() == expression.getOperand().get()) {
return expression.getSharedPointer();
} else {
- return static_cast<std::shared_ptr<BaseExpression const>>(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
+ return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
}
}
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 32539dade..1961fc738 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -392,9 +392,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 95209ed79..91e9ba0c7 100644
--- a/src/utility/vector.h
+++ b/src/utility/vector.h
@@ -346,7 +346,7 @@ namespace storm {
*/
template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T precision, bool relativeError) {
- STORM_LOG_THROW(vectorLeft.size() == vectorRight.size(), 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)) {
@@ -370,7 +370,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) {
- STORM_LOG_THROW(vectorLeft.size() == vectorRight.size(), 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)) {
diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp
index ff06e1815..2e3cb8385 100644
--- a/test/functional/storage/BitVectorTest.cpp
+++ b/test/functional/storage/BitVectorTest.cpp
@@ -120,8 +120,18 @@ TEST(BitVectorTest, GetSetInt) {
TEST(BitVectorDeathTest, GetSetAssertion) {
storm::storage::BitVector vector(32);
- EXPECT_DEATH_IF_SUPPORTED(vector.get(32), "");
- EXPECT_DEATH_IF_SUPPORTED(vector.set(32), "");
+#ifndef NDEBUG
+#ifdef WINDOWS
+ EXPECT_EXIT(vector.get(32), ::testing::ExitedWithCode(0), ".*");
+ EXPECT_EXIT(vector.set(32), ::testing::ExitedWithCode(0), ".*");
+#else
+ EXPECT_DEATH_IF_SUPPORTED(vector.get(32), "");
+ EXPECT_DEATH_IF_SUPPORTED(vector.set(32), "");
+#endif
+#else
+ std::cerr << "WARNING: Not testing GetSetAssertions, as they are disabled in release mode." << std::endl;
+ SUCCEED();
+#endif
}
TEST(BitVectorTest, Resize) {
@@ -303,7 +313,17 @@ TEST(BitVectorTest, OperatorModulo) {
vector3.set(i, i % 2 == 0);
}
- EXPECT_DEATH_IF_SUPPORTED(vector1 % vector3, "");
+
+#ifndef NDEBUG
+#ifdef WINDOWS
+ EXPECT_EXIT(vector1 % vector3, ::testing::ExitedWithCode(0), ".*");
+#else
+ EXPECT_DEATH_IF_SUPPORTED(vector1 % vector3, "");
+#endif
+#else
+ std::cerr << "WARNING: Not testing OperatorModulo size check, as assertions are disabled in release mode." << std::endl;
+ SUCCEED();
+#endif
}
TEST(BitVectorTest, OperatorNot) {
diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
index 196cde5b8..63b10a03a 100644
--- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
@@ -17,7 +17,11 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
EXPECT_EQ(13, result->getNumberOfStates());
EXPECT_EQ(20, result->getNumberOfTransitions());
- typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+#ifdef WINDOWS
+ storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+#else
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+#endif
options.respectedAtomicPropositions = std::set<std::string>({"one"});
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, options);
@@ -39,8 +43,13 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+
+#ifdef WINDOWS
+ storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+#else
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+#endif
- typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
ASSERT_NO_THROW(result = bisim4.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
@@ -62,7 +71,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
EXPECT_EQ(334, result->getNumberOfStates());
EXPECT_EQ(546, result->getNumberOfTransitions());
- typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+#ifdef WINDOWS
+ storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+#else
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+#endif
options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, options);
@@ -85,7 +98,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
- typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+#ifdef WINDOWS
+ storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+#else
+ typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+#endif
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
ASSERT_NO_THROW(result = bisim4.getQuotient());
@@ -95,7 +112,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(eventuallyFormula);
+#ifdef WINDOWS
+ storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options3(*dtmc, *probabilityOperatorFormula);
+#else
typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options3(*dtmc, *probabilityOperatorFormula);
+#endif
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim5(*dtmc, options3);
ASSERT_NO_THROW(result = bisim5.getQuotient());
@@ -105,7 +126,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), labelFormula, 50);
+#ifdef WINDOWS
+ storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options4(*dtmc, *boundedUntilFormula);
+#else
typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options4(*dtmc, *boundedUntilFormula);
+#endif
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim6(*dtmc, options4);
ASSERT_NO_THROW(result = bisim6.getQuotient());
diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp
index 787a5a6d5..a54debffc 100644
--- a/test/functional/storage/ExpressionTest.cpp
+++ b/test/functional/storage/ExpressionTest.cpp
@@ -275,7 +275,12 @@ TEST(Expression, SubstitutionTest) {
storm::expressions::Expression tempExpression;
ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
+#ifdef WINDOWS
+ storm::expressions::Expression twopointseven = manager->rational(2.7);
+ std::map<storm::expressions::Variable, storm::expressions::Expression> substution = { std::make_pair(manager->getVariable("y"), twopointseven), std::make_pair(manager->getVariable("x"), manager->boolean(true)) };
+#else
std::map<storm::expressions::Variable, storm::expressions::Expression> substution = { std::make_pair(manager->getVariable("y"), manager->rational(2.7)), std::make_pair(manager->getVariable("x"), manager->boolean(true)) };
+#endif
storm::expressions::Expression substitutedExpression;
ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
EXPECT_TRUE(substitutedExpression.simplify().isTrue());