sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'master' of https://sselab.de/lab9/private/git/storm 

Former-commit-id: ffe35039a5
main
sjunges 10 years ago
parent
1bb4d2c0ae 5365d50811
commit
eb19d7f709
26 changed files with 172 additions and 171 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      CMakeLists.txt
  2. 2
      src/builder/ExplicitPrismModelBuilder.cpp
  3. 3
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  4. 2
      src/settings/ArgumentBase.cpp
  5. 1
      src/settings/ArgumentBuilder.h
  6. 2
      src/settings/Option.cpp
  7. 3
      src/settings/SettingsManager.cpp
  8. 2
      src/solver/NativeLinearEquationSolver.cpp
  9. 1
      src/solver/SymbolicGameSolver.cpp
  10. 1
      src/solver/SymbolicLinearEquationSolver.cpp
  11. 16
      src/solver/TopologicalMinMaxLinearEquationSolver.cpp
  12. 2
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  13. 1
      src/storage/Distribution.cpp
  14. 48
      src/storage/expressions/BinaryNumericalFunctionExpression.cpp
  15. 28
      src/storage/expressions/BinaryRelationExpression.cpp
  16. 3
      src/storage/expressions/LinearityCheckVisitor.cpp
  17. 9
      src/storage/expressions/UnaryBooleanFunctionExpression.cpp
  18. 26
      src/storage/expressions/UnaryNumericalFunctionExpression.cpp
  19. 2
      src/utility/cli.h
  20. 3
      src/utility/solver.cpp
  21. 76
      test/functional/builder/DdPrismModelBuilderTest.cpp
  22. 64
      test/functional/builder/ExplicitPrismModelBuilderTest.cpp
  23. 12
      test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  24. 8
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  25. 12
      test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
  26. 12
      test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp

2
CMakeLists.txt
View File

@ -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)

2
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -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.

3
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -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;
}

2
src/settings/ArgumentBase.cpp
View File

@ -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();

1
src/settings/ArgumentBuilder.h
View File

@ -176,6 +176,7 @@ return *this; \
}
break;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException, "Argument has illegal type.");
}
private:

2
src/settings/Option.cpp
View File

@ -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) << "--";

3
src/settings/SettingsManager.cpp
View File

@ -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.

2
src/solver/NativeLinearEquationSolver.cpp
View File

@ -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";
}
}

1
src/solver/SymbolicGameSolver.cpp
View File

@ -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();

1
src/solver/SymbolicLinearEquationSolver.cpp
View File

@ -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();

16
src/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -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;
}
}

2
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -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

1
src/storage/Distribution.cpp
View File

@ -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) {

48
src/storage/expressions/BinaryNumericalFunctionExpression.cpp
View File

@ -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 {

28
src/storage/expressions/BinaryRelationExpression.cpp
View File

@ -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 {

3
src/storage/expressions/LinearityCheckVisitor.cpp
View File

@ -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) {

9
src/storage/expressions/UnaryBooleanFunctionExpression.cpp
View File

@ -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 {

26
src/storage/expressions/UnaryNumericalFunctionExpression.cpp
View File

@ -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 {

2
src/utility/cli.h
View File

@ -269,7 +269,6 @@ 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;

3
src/utility/solver.cpp
View File

@ -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));
}
}

76
test/functional/builder/DdPrismModelBuilderTest.cpp
View File

@ -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());
}

64
test/functional/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -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());
}

12
test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -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);

8
test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

@ -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);

12
test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -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);

12
test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
View File

@ -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);

Write Preview
Loading…
Cancel
Save