From 0f9c7537784c931ad8fab005d76f9b45fc6dfa0e Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Fri, 6 Feb 2015 16:41:45 +0100 Subject: [PATCH 1/8] Fixed Windows build error Former-commit-id: a59eafdaf8594c159a1b435c6050808a87d7f6e3 --- ...sticModelBisimulationDecompositionTest.cpp | 33 ++++++++++++++++--- 1 file changed, 29 insertions(+), 4 deletions(-) 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::Options options; +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition::Options options; +#else + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; +#endif options.respectedAtomicPropositions = std::set({"one"}); storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, options); @@ -39,8 +43,13 @@ TEST(DeterministicModelBisimulationDecomposition, Die) { auto labelFormula = std::make_shared("one"); auto eventuallyFormula = std::make_shared(labelFormula); + +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); +#else + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); +#endif - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); storm::storage::DeterministicModelBisimulationDecomposition 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::Options options; +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition::Options options; +#else + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; +#endif options.respectedAtomicPropositions = std::set({"observe0Greater1"}); storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, options); @@ -85,7 +98,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { auto labelFormula = std::make_shared("observe0Greater1"); auto eventuallyFormula = std::make_shared(labelFormula); - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); +#else + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); +#endif storm::storage::DeterministicModelBisimulationDecomposition bisim4(*dtmc, options2); ASSERT_NO_THROW(result = bisim4.getQuotient()); @@ -95,7 +112,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { auto probabilityOperatorFormula = std::make_shared(eventuallyFormula); +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition::Options options3(*dtmc, *probabilityOperatorFormula); +#else typename storm::storage::DeterministicModelBisimulationDecomposition::Options options3(*dtmc, *probabilityOperatorFormula); +#endif storm::storage::DeterministicModelBisimulationDecomposition bisim5(*dtmc, options3); ASSERT_NO_THROW(result = bisim5.getQuotient()); @@ -105,7 +126,11 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { auto boundedUntilFormula = std::make_shared(std::make_shared(true), labelFormula, 50); +#ifdef WINDOWS + storm::storage::DeterministicModelBisimulationDecomposition::Options options4(*dtmc, *boundedUntilFormula); +#else typename storm::storage::DeterministicModelBisimulationDecomposition::Options options4(*dtmc, *boundedUntilFormula); +#endif storm::storage::DeterministicModelBisimulationDecomposition bisim6(*dtmc, options4); ASSERT_NO_THROW(result = bisim6.getQuotient()); From 8b1a4b4e5236b3846103e8802d1be8f5c57349df Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Tue, 10 Feb 2015 13:24:21 +0100 Subject: [PATCH 2/8] Quickfix s.t. we have a defined index and don't dereference end() which is bad Former-commit-id: c55bb57dd5d89d282b9713c6d078554439a64da6 --- src/parser/PrismParser.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 { From f5e383722fad767236af945d9716a9145f04932a Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 10 Feb 2015 14:49:29 +0100 Subject: [PATCH 3/8] Fixed use of uninitialized value. Deleted assignment operators for classes derived from BaseExpression. Former-commit-id: 3d6250b3934a30a20693a050ba190d06023fa611 --- .../reachability/SparseDtmcEliminationModelChecker.cpp | 2 +- src/solver/GmmxxLinearEquationSolver.cpp | 3 +-- src/solver/GmmxxLinearEquationSolver.h | 8 ++++---- src/storage/expressions/BaseExpression.h | 4 ++-- .../expressions/BinaryBooleanFunctionExpression.h | 4 ++-- src/storage/expressions/BinaryExpression.h | 4 ++-- .../expressions/BinaryNumericalFunctionExpression.h | 4 ++-- src/storage/expressions/BooleanLiteralExpression.h | 4 ++-- src/storage/expressions/DoubleLiteralExpression.h | 4 ++-- src/storage/expressions/IfThenElseExpression.h | 4 ++-- src/storage/expressions/IntegerLiteralExpression.h | 4 ++-- .../expressions/UnaryBooleanFunctionExpression.h | 4 ++-- src/storage/expressions/UnaryExpression.h | 6 +++--- .../expressions/UnaryNumericalFunctionExpression.h | 4 ++-- src/storage/expressions/VariableExpression.h | 4 ++-- src/utility/cli.h | 10 ++++++++-- src/utility/vector.h | 10 ++-------- 17 files changed, 41 insertions(+), 42 deletions(-) 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 - GmmxxLinearEquationSolver::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::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 GmmxxLinearEquationSolver::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 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 result; if (model->getType() == storm::models::DTMC) { std::shared_ptr> dtmc = model->as>(); -// storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); - result = modelchecker.check(*formula.get()); + if (modelchecker.canHandle(*formula.get())) { + result = modelchecker.check(*formula.get()); + } else { + storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker2(*dtmc); + if (modelchecker2.canHandle(*formula.get())) { + modelchecker2.check(*formula.get()); + } + } } else if (model->getType() == storm::models::MDP) { std::shared_ptr> mdp = model->as>(); storm::modelchecker::SparseMdpPrctlModelChecker 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 bool equalModuloPrecision(std::vector const& vectorLeft, std::vector 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 bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector 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)) { From 07ddaa314c41f27d80f33fe3ac68fcd9d29bbaaa Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Tue, 10 Feb 2015 17:12:31 +0100 Subject: [PATCH 4/8] User declared move constructor and move assignment, as they are currently required to ensure pointer validity. Former-commit-id: 5e239c60ccefde54de4bffb8e5d38f7570c7cba7 --- ...erministicModelBisimulationDecomposition.h | 39 +++++++++++++++++-- 1 file changed, 36 insertions(+), 3 deletions(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index eae63f442..55cc2241c 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -275,9 +275,42 @@ 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; +#ifdef WINDOWS + Partition(Partition&& other) + : blocks(), numberOfBlocks(other.numberOfBlocks), stateToBlockMapping(), statesAndValues(), positions(), keepSilentProbabilities(other.keepSilentProbabilities), silentProbabilities() + { + //std::cout << "Partition(Partition&& other)" << std::endl; + //std::cout.flush(); + blocks.swap(other.blocks); + other.numberOfBlocks = 0; + stateToBlockMapping.swap(other.stateToBlockMapping); + statesAndValues.swap(other.statesAndValues); + positions.swap(other.positions); + silentProbabilities.swap(other.silentProbabilities); + } + Partition& operator=(Partition&& other) + { + //std::cout << "Partition& operator=(Partition&& other)" << std::endl; + //std::cout.flush(); + blocks.clear(); + blocks.swap(other.blocks); + numberOfBlocks = other.numberOfBlocks; + other.numberOfBlocks = 0; + stateToBlockMapping.clear(); + stateToBlockMapping.swap(other.stateToBlockMapping); + statesAndValues.clear(); + statesAndValues.swap(other.statesAndValues); + positions.clear(); + positions.swap(other.positions); + keepSilentProbabilities = other.keepSilentProbabilities; + silentProbabilities.clear(); + silentProbabilities.swap(other.silentProbabilities); + + return *this; + } +#else + Partition(Partition&& other) = default; + Partition& operator=(Partition&& other) = default; #endif /*! From e41922347de632755ef90778e2a387ff93679da7 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Tue, 10 Feb 2015 19:09:46 +0100 Subject: [PATCH 5/8] Adapted ExpressionTest.cpp to weird behavior of windows when using temporary shared_ptr in make_pair in initializer_list. Now using const_pointer_cast instead of static_cast to modify shared pointers. (Although it worked with static_casts, but you never know) Former-commit-id: d42487bb0c4cc479a4b349a2aa12b0ccf9963869 --- src/storage/expressions/SubstitutionVisitor.cpp | 12 ++++++------ test/functional/storage/ExpressionTest.cpp | 5 +++++ 2 files changed, 11 insertions(+), 6 deletions(-) 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(new IfThenElseExpression(expression.getManager(), expression.getType(), conditionExpression, thenExpression, elseExpression))); + return std::const_pointer_cast(std::shared_ptr(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(new BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType()))); + return std::const_pointer_cast(std::shared_ptr(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(new BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType()))); + return std::const_pointer_cast(std::shared_ptr(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(new BinaryRelationExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getRelationType()))); + return std::const_pointer_cast(std::shared_ptr(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(new UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType()))); + return std::const_pointer_cast(std::shared_ptr(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(new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType()))); + return std::const_pointer_cast(std::shared_ptr(new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType()))); } } 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 substution = { std::make_pair(manager->getVariable("y"), twopointseven), std::make_pair(manager->getVariable("x"), manager->boolean(true)) }; +#else std::map 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()); From 4b44e625d08e547ca569dfbe11f6c914780215ea Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Tue, 10 Feb 2015 23:04:18 +0100 Subject: [PATCH 6/8] Adapted Death-Tests in BitVectorTest.cpp to return codes upon assertion failure on Windows and deactivate them everywhere if the macro NDEBUG is defined (as that disables assertions) Former-commit-id: be04a49e573abaa29a21033183af113888182db0 --- test/functional/storage/BitVectorTest.cpp | 26 ++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index ff06e1815..7329e3705 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; + SUCCESS(); +#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; + SUCCESS(); +#endif } TEST(BitVectorTest, OperatorNot) { From 00ddce497d69d3c38a0e3ec9feae031c4fe85bb8 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Tue, 10 Feb 2015 23:20:15 +0100 Subject: [PATCH 7/8] corrected identifier name. One should actually read documentation, not just look at it... Former-commit-id: 69d81544966de00a5c142aab7bae3f1a20dea132 --- test/functional/storage/BitVectorTest.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index 7329e3705..2e3cb8385 100644 --- a/test/functional/storage/BitVectorTest.cpp +++ b/test/functional/storage/BitVectorTest.cpp @@ -130,7 +130,7 @@ TEST(BitVectorDeathTest, GetSetAssertion) { #endif #else std::cerr << "WARNING: Not testing GetSetAssertions, as they are disabled in release mode." << std::endl; - SUCCESS(); + SUCCEED(); #endif } @@ -322,7 +322,7 @@ TEST(BitVectorTest, OperatorModulo) { #endif #else std::cerr << "WARNING: Not testing OperatorModulo size check, as assertions are disabled in release mode." << std::endl; - SUCCESS(); + SUCCEED(); #endif } From 56ea5fca147928c711560991cccd14d404be5693 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 11 Feb 2015 14:40:18 +0100 Subject: [PATCH 8/8] Included move-construction and move-assignment for partition. Former-commit-id: 8ed399c30807617ce36b49c9dac28fe27acbfa21 --- ...erministicModelBisimulationDecomposition.h | 49 ++++++------------- 1 file changed, 16 insertions(+), 33 deletions(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 55cc2241c..4199d39e5 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -275,43 +275,26 @@ namespace storm { Partition() = default; Partition(Partition const& other) = default; Partition& operator=(Partition const& other) = default; -#ifdef WINDOWS - Partition(Partition&& other) - : blocks(), numberOfBlocks(other.numberOfBlocks), stateToBlockMapping(), statesAndValues(), positions(), keepSilentProbabilities(other.keepSilentProbabilities), silentProbabilities() - { - //std::cout << "Partition(Partition&& other)" << std::endl; - //std::cout.flush(); - blocks.swap(other.blocks); - other.numberOfBlocks = 0; - stateToBlockMapping.swap(other.stateToBlockMapping); - statesAndValues.swap(other.statesAndValues); - positions.swap(other.positions); - silentProbabilities.swap(other.silentProbabilities); + + // 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) - { - //std::cout << "Partition& operator=(Partition&& other)" << std::endl; - //std::cout.flush(); - blocks.clear(); - blocks.swap(other.blocks); - numberOfBlocks = other.numberOfBlocks; - other.numberOfBlocks = 0; - stateToBlockMapping.clear(); - stateToBlockMapping.swap(other.stateToBlockMapping); - statesAndValues.clear(); - statesAndValues.swap(other.statesAndValues); - positions.clear(); - positions.swap(other.positions); - keepSilentProbabilities = other.keepSilentProbabilities; - silentProbabilities.clear(); - silentProbabilities.swap(other.silentProbabilities); + + 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; } -#else - Partition(Partition&& other) = default; - Partition& operator=(Partition&& other) = default; -#endif /*! * Splits all blocks of the partition such that afterwards all blocks contain only states with the label