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<int_fast64_t>(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<uint_fast64_t> usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation);
usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end());
- // Display achieved probability.
- std::pair<uint_fast64_t, double> 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<uint_fast64_t>(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<uint_fast64_t>(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<std::string> 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<ValueType>::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<Type>::SymbolicGameSolver(storm::dd::Add<Type> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> 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<DdType, ValueType>::SymbolicLinearEquationSolver(storm::dd::Add<DdType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> 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 <utility>
-#include <chrono>
#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<std::chrono::milliseconds>(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<ValueType> sccDecomposition(this->A, fullSystem, false, false);
@@ -151,11 +143,6 @@ namespace storm {
std::vector<std::pair<bool, storm::storage::StateBlock>> 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<std::chrono::milliseconds>(sccEndTime - sccStartTime).count() << "ms." << std::endl;
-
- std::chrono::high_resolution_clock::time_point calcStartTime = std::chrono::high_resolution_clock::now();
-
std::vector<ValueType>* currentX = nullptr;
std::vector<ValueType>* 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<std::chrono::milliseconds>(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<int_fast64_t>(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<int_fast64_t>(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<BaseExpression const> 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<BaseExpression const> BinaryRelationExpression::simplify() const {
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<BaseExpression const> 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<BaseExpression const> UnaryNumericalFunctionExpression::simplify() const {
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 8a28cb0e4..63de731b3 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -269,8 +269,7 @@ namespace storm {
template<>
inline void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> 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<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
@@ -302,7 +301,6 @@ namespace storm {
template<storm::dd::DdType DdType>
void verifySymbolicModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> formula) {
- storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> 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<storm::solver::LinearEquationSolver<ValueType>>(new storm::solver::GmmxxLinearEquationSolver<ValueType>(matrix));
case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>(new storm::solver::NativeLinearEquationSolver<ValueType>(matrix));
+ default: return std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>(new storm::solver::GmmxxLinearEquationSolver<ValueType>(matrix));
}
}
@@ -71,6 +72,7 @@ namespace storm {
switch (equationSolver) {
case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix));
case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix));
+ default: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix));
}
}
@@ -94,6 +96,7 @@ namespace storm {
switch (lpSolver) {
case storm::settings::modules::GeneralSettings::LpSolver::Gurobi: return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
case storm::settings::modules::GeneralSettings::LpSolver::glpk: return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GlpkLpSolver(name));
+ default: return std::unique_ptr<storm::solver::LpSolver>(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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
- 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<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -83,9 +83,9 @@ TEST(DdPrismModelBuilderTest, Mdp) {
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
- 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<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -93,9 +93,9 @@ TEST(DdPrismModelBuilderTest, Mdp) {
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
- 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<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -103,9 +103,9 @@ TEST(DdPrismModelBuilderTest, Mdp) {
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
- 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<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -113,9 +113,9 @@ TEST(DdPrismModelBuilderTest, Mdp) {
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
- 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<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -123,7 +123,7 @@ TEST(DdPrismModelBuilderTest, Mdp) {
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
- 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::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<double>::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<double>::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<double>::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<double>::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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::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<double>::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<double>::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<double>::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<double>::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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::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<double>::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<double>::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<double>::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<double>::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<double>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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);