diff --git a/CMakeLists.txt b/CMakeLists.txt index c0179e39d..0ea314db2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -116,7 +116,7 @@ if(CMAKE_COMPILER_IS_GNUCC) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops") add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -Wno-deprecated-declarations") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs") set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations") # Turn on popcnt instruction if desired (yes by default) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 4315bfdde..8b3dbffa0 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -223,7 +223,7 @@ namespace storm { int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); - STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); + STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } // Check that we processed all assignments. diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 7bec64e63..f7891ef5e 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -961,9 +961,6 @@ namespace storm { boost::container::flat_set usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation); usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end()); - // Display achieved probability. - std::pair initialStateProbabilityPair = getReachabilityProbability(*solver, labeledMdp, variableInformation); - // (5) Return result. return usedLabelSet; } diff --git a/src/settings/ArgumentBase.cpp b/src/settings/ArgumentBase.cpp index 93b3169e6..5ccfdbe2f 100644 --- a/src/settings/ArgumentBase.cpp +++ b/src/settings/ArgumentBase.cpp @@ -9,7 +9,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument) { - std::streamsize width = out.width(); + uint_fast64_t width = static_cast(out.width()); uint_fast64_t charactersPrinted = 0; out << std::setw(0) << std::left << "<" << argument.getName() << "> "; charactersPrinted += 2 + argument.getName().length(); diff --git a/src/settings/ArgumentBuilder.h b/src/settings/ArgumentBuilder.h index a6902ab85..18f03334d 100644 --- a/src/settings/ArgumentBuilder.h +++ b/src/settings/ArgumentBuilder.h @@ -176,6 +176,7 @@ return *this; \ } break; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException, "Argument has illegal type."); } private: diff --git a/src/settings/Option.cpp b/src/settings/Option.cpp index 384dc1c04..02a3ca1c9 100644 --- a/src/settings/Option.cpp +++ b/src/settings/Option.cpp @@ -27,7 +27,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& out, Option const& option) { - std::streamsize width = out.width(); + uint_fast64_t width = static_cast(out.width()); uint_fast64_t charactersPrinted = 0; out << std::setw(0) << "--"; diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index dd5761dee..857badfe6 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -45,7 +45,7 @@ namespace storm { // We convert the arguments to a vector of strings and strip off the first element since it refers to the // name of the program. std::vector argumentVector(argc - 1); - for (uint_fast64_t i = 1; i < argc; ++i) { + for (int i = 1; i < argc; ++i) { argumentVector[i - 1] = std::string(argv[i]); } @@ -70,7 +70,6 @@ namespace storm { // Walk through all arguments. for (uint_fast64_t i = 0; i < commandLineArguments.size(); ++i) { - bool existsNextArgument = i < commandLineArguments.size() - 1; std::string const& currentArgument = commandLineArguments[i]; // Check if the given argument is a new option or belongs to a previously given option. diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index a389853c6..35deef1a3 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -156,6 +156,8 @@ namespace storm { std::string NativeLinearEquationSolver::methodToString() const { switch (method) { case SolutionMethod::Jacobi: return "jacobi"; + case SolutionMethod::GaussSeidel: return "gauss-seidel"; + case SolutionMethod::SOR: return "sor"; } } diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index cafa4eb04..8ad635be5 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -10,7 +10,6 @@ namespace storm { SymbolicGameSolver::SymbolicGameSolver(storm::dd::Add const& gameMatrix, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) { // Get the settings object to customize solving. storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::generalSettings(); // Get appropriate settings. maximalNumberOfIterations = settings.getMaximalIterationCount(); diff --git a/src/solver/SymbolicLinearEquationSolver.cpp b/src/solver/SymbolicLinearEquationSolver.cpp index 24a9d12b0..5ec30cbb1 100644 --- a/src/solver/SymbolicLinearEquationSolver.cpp +++ b/src/solver/SymbolicLinearEquationSolver.cpp @@ -15,7 +15,6 @@ namespace storm { SymbolicLinearEquationSolver::SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { // Get the settings object to customize solving. storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::generalSettings(); // Get appropriate settings. maximalNumberOfIterations = settings.getMaximalIterationCount(); diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index 8ea3478b0..3180f0a41 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -1,7 +1,6 @@ #include "src/solver/TopologicalMinMaxLinearEquationSolver.h" #include -#include #include "src/settings/SettingsManager.h" #include "src/utility/vector.h" @@ -103,7 +102,6 @@ namespace storm { #ifdef STORM_HAVE_CUDA STORM_LOG_THROW(resetCudaDevice(), storm::exceptions::InvalidStateException, "Could not reset CUDA Device, can not use CUDA Equation Solver."); - std::chrono::high_resolution_clock::time_point calcStartTime = std::chrono::high_resolution_clock::now(); bool result = false; size_t globalIterations = 0; if (minimize) { @@ -122,11 +120,6 @@ namespace storm { converged = true; } - std::chrono::high_resolution_clock::time_point calcEndTime = std::chrono::high_resolution_clock::now(); - //std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast(calcEndTime - calcStartTime).count() << "ms." << std::endl; - - //std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << globalIterations << " iterations in a single block." << std::endl; - // Check if the solver converged and issue a warning otherwise. if (converged) { LOG4CPLUS_INFO(logger, "Iterative solver converged after " << globalIterations << " iterations."); @@ -138,7 +131,6 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!"; #endif } else { - std::chrono::high_resolution_clock::time_point sccStartTime = std::chrono::high_resolution_clock::now(); storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(this->A, fullSystem, false, false); @@ -151,11 +143,6 @@ namespace storm { std::vector> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, this->A); LOG4CPLUS_INFO(logger, "Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs."); - std::chrono::high_resolution_clock::time_point sccEndTime = std::chrono::high_resolution_clock::now(); - //std::cout << "Computing the SCC Decomposition took " << std::chrono::duration_cast(sccEndTime - sccStartTime).count() << "ms." << std::endl; - - std::chrono::high_resolution_clock::time_point calcStartTime = std::chrono::high_resolution_clock::now(); - std::vector* currentX = nullptr; std::vector* swap = nullptr; size_t currentMaxLocalIterations = 0; @@ -314,9 +301,6 @@ namespace storm { } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converged after " << currentMaxLocalIterations << " iterations."); } - - std::chrono::high_resolution_clock::time_point calcEndTime = std::chrono::high_resolution_clock::now(); - //std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast(calcEndTime - calcStartTime).count() << "ms." << std::endl; } } diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 85a66d02b..c071afc20 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -1376,7 +1376,7 @@ namespace storm { } // Finally, split the block. - Block& nondivergentBlock = partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits()); + partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits()); // Since the remaining states in the block are divergent, we can mark the block as absorbing. // This also guarantees that the self-loop will be added to the state of the quotient diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp index 50e93f567..ce42b6ab4 100644 --- a/src/storage/Distribution.cpp +++ b/src/storage/Distribution.cpp @@ -23,7 +23,6 @@ namespace storm { auto first1 = this->distribution.begin(); auto last1 = this->distribution.end(); auto first2 = other.distribution.begin(); - auto last2 = other.distribution.end(); for (; first1 != last1; ++first1, ++first2) { if (first1->first != first2->first) { diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp index 4e95ea551..de02d793b 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -19,15 +19,17 @@ namespace storm { } storm::expressions::OperatorType BinaryNumericalFunctionExpression::getOperator() const { + storm::expressions::OperatorType result = storm::expressions::OperatorType::Plus; switch (this->getOperatorType()) { - case OperatorType::Plus: return storm::expressions::OperatorType::Plus; break; - case OperatorType::Minus: return storm::expressions::OperatorType::Minus; break; - case OperatorType::Times: return storm::expressions::OperatorType::Times; break; - case OperatorType::Divide: return storm::expressions::OperatorType::Divide; break; - case OperatorType::Min: return storm::expressions::OperatorType::Min; break; - case OperatorType::Max: return storm::expressions::OperatorType::Max; break; - case OperatorType::Power: return storm::expressions::OperatorType::Power; break; + case OperatorType::Plus: result = storm::expressions::OperatorType::Plus; break; + case OperatorType::Minus: result = storm::expressions::OperatorType::Minus; break; + case OperatorType::Times: result = storm::expressions::OperatorType::Times; break; + case OperatorType::Divide: result = storm::expressions::OperatorType::Divide; break; + case OperatorType::Min: result = storm::expressions::OperatorType::Min; break; + case OperatorType::Max: result = storm::expressions::OperatorType::Max; break; + case OperatorType::Power: result = storm::expressions::OperatorType::Power; break; } + return result; } int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const { @@ -35,15 +37,17 @@ namespace storm { int_fast64_t firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation); int_fast64_t secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation); + int_fast64_t result = 0; switch (this->getOperatorType()) { - case OperatorType::Plus: return firstOperandEvaluation + secondOperandEvaluation; break; - case OperatorType::Minus: return firstOperandEvaluation - secondOperandEvaluation; break; - case OperatorType::Times: return firstOperandEvaluation * secondOperandEvaluation; break; - case OperatorType::Divide: return firstOperandEvaluation / secondOperandEvaluation; break; - case OperatorType::Min: return std::min(firstOperandEvaluation, secondOperandEvaluation); break; - case OperatorType::Max: return std::max(firstOperandEvaluation, secondOperandEvaluation); break; - case OperatorType::Power: return static_cast(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; + case OperatorType::Plus: result = firstOperandEvaluation + secondOperandEvaluation; break; + case OperatorType::Minus: result = firstOperandEvaluation - secondOperandEvaluation; break; + case OperatorType::Times: result = firstOperandEvaluation * secondOperandEvaluation; break; + case OperatorType::Divide: result = firstOperandEvaluation / secondOperandEvaluation; break; + case OperatorType::Min: result = std::min(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Max: result = std::max(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Power: result = static_cast(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; } + return result; } double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const { @@ -51,15 +55,17 @@ namespace storm { double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation); double secondOperandEvaluation = this->getSecondOperand()->evaluateAsDouble(valuation); + double result = 0; switch (this->getOperatorType()) { - case OperatorType::Plus: return firstOperandEvaluation + secondOperandEvaluation; break; - case OperatorType::Minus: return firstOperandEvaluation - secondOperandEvaluation; break; - case OperatorType::Times: return firstOperandEvaluation * secondOperandEvaluation; break; - case OperatorType::Divide: return firstOperandEvaluation / secondOperandEvaluation; break; - case OperatorType::Min: return std::min(firstOperandEvaluation, secondOperandEvaluation); break; - case OperatorType::Max: return std::max(firstOperandEvaluation, secondOperandEvaluation); break; - case OperatorType::Power: return std::pow(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Plus: result = firstOperandEvaluation + secondOperandEvaluation; break; + case OperatorType::Minus: result = firstOperandEvaluation - secondOperandEvaluation; break; + case OperatorType::Times: result = firstOperandEvaluation * secondOperandEvaluation; break; + case OperatorType::Divide: result = firstOperandEvaluation / secondOperandEvaluation; break; + case OperatorType::Min: result = std::min(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Max: result = std::max(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Power: result = std::pow(firstOperandEvaluation, secondOperandEvaluation); break; } + return result; } std::shared_ptr BinaryNumericalFunctionExpression::simplify() const { diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp index f72672296..e6022380e 100644 --- a/src/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storage/expressions/BinaryRelationExpression.cpp @@ -13,14 +13,16 @@ namespace storm { } storm::expressions::OperatorType BinaryRelationExpression::getOperator() const { + storm::expressions::OperatorType result = storm::expressions::OperatorType::Equal; switch (this->getRelationType()) { - case RelationType::Equal: return storm::expressions::OperatorType::Equal; break; - case RelationType::NotEqual: return storm::expressions::OperatorType::NotEqual; break; - case RelationType::Less: return storm::expressions::OperatorType::Less; break; - case RelationType::LessOrEqual: return storm::expressions::OperatorType::LessOrEqual; break; - case RelationType::Greater: return storm::expressions::OperatorType::Greater; break; - case RelationType::GreaterOrEqual: return storm::expressions::OperatorType::GreaterOrEqual; break; + case RelationType::Equal: result = storm::expressions::OperatorType::Equal; break; + case RelationType::NotEqual: result = storm::expressions::OperatorType::NotEqual; break; + case RelationType::Less: result = storm::expressions::OperatorType::Less; break; + case RelationType::LessOrEqual: result = storm::expressions::OperatorType::LessOrEqual; break; + case RelationType::Greater: result = storm::expressions::OperatorType::Greater; break; + case RelationType::GreaterOrEqual: result = storm::expressions::OperatorType::GreaterOrEqual; break; } + return result; } bool BinaryRelationExpression::evaluateAsBool(Valuation const* valuation) const { @@ -28,14 +30,16 @@ namespace storm { double firstOperandEvaluated = this->getFirstOperand()->evaluateAsDouble(valuation); double secondOperandEvaluated = this->getSecondOperand()->evaluateAsDouble(valuation); + bool result = false; switch (this->getRelationType()) { - case RelationType::Equal: return firstOperandEvaluated == secondOperandEvaluated; break; - case RelationType::NotEqual: return firstOperandEvaluated != secondOperandEvaluated; break; - case RelationType::Greater: return firstOperandEvaluated > secondOperandEvaluated; break; - case RelationType::GreaterOrEqual: return firstOperandEvaluated >= secondOperandEvaluated; break; - case RelationType::Less: return firstOperandEvaluated < secondOperandEvaluated; break; - case RelationType::LessOrEqual: return firstOperandEvaluated <= secondOperandEvaluated; break; + case RelationType::Equal: result = firstOperandEvaluated == secondOperandEvaluated; break; + case RelationType::NotEqual: result = firstOperandEvaluated != secondOperandEvaluated; break; + case RelationType::Greater: result = firstOperandEvaluated > secondOperandEvaluated; break; + case RelationType::GreaterOrEqual: result = firstOperandEvaluated >= secondOperandEvaluated; break; + case RelationType::Less: result = firstOperandEvaluated < secondOperandEvaluated; break; + case RelationType::LessOrEqual: result = firstOperandEvaluated <= secondOperandEvaluated; break; } + return result; } std::shared_ptr BinaryRelationExpression::simplify() const { diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp index f3e65a94f..4692675bf 100644 --- a/src/storage/expressions/IfThenElseExpression.cpp +++ b/src/storage/expressions/IfThenElseExpression.cpp @@ -70,7 +70,7 @@ namespace storm { } std::shared_ptr IfThenElseExpression::simplify() const { - std::shared_ptr conditionSimplified; + std::shared_ptr conditionSimplified = this->condition->simplify(); if (conditionSimplified->isTrue()) { return this->thenExpression->simplify(); } else if (conditionSimplified->isFalse()) { diff --git a/src/storage/expressions/LinearityCheckVisitor.cpp b/src/storage/expressions/LinearityCheckVisitor.cpp index 5749d3a35..35e1e5c76 100644 --- a/src/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storage/expressions/LinearityCheckVisitor.cpp @@ -3,6 +3,7 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidTypeException.h" +#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace expressions { @@ -51,6 +52,7 @@ namespace storm { case BinaryNumericalFunctionExpression::OperatorType::Max: return LinearityStatus::NonLinear; break; case BinaryNumericalFunctionExpression::OperatorType::Power: return LinearityStatus::NonLinear; break; } + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal binary numerical expression operator."); } boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const& expression) { @@ -72,6 +74,7 @@ namespace storm { case UnaryNumericalFunctionExpression::OperatorType::Floor: case UnaryNumericalFunctionExpression::OperatorType::Ceil: return LinearityStatus::NonLinear; } + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator."); } boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression) { diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp index e4069ec44..020d2de27 100644 --- a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp @@ -14,18 +14,21 @@ namespace storm { } storm::expressions::OperatorType UnaryBooleanFunctionExpression::getOperator() const { + storm::expressions::OperatorType result = storm::expressions::OperatorType::Not; switch (this->getOperatorType()) { - case OperatorType::Not: return storm::expressions::OperatorType::Not; + case OperatorType::Not: result = storm::expressions::OperatorType::Not; } + return result; } bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const { STORM_LOG_THROW(this->hasBooleanType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); - bool operandEvaluated = this->getOperand()->evaluateAsBool(valuation); + bool result = this->getOperand()->evaluateAsBool(valuation); switch (this->getOperatorType()) { - case OperatorType::Not: return !operandEvaluated; break; + case OperatorType::Not: result = !result; break; } + return result; } std::shared_ptr UnaryBooleanFunctionExpression::simplify() const { diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp index edfb22702..e0181e139 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -19,33 +19,37 @@ namespace storm { } storm::expressions::OperatorType UnaryNumericalFunctionExpression::getOperator() const { + storm::expressions::OperatorType result = storm::expressions::OperatorType::Minus; switch (this->getOperatorType()) { - case OperatorType::Minus: return storm::expressions::OperatorType::Minus; break; - case OperatorType::Floor: return storm::expressions::OperatorType::Floor; break; - case OperatorType::Ceil: return storm::expressions::OperatorType::Ceil; break; + case OperatorType::Minus: result = storm::expressions::OperatorType::Minus; break; + case OperatorType::Floor: result = storm::expressions::OperatorType::Floor; break; + case OperatorType::Ceil: result = storm::expressions::OperatorType::Ceil; break; } + return result; } int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const { STORM_LOG_THROW(this->hasIntegerType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); - int_fast64_t operandEvaluated = this->getOperand()->evaluateAsInt(valuation); + int_fast64_t result = this->getOperand()->evaluateAsInt(valuation); switch (this->getOperatorType()) { - case OperatorType::Minus: return -operandEvaluated; break; - case OperatorType::Floor: return std::floor(operandEvaluated); break; - case OperatorType::Ceil: return std::ceil(operandEvaluated); break; + case OperatorType::Minus: result = -result; break; + case OperatorType::Floor: result = std::floor(result); break; + case OperatorType::Ceil: result = std::ceil(result); break; } + return result; } double UnaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const { STORM_LOG_THROW(this->hasNumericalType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); - double operandEvaluated = this->getOperand()->evaluateAsDouble(valuation); + double result = this->getOperand()->evaluateAsDouble(valuation); switch (this->getOperatorType()) { - case OperatorType::Minus: return -operandEvaluated; break; - case OperatorType::Floor: return std::floor(operandEvaluated); break; - case OperatorType::Ceil: return std::ceil(operandEvaluated); break; + case OperatorType::Minus: result = -result; break; + case OperatorType::Floor: result = std::floor(result); break; + case OperatorType::Ceil: result = std::ceil(result); break; } + return result; } std::shared_ptr UnaryNumericalFunctionExpression::simplify() const { diff --git a/src/utility/cli.h b/src/utility/cli.h index 3e1b820e4..b2f07046e 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -269,8 +269,7 @@ namespace storm { template<> inline void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { - storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - + STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); std::shared_ptr> dtmc = model->template as>(); @@ -302,7 +301,6 @@ namespace storm { template void verifySymbolicModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { - storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 785f1d00c..1cc0ea445 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -33,6 +33,7 @@ namespace storm { switch (equationSolver) { case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeLinearEquationSolver(matrix)); + default: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); } } @@ -71,6 +72,7 @@ namespace storm { switch (equationSolver) { case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); + default: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); } } @@ -94,6 +96,7 @@ namespace storm { switch (lpSolver) { case storm::settings::modules::GeneralSettings::LpSolver::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); case storm::settings::modules::GeneralSettings::LpSolver::glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); + default: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); } } diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index db6adc88f..c93ac830a 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -11,28 +11,28 @@ TEST(DdPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(13, model->getNumberOfStates()); - EXPECT_EQ(20, model->getNumberOfTransitions()); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(677, model->getNumberOfStates()); - EXPECT_EQ(867, model->getNumberOfTransitions()); + EXPECT_EQ(677ul, model->getNumberOfStates()); + EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(8607, model->getNumberOfStates()); - EXPECT_EQ(15113, model->getNumberOfTransitions()); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(273, model->getNumberOfStates()); - EXPECT_EQ(397, model->getNumberOfTransitions()); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(1728, model->getNumberOfStates()); - EXPECT_EQ(2505, model->getNumberOfTransitions()); + EXPECT_EQ(1728ul, model->getNumberOfStates()); + EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest, Ctmc) { @@ -42,28 +42,28 @@ TEST(DdPrismModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(276, model->getNumberOfStates()); - EXPECT_EQ(1120, model->getNumberOfTransitions()); + EXPECT_EQ(276ul, model->getNumberOfStates()); + EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(3478, model->getNumberOfStates()); - EXPECT_EQ(14639, model->getNumberOfTransitions()); + EXPECT_EQ(3478ul, model->getNumberOfStates()); + EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(12, model->getNumberOfStates()); - EXPECT_EQ(22, model->getNumberOfTransitions()); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(810, model->getNumberOfStates()); - EXPECT_EQ(3699, model->getNumberOfTransitions()); + EXPECT_EQ(810ul, model->getNumberOfStates()); + EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(66, model->getNumberOfStates()); - EXPECT_EQ(189, model->getNumberOfTransitions()); + EXPECT_EQ(66ul, model->getNumberOfStates()); + EXPECT_EQ(189ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest, Mdp) { @@ -73,9 +73,9 @@ TEST(DdPrismModelBuilderTest, Mdp) { EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); - EXPECT_EQ(169, mdp->getNumberOfStates()); - EXPECT_EQ(436, mdp->getNumberOfTransitions()); - EXPECT_EQ(254, mdp->getNumberOfChoices()); + EXPECT_EQ(169ul, mdp->getNumberOfStates()); + EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(254ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); @@ -83,9 +83,9 @@ TEST(DdPrismModelBuilderTest, Mdp) { EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); - EXPECT_EQ(364, mdp->getNumberOfStates()); - EXPECT_EQ(654, mdp->getNumberOfTransitions()); - EXPECT_EQ(573, mdp->getNumberOfChoices()); + EXPECT_EQ(364ul, mdp->getNumberOfStates()); + EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(573ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); @@ -93,9 +93,9 @@ TEST(DdPrismModelBuilderTest, Mdp) { EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); - EXPECT_EQ(272, mdp->getNumberOfStates()); - EXPECT_EQ(492, mdp->getNumberOfTransitions()); - EXPECT_EQ(400, mdp->getNumberOfChoices()); + EXPECT_EQ(272ul, mdp->getNumberOfStates()); + EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(400ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); @@ -103,9 +103,9 @@ TEST(DdPrismModelBuilderTest, Mdp) { EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); - EXPECT_EQ(1038, mdp->getNumberOfStates()); - EXPECT_EQ(1282, mdp->getNumberOfTransitions()); - EXPECT_EQ(1054, mdp->getNumberOfChoices()); + EXPECT_EQ(1038ul, mdp->getNumberOfStates()); + EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); @@ -113,9 +113,9 @@ TEST(DdPrismModelBuilderTest, Mdp) { EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); - EXPECT_EQ(4093, mdp->getNumberOfStates()); - EXPECT_EQ(5585, mdp->getNumberOfTransitions()); - EXPECT_EQ(5519, mdp->getNumberOfChoices()); + EXPECT_EQ(4093ul, mdp->getNumberOfStates()); + EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); @@ -123,7 +123,7 @@ TEST(DdPrismModelBuilderTest, Mdp) { EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); - EXPECT_EQ(37, mdp->getNumberOfStates()); - EXPECT_EQ(59, mdp->getNumberOfTransitions()); - EXPECT_EQ(59, mdp->getNumberOfChoices()); + EXPECT_EQ(37ul, mdp->getNumberOfStates()); + EXPECT_EQ(59ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(59ul, mdp->getNumberOfChoices()); } \ No newline at end of file diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index bf4ee90d8..8b8fde965 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -8,28 +8,28 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(13, model->getNumberOfStates()); - EXPECT_EQ(20, model->getNumberOfTransitions()); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(677, model->getNumberOfStates()); - EXPECT_EQ(867, model->getNumberOfTransitions()); + EXPECT_EQ(677ul, model->getNumberOfStates()); + EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(8607, model->getNumberOfStates()); - EXPECT_EQ(15113, model->getNumberOfTransitions()); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(273, model->getNumberOfStates()); - EXPECT_EQ(397, model->getNumberOfTransitions()); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(1728, model->getNumberOfStates()); - EXPECT_EQ(2505, model->getNumberOfTransitions()); + EXPECT_EQ(1728ul, model->getNumberOfStates()); + EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } TEST(ExplicitPrismModelBuilderTest, Ctmc) { @@ -39,59 +39,59 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(276, model->getNumberOfStates()); - EXPECT_EQ(1120, model->getNumberOfTransitions()); + EXPECT_EQ(276ul, model->getNumberOfStates()); + EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(3478, model->getNumberOfStates()); - EXPECT_EQ(14639, model->getNumberOfTransitions()); + EXPECT_EQ(3478ul, model->getNumberOfStates()); + EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(12, model->getNumberOfStates()); - EXPECT_EQ(22, model->getNumberOfTransitions()); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(810, model->getNumberOfStates()); - EXPECT_EQ(3699, model->getNumberOfTransitions()); + EXPECT_EQ(810ul, model->getNumberOfStates()); + EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(66, model->getNumberOfStates()); - EXPECT_EQ(189, model->getNumberOfTransitions()); + EXPECT_EQ(66ul, model->getNumberOfStates()); + EXPECT_EQ(189ul, model->getNumberOfTransitions()); } TEST(ExplicitPrismModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(169, model->getNumberOfStates()); - EXPECT_EQ(436, model->getNumberOfTransitions()); + EXPECT_EQ(169ul, model->getNumberOfStates()); + EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(364, model->getNumberOfStates()); - EXPECT_EQ(654, model->getNumberOfTransitions()); + EXPECT_EQ(364ul, model->getNumberOfStates()); + EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(272, model->getNumberOfStates()); - EXPECT_EQ(492, model->getNumberOfTransitions()); + EXPECT_EQ(272ul, model->getNumberOfStates()); + EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(1038, model->getNumberOfStates()); - EXPECT_EQ(1282, model->getNumberOfTransitions()); + EXPECT_EQ(1038ul, model->getNumberOfStates()); + EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(4093, model->getNumberOfStates()); - EXPECT_EQ(5585, model->getNumberOfTransitions()); + EXPECT_EQ(4093ul, model->getNumberOfStates()); + EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); - EXPECT_EQ(37, model->getNumberOfStates()); - EXPECT_EQ(59, model->getNumberOfTransitions()); + EXPECT_EQ(37ul, model->getNumberOfStates()); + EXPECT_EQ(59ul, model->getNumberOfTransitions()); } \ No newline at end of file diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index df17ce336..e2dfdcfd4 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -24,8 +24,8 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { options.buildRewards = true; options.rewardModelName = "coin_flips"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(13, model->getNumberOfStates()); - EXPECT_EQ(20, model->getNumberOfTransitions()); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -78,8 +78,8 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(8607, model->getNumberOfStates()); - EXPECT_EQ(15113, model->getNumberOfTransitions()); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -130,8 +130,8 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { options.buildRewards = true; options.rewardModelName = "num_rounds"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(273, model->getNumberOfStates()); - EXPECT_EQ(397, model->getNumberOfTransitions()); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 44de993a1..571492a5b 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -24,8 +24,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { options.buildRewards = true; options.rewardModelName = "coinflips"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(169, model->getNumberOfStates()); - EXPECT_EQ(436, model->getNumberOfTransitions()); + EXPECT_EQ(169ul, model->getNumberOfStates()); + EXPECT_EQ(436ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); @@ -126,8 +126,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { options.buildRewards = true; options.rewardModelName = "rounds"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(3172, model->getNumberOfStates()); - EXPECT_EQ(7144, model->getNumberOfTransitions()); + EXPECT_EQ(3172ul, model->getNumberOfStates()); + EXPECT_EQ(7144ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 60f283cd2..26869f425 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -24,8 +24,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { options.buildRewards = true; options.rewardModelName = "coin_flips"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(13, model->getNumberOfStates()); - EXPECT_EQ(20, model->getNumberOfTransitions()); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -78,8 +78,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(8607, model->getNumberOfStates()); - EXPECT_EQ(15113, model->getNumberOfTransitions()); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -130,8 +130,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { options.buildRewards = true; options.rewardModelName = "num_rounds"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(273, model->getNumberOfStates()); - EXPECT_EQ(397, model->getNumberOfTransitions()); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 02d6ad5ba..916633101 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -23,8 +23,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { options.buildRewards = true; options.rewardModelName = "coin_flips"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(13, model->getNumberOfStates()); - EXPECT_EQ(20, model->getNumberOfTransitions()); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -77,8 +77,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(8607, model->getNumberOfStates()); - EXPECT_EQ(15113, model->getNumberOfTransitions()); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); @@ -129,8 +129,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { options.buildRewards = true; options.rewardModelName = "num_rounds"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(273, model->getNumberOfStates()); - EXPECT_EQ(397, model->getNumberOfTransitions()); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);