From 19029cd905180ff4ff86dc3020277ead8db11885 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 19 Nov 2015 18:00:51 +0100 Subject: [PATCH] functional tests compile and run again, yay! Former-commit-id: 60d3ce16b9d999f6a73fb88fb0ea6e41934eb56c --- src/adapters/AddExpressionAdapter.cpp | 6 +- src/storage/dd/Add.cpp | 29 ++-- src/storage/dd/Add.h | 33 ++-- src/storage/dd/Bdd.cpp | 18 ++- src/storage/dd/Bdd.h | 13 +- src/storage/dd/Dd.cpp | 5 + src/storage/dd/DdManager.cpp | 22 ++- src/storage/dd/DdManager.h | 8 +- src/storage/dd/DdMetaVariable.cpp | 3 + src/storage/dd/cudd/CuddAddIterator.cpp | 17 +- src/storage/dd/cudd/CuddAddIterator.h | 6 +- src/storage/dd/cudd/CuddOdd.cpp | 12 +- src/storage/dd/cudd/CuddOdd.h | 3 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 30 ++-- src/storage/dd/cudd/InternalCuddAdd.h | 4 +- src/storage/dd/cudd/InternalCuddBdd.cpp | 5 + src/storage/dd/cudd/InternalCuddBdd.h | 1 + src/storage/dd/cudd/InternalCuddDdManager.cpp | 17 ++ src/storage/dd/cudd/InternalCuddDdManager.h | 8 +- src/utility/graph.cpp | 95 +++++------ src/utility/graph.h | 2 +- src/utility/solver.cpp | 12 +- src/utility/solver.h | 26 ++- src/utility/storm.h | 4 +- .../builder/DdPrismModelBuilderTest.cpp | 3 - .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 46 +++--- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 20 +-- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 28 ++-- .../NativeHybridCtmcCslModelCheckerTest.cpp | 38 ++--- .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 20 +-- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 28 ++-- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 20 +-- .../SymbolicMdpPrctlModelCheckerTest.cpp | 28 ++-- .../solver/FullySymbolicGameSolverTest.cpp | 39 +++-- test/functional/storage/CuddDdTest.cpp | 151 +++++++++--------- test/functional/utility/GraphTest.cpp | 7 +- 36 files changed, 433 insertions(+), 374 deletions(-) diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index ee79488ac..baf1121e8 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -164,17 +164,17 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { - return ddManager->getConstant(expression.getValue()); + return ddManager->getConstant(static_cast(expression.getValue())); } template boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { - return ddManager->getConstant(expression.getValue()); + return ddManager->getConstant(static_cast(expression.getValue())); } template boost::any AddExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { - return ddManager->getConstant(expression.getValue()); + return ddManager->getConstant(static_cast(expression.getValue())); } // Explicitly instantiate the symbolic expression adapter diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 3d8225a25..22f0f9a29 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -223,7 +223,8 @@ namespace storm { to.push_back(ddVariable.template toAdd()); } } - return Add(this->getDdManager(), internalAdd.swapVariables(from, to), newContainedMetaVariables); + STORM_LOG_THROW(from.size() == to.size(), storm::exceptions::InvalidArgumentException, "Unable to swap mismatching meta variables."); + return Add(this->getDdManager(), internalAdd.swapVariables(from, to), newContainedMetaVariables); } template @@ -385,16 +386,11 @@ namespace storm { template std::vector Add::toVector(Odd const& rowOdd) const { std::vector result(rowOdd.getTotalOffset()); - std::vector ddVariableIndices = this->getDdManager()->getSortedVariableIndices(); - addToExplicitVector(rowOdd, ddVariableIndices, result); + std::vector ddVariableIndices = this->getSortedVariableIndices(); + internalAdd.composeWithExplicitVector(rowOdd, ddVariableIndices, result, std::plus()); return result; } - template - void Add::addToExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { - internalAdd.composeWithExplicitVector(odd, ddVariableIndices, targetVector, std::plus()); - } - template std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector const& groupOffsets) const { std::set rowMetaVariables; @@ -491,7 +487,7 @@ namespace storm { // Prepare the vectors that represent the matrix. std::vector rowIndications(rowOdd.getTotalOffset() + 1); - std::vector> columnsAndValues(this->getNonZeroCount()); + std::vector> columnsAndValues(this->getNonZeroCount()); // Create a trivial row grouping. std::vector trivialRowGroupIndices(rowIndications.size()); @@ -528,7 +524,7 @@ namespace storm { rowIndications[0] = 0; // Construct matrix and return result. - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); } template @@ -604,7 +600,7 @@ namespace storm { std::vector> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices); // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); + std::vector> columnsAndValues(this->getNonZeroCount()); // Now compute the indices at which the individual rows start. std::vector rowIndications(rowGroupIndices.back() + 1); @@ -652,7 +648,7 @@ namespace storm { } rowIndications[0] = 0; - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); } template @@ -722,13 +718,13 @@ namespace storm { rowGroupIndices[0] = 0; // Create the explicit vector we need to fill later. - std::vector explicitVector(rowGroupIndices.back()); + std::vector explicitVector(rowGroupIndices.back()); // Next, we split the matrix into one for each group. Note that this only works if the group variables are at the very top. std::vector, InternalAdd>> groups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices); // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); + std::vector> columnsAndValues(this->getNonZeroCount()); // Now compute the indices at which the individual rows start. std::vector rowIndications(rowGroupIndices.back() + 1); @@ -739,7 +735,7 @@ namespace storm { std::pair, InternalAdd> const& ddPair = groups[i]; ddPair.first.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false); - ddPair.second.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus()); + ddPair.second.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus()); statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).template toAdd(); stateToRowGroupCount += statesWithGroupEnabled[i]; @@ -777,7 +773,7 @@ namespace storm { } rowIndications[0] = 0; - return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); } template @@ -822,5 +818,6 @@ namespace storm { } template class Add; + template class Add; } } \ No newline at end of file diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index da5cf9b5d..295132840 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -37,6 +37,17 @@ namespace storm { Add(Add&& other) = default; Add& operator=(Add&& other) = default; + /*! + * Builds an ADD representing the given vector. + * + * @param ddManager The manager responsible for the ADD. + * @param values The vector that is to be represented by the ADD. + * @param odd The ODD used for the translation. + * @param metaVariables The meta variables used for the translation. + * @return The resulting (CUDD) ADD. + */ + static Add fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); + /*! * Retrieves whether the two DDs represent the same function. * @@ -668,27 +679,7 @@ namespace storm { * (if it was given). */ std::pair, std::vector> toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Adds the current (DD-based) vector to the given explicit one. - * - * @param odd The ODD used for the translation. - * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. - * @param targetVector The vector to which the translated DD-based vector is to be added. - */ - void addToExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - - /*! - * Builds an ADD representing the given vector. - * - * @param ddManager The manager responsible for the ADD. - * @param values The vector that is to be represented by the ADD. - * @param odd The ODD used for the translation. - * @param metaVariables The meta variables used for the translation. - * @return The resulting (CUDD) ADD. - */ - static Add fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); - + // The internal ADD that depends on the chosen library. InternalAdd internalAdd; }; diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 08c47a82f..e199ad58a 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -16,7 +16,7 @@ namespace storm { namespace dd { template - Bdd::Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalBdd(internalBdd) { + Bdd::Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalBdd(internalBdd) { // Intentionally left empty. } @@ -36,7 +36,7 @@ namespace storm { template template - Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { + Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { return Bdd(ddManager, InternalBdd::fromVector(&ddManager->internalDdManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables); } @@ -121,7 +121,7 @@ namespace storm { template Bdd Bdd::andExists(Bdd const& other, std::set const& existentialVariables) const { - Bdd cube = getCube(*this->getDdManager(), existentialVariables); + Bdd cube = getCube(*this->getDdManager(), existentialVariables); std::set unionOfMetaVariables; std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); @@ -171,12 +171,12 @@ namespace storm { template template Add Bdd::toAdd() const { - return Add(internalBdd.template toAdd()); + return Add(this->getDdManager(), internalBdd.template toAdd(), this->getContainedMetaVariables()); } template storm::storage::BitVector Bdd::toVector(storm::dd::Odd const& rowOdd) const { - return internalBdd.toVector(rowOdd, this->getDdManager()->getSortedVariableIndices()); + return internalBdd.toVector(rowOdd, this->getSortedVariableIndices()); } template @@ -237,6 +237,12 @@ namespace storm { return internalBdd; } - template class Bdd; + template class Bdd; + + template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + + template Add Bdd::toAdd() const; + template Add Bdd::toAdd() const; } } \ No newline at end of file diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index 5f672453d..ecb1028e9 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -11,11 +11,18 @@ namespace storm { template class Add; + template + class Odd; + template class Bdd : public Dd { public: friend class DdManager; - friend class Add; + + template + friend class Add; + + friend class Odd; // Instantiate all copy/move constructors/assignments with the default implementation. Bdd() = default; @@ -250,7 +257,7 @@ namespace storm { * @param cuddBdd The CUDD BDD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables = std::set()); + Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables = std::set()); /*! * Builds a BDD representing the values that make the given filter function evaluate to true. @@ -263,7 +270,7 @@ namespace storm { * @return The resulting (CUDD) BDD. */ template - static Bdd fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + static Bdd fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); // The internal BDD that depends on the chosen library. InternalBdd internalBdd; diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp index 4f190a134..2a806156c 100644 --- a/src/storage/dd/Dd.cpp +++ b/src/storage/dd/Dd.cpp @@ -4,6 +4,9 @@ #include "src/storage/dd/DdManager.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + namespace storm { namespace dd { template @@ -74,6 +77,8 @@ namespace storm { template std::set Dd::subtractMetaVariables(storm::dd::Dd const& first, storm::dd::Dd const& second) { + bool includesAllMetaVariables = std::includes(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end()); + STORM_LOG_THROW(includesAllMetaVariables, storm::exceptions::InvalidArgumentException, "Cannot subtract meta variables that are not contained in the DD."); std::set metaVariables; std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); return metaVariables; diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 95226f8aa..687496629 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -37,7 +37,7 @@ namespace storm { template template Add DdManager::getConstant(ValueType const& value) const { - return Add(this->shared_from_this(), internalDdManager.constant(value)); + return Add(this->shared_from_this(), internalDdManager.getConstant(value)); } template @@ -89,7 +89,7 @@ namespace storm { Add result = this->getAddZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result += this->getEncoding(variable, value).toAdd() * this->getConstant(value); + result += this->getEncoding(variable, value).template toAdd() * this->getConstant(static_cast(value)); } return result; } @@ -115,7 +115,7 @@ namespace storm { for (std::size_t i = 0; i < numberOfBits; ++i) { auto ddVariablePair = internalDdManager.createNewDdVariablePair(); variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); - variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {unprimed})); + variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); } metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables)); @@ -281,8 +281,8 @@ namespace storm { template std::vector DdManager::getSortedVariableIndices(std::set const& metaVariables) const { std::vector ddVariableIndices; - for (auto const& metaVariable : metaVariableMap) { - for (auto const& ddVariable : metaVariable.second.getDdVariables()) { + for (auto const& metaVariable : metaVariables) { + for (auto const& ddVariable : metaVariableMap.at(metaVariable).getDdVariables()) { ddVariableIndices.push_back(ddVariable.getIndex()); } } @@ -313,5 +313,17 @@ namespace storm { } template class DdManager; + + template Add DdManager::getAddZero() const; + template Add DdManager::getAddZero() const; + + template Add DdManager::getAddOne() const; + template Add DdManager::getAddOne() const; + + template Add DdManager::getConstant(double const& value) const; + template Add DdManager::getConstant(uint_fast64_t const& value) const; + + template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; + template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; } } \ No newline at end of file diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index d4f23fdfd..c6b238905 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -24,10 +24,14 @@ namespace storm { class DdManager : public std::enable_shared_from_this> { public: friend class Bdd; - friend class Add; - friend class AddIterator; friend class Odd; + template + friend class Add; + + template + friend class AddIterator; + /*! * Creates an empty manager without any meta variables. */ diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index 00ef6452a..bffdb480d 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -1,5 +1,7 @@ #include "src/storage/dd/DdMetaVariable.h" +#include "src/utility/macros.h" + namespace storm { namespace dd { template @@ -49,6 +51,7 @@ namespace storm { template void DdMetaVariable::createCube() { + STORM_LOG_ASSERT(!this->ddVariables.empty(), "The DD variables must not be empty."); auto it = this->ddVariables.begin(); this->cube = *it; ++it; diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp index 070a3982d..5b3761cd8 100644 --- a/src/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storage/dd/cudd/CuddAddIterator.cpp @@ -7,12 +7,12 @@ namespace storm { namespace dd { template - AddIterator::AddIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + AddIterator::AddIterator() : ddManager(), generator(), cube(), valueAsDouble(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { // Intentionally left empty. } template - AddIterator::AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { + AddIterator::AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), valueAsDouble(static_cast(value)), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { // If the given generator is not yet at its end, we need to create the current valuation from the cube from // scratch. if (!this->isAtEnd) { @@ -22,7 +22,7 @@ namespace storm { } template - AddIterator::AddIterator(AddIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { + AddIterator::AddIterator(AddIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), valueAsDouble(other.valueAsDouble), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { // Null-out the pointers of which we took possession. other.cube = nullptr; other.generator = nullptr; @@ -34,7 +34,7 @@ namespace storm { this->ddManager = other.ddManager; this->generator = other.generator; this->cube = other.cube; - this->value = other.value; + this->valueAsDouble = other.valueAsDouble; this->isAtEnd = other.isAtEnd; this->metaVariables = other.metaVariables; this->cubeCounter = other.cubeCounter; @@ -67,7 +67,7 @@ namespace storm { // found solutions and get the next "first" cube. if (this->relevantDontCareDdVariables.empty() || this->cubeCounter >= std::pow(2, this->relevantDontCareDdVariables.size()) - 1) { // Get the next cube and check for emptiness. - ABDD::NextCube(generator, &cube, &value); + ABDD::NextCube(generator, &cube, &valueAsDouble); this->isAtEnd = (Cudd_IsGenEmpty(generator) != 0); // In case we are not done yet, we get ready to treat the next cube. @@ -164,7 +164,7 @@ namespace storm { return true; } else { return this->ddManager.get() == other.ddManager.get() && this->generator == other.generator - && this->cube == other.cube && this->value == other.value && this->isAtEnd == other.isAtEnd + && this->cube == other.cube && this->valueAsDouble == other.valueAsDouble && this->isAtEnd == other.isAtEnd && this->metaVariables == other.metaVariables && this->cubeCounter == other.cubeCounter && this->relevantDontCareDdVariables == other.relevantDontCareDdVariables && this->currentValuation == other.currentValuation; @@ -177,10 +177,11 @@ namespace storm { } template - std::pair AddIterator::operator*() const { - return std::make_pair(currentValuation, value); + std::pair AddIterator::operator*() const { + return std::make_pair(currentValuation, static_cast(valueAsDouble)); } template class AddIterator; + template class AddIterator; } } \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddAddIterator.h b/src/storage/dd/cudd/CuddAddIterator.h index 577c1695f..12b506b8f 100644 --- a/src/storage/dd/cudd/CuddAddIterator.h +++ b/src/storage/dd/cudd/CuddAddIterator.h @@ -54,7 +54,7 @@ namespace storm { * * @return A pair of a valuation and the function value. */ - std::pair operator*() const; + std::pair operator*() const; /*! * Compares the iterator with the given one. Two iterators are considered equal when all their underlying @@ -88,7 +88,7 @@ namespace storm { * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even * if a meta variable does not at all influence the the function value. */ - AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); + AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); /*! * Recreates the internal information when a new cube needs to be treated. @@ -110,7 +110,7 @@ namespace storm { int* cube; // The function value of the current cube. - double value; + double valueAsDouble; // A flag that indicates whether the iterator is at its end and may not be moved further. This is also used // for the check against the end iterator. diff --git a/src/storage/dd/cudd/CuddOdd.cpp b/src/storage/dd/cudd/CuddOdd.cpp index 0e238e1ff..96e4a339f 100644 --- a/src/storage/dd/cudd/CuddOdd.cpp +++ b/src/storage/dd/cudd/CuddOdd.cpp @@ -13,7 +13,8 @@ namespace storm { namespace dd { - Odd::Odd(Add const& add) { + template + Odd::Odd(Add const& add) { std::shared_ptr const> manager = add.getDdManager(); // First, we need to determine the involved DD variables indices. @@ -37,12 +38,12 @@ namespace storm { // First, we need to determine the involved DD variables indices. std::vector ddVariableIndices = bdd.getSortedVariableIndices(); - + // Prepare a unique table for each level that keeps the constructed ODD nodes unique. std::vector, std::shared_ptr>, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1); // Now construct the ODD structure from the BDD. - std::shared_ptr> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->internalDdManager.getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.internalBdd.getCuddDdNode()), manager->internalDdManager.getCuddManager(), 0, Cudd_IsComplement(bdd.internalBdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Finally, move the children of the root ODD into this ODD. this->elseNode = std::move(rootOdd->elseNode); @@ -116,7 +117,7 @@ namespace storm { std::vector ddVariableIndices = selectedValues.getSortedVariableIndices(); uint_fast64_t currentIndex = 0; - addSelectedValuesToVectorRec(selectedValues.getCuddDdNode(), selectedValues.getDdManager()->getCuddManager(), 0, Cudd_IsComplement(selectedValues.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, *this, result, currentIndex, values); + addSelectedValuesToVectorRec(selectedValues.internalBdd.getCuddDdNode(), selectedValues.getDdManager()->internalDdManager.getCuddManager(), 0, Cudd_IsComplement(selectedValues.internalBdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, *this, result, currentIndex, values); return result; } @@ -324,5 +325,8 @@ namespace storm { } } } + + template Odd::Odd(Add const& add); + template Odd::Odd(Add const& add); } } \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddOdd.h b/src/storage/dd/cudd/CuddOdd.h index 3a9e65883..79be50332 100644 --- a/src/storage/dd/cudd/CuddOdd.h +++ b/src/storage/dd/cudd/CuddOdd.h @@ -21,7 +21,8 @@ namespace storm { * * @param add The ADD for which to build the offset-labeled ADD. */ - Odd(Add const& add); + template + Odd(Add const& add); /*! * Constructs an offset-labeled DD from the given BDD. diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 611e23714..fd7fb87bc 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -8,9 +8,15 @@ #include "src/storage/SparseMatrix.h" #include "src/utility/constants.h" +#include "src/utility/macros.h" namespace storm { namespace dd { + template + InternalAdd::InternalAdd(InternalDdManager const* ddManager, ADD cuddAdd) : ddManager(ddManager), cuddAdd(cuddAdd) { + // Intentionally left empty. + } + template bool InternalAdd::operator==(InternalAdd const& other) const { return this->getCuddAdd() == other.getCuddAdd(); @@ -179,6 +185,7 @@ namespace storm { InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { std::vector fromAdd; std::vector toAdd; + STORM_LOG_ASSERT(fromAdd.size() == toAdd.size(), "Sizes of vectors do not match."); for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromAdd.push_back(it1->getCuddAdd()); toAdd.push_back(it2->getCuddAdd()); @@ -403,7 +410,7 @@ namespace storm { template std::vector, InternalAdd>> InternalAdd::splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const { std::vector, InternalAdd>> result; - splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + splitIntoGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); return result; } @@ -418,18 +425,18 @@ namespace storm { groups.push_back(std::make_pair(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd1)), InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd2)))); } else if (ddGroupVariableIndices[currentLevel] < dd1->index) { if (ddGroupVariableIndices[currentLevel] < dd2->index) { - splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } else { - splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } } else if (ddGroupVariableIndices[currentLevel] < dd2->index) { - splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } else { - splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } } @@ -439,7 +446,7 @@ namespace storm { } template - void InternalAdd::toMatrixComponentsRec(DdNode const* dd, std::vector const& rowGroupOffsets, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { + void InternalAdd::toMatrixComponentsRec(DdNode const* dd, std::vector const& rowGroupOffsets, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { return; @@ -448,7 +455,7 @@ namespace storm { // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentRowLevel + currentColumnLevel == maxLevel) { if (generateValues) { - columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); + columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); } ++rowIndications[rowGroupOffsets[currentRowOffset]]; } else { @@ -770,5 +777,6 @@ namespace storm { } template class InternalAdd; + template class InternalAdd; } } \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index d16e4e093..2643912d0 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -41,6 +41,8 @@ namespace storm { template class InternalAdd { public: + friend class Odd; + /*! * Creates an ADD that encapsulates the given CUDD ADD. * @@ -580,7 +582,7 @@ namespace storm { * only works if the offsets given in rowIndications are already correct. If they need to be computed first, * this flag needs to be false. */ - void toMatrixComponentsRec(DdNode const* dd, std::vector const& rowGroupOffsets, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const; + void toMatrixComponentsRec(DdNode const* dd, std::vector const& rowGroupOffsets, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const; /*! * Builds an ADD representing the given vector. diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 8e53d9573..72d12d6ae 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -265,5 +265,10 @@ namespace storm { } } + template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); + template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); + + template InternalAdd InternalBdd::toAdd() const; + template InternalAdd InternalBdd::toAdd() const; } } \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 1fa776c3f..daf77db9b 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -37,6 +37,7 @@ namespace storm { class InternalBdd { public: friend class InternalAdd; + friend class Odd; /*! * Creates a DD that encapsulates the given CUDD ADD. diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp index a543cc24b..2e95913ea 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp @@ -84,5 +84,22 @@ namespace storm { void InternalDdManager::triggerReordering() { this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0); } + + Cudd& InternalDdManager::getCuddManager() { + return cuddManager; + } + + Cudd const& InternalDdManager::getCuddManager() const { + return cuddManager; + } + + template InternalAdd InternalDdManager::getAddOne() const; + template InternalAdd InternalDdManager::getAddOne() const; + + template InternalAdd InternalDdManager::getAddZero() const; + template InternalAdd InternalDdManager::getAddZero() const; + + template InternalAdd InternalDdManager::getConstant(double const& value) const; + template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; } } \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddDdManager.h b/src/storage/dd/cudd/InternalCuddDdManager.h index a967ca0dd..7e3b2e655 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.h +++ b/src/storage/dd/cudd/InternalCuddDdManager.h @@ -23,10 +23,12 @@ namespace storm { template<> class InternalDdManager { public: - friend class InternalAdd; friend class InternalBdd; friend class Odd; - + + template + friend class InternalAdd; + /*! * Creates a new internal manager for CUDD DDs. */ @@ -116,7 +118,7 @@ namespace storm { // The technique that is used for dynamic reordering. Cudd_ReorderingType reorderingTechnique; - }; + }; } } diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 15b1a3a7d..81856a665 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -13,9 +13,9 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/utility/constants.h" #include "src/exceptions/InvalidArgumentException.h" -#include "src/storage/dd/cudd/CuddBdd.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddDdManager.h" +#include "src/storage/dd/Bdd.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/DdManager.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -180,8 +180,8 @@ namespace storm { return result; } - template - storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound) { + template + storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd lastIterationStates = manager.getBddZero(); @@ -205,21 +205,21 @@ namespace storm { return statesWithProbabilityGreater0; } - template - storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { + template + storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { storm::dd::Bdd statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates()); statesWithProbability1 = !statesWithProbability1 && model.getReachableStates(); return statesWithProbability1; } - template - storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { storm::dd::Bdd statesWithProbabilityGreater0 = performProbGreater0(model, transitionMatrix, phiStates, psiStates); return performProb1(model, transitionMatrix, phiStates, psiStates, statesWithProbabilityGreater0); } - template - std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); result.first = performProbGreater0(model, transitionMatrix, phiStates, psiStates); @@ -228,8 +228,8 @@ namespace storm { return result; } - template - std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); result.first = performProbGreater0(model, transitionMatrixBdd, phiStates, psiStates); @@ -666,8 +666,8 @@ namespace storm { return performProb01Min(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates); } - template - storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd lastIterationStates = manager.getBddZero(); @@ -687,13 +687,13 @@ namespace storm { return statesWithProbabilityGreater0E; } - template - storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { return !performProbGreater0E(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); } - template - storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd lastIterationStates = manager.getBddZero(); @@ -714,13 +714,13 @@ namespace storm { return statesWithProbabilityGreater0A; } - template - storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { return !performProbGreater0A(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); } - template - storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { + template + storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd lastIterationStates = manager.getBddZero(); @@ -741,8 +741,8 @@ namespace storm { return statesWithProbability1A; } - template - storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) { + template + storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd statesWithProbability1E = statesWithProbabilityGreater0E; @@ -782,8 +782,8 @@ namespace storm { return statesWithProbability1E; } - template - std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); result.first = performProb0A(model, transitionMatrix, phiStates, psiStates); @@ -791,8 +791,8 @@ namespace storm { return result; } - template - std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + template + std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); result.first = performProb0E(model, transitionMatrix, phiStates, psiStates); @@ -1107,42 +1107,31 @@ namespace storm { #endif + template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); - template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0); - template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0); + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); - template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - - template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - - template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - - template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - - - template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); - - - template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; - - - template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - - - template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); } // namespace graph } // namespace utility diff --git a/src/utility/graph.h b/src/utility/graph.h index 30c26d3c2..b7a318b10 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -182,7 +182,7 @@ namespace storm { * @return All states with probability 1. */ template - storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 15d8a71ac..b6fd0ef8d 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -30,18 +30,18 @@ namespace storm { template - std::unique_ptr> SymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + std::unique_ptr> SymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { return std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs)); } template - std::unique_ptr> SymbolicMinMaxLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const { + std::unique_ptr> SymbolicMinMaxLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const { return std::unique_ptr>(new storm::solver::SymbolicMinMaxLinearEquationSolver(A, allRows, illegalMask, rowMetaVariables, columnMetaVariables, choiceVariables, rowColumnMetaVariablePairs)); } - template - std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { - return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); + template + std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { + return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); } template @@ -190,7 +190,7 @@ namespace storm { template class SymbolicLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; - template class SymbolicGameSolverFactory; + template class SymbolicGameSolverFactory; template class LinearEquationSolverFactory; template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; diff --git a/src/utility/solver.h b/src/utility/solver.h index 1b53deb80..cf2c63663 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -11,12 +11,24 @@ namespace storm { namespace solver { - template class SymbolicGameSolver; - template class SymbolicLinearEquationSolver; - template class SymbolicMinMaxLinearEquationSolver; - template class GameSolver; - template class LinearEquationSolver; - template class MinMaxLinearEquationSolver; + template + class SymbolicGameSolver; + + template + class SymbolicLinearEquationSolver; + + template + class SymbolicMinMaxLinearEquationSolver; + + template + class GameSolver; + + template + class LinearEquationSolver; + + template + class MinMaxLinearEquationSolver; + class LpSolver; class SmtSolver; @@ -60,7 +72,7 @@ namespace storm { template class SymbolicGameSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; template diff --git a/src/utility/storm.h b/src/utility/storm.h index b57bba2a1..8378d8367 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -34,8 +34,8 @@ #include "src/models/symbolic/Model.h" #include "src/models/symbolic/StandardRewardModel.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" #include "src/parser/AutoParser.h" diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index c89d578a2..dbf8c60d6 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -7,9 +7,6 @@ #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" -#include "src/storage/dd/cudd/CuddDd.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index a75910a8c..f453c86b8 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -50,7 +50,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); @@ -59,7 +59,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); @@ -68,7 +68,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); @@ -77,7 +77,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); @@ -86,7 +86,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); @@ -95,7 +95,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); @@ -104,7 +104,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); @@ -112,7 +112,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMax(), storm::settings::generalSettings().getPrecision()); } @@ -147,7 +147,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); @@ -156,7 +156,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); @@ -165,7 +165,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); @@ -174,7 +174,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); @@ -183,7 +183,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); @@ -191,7 +191,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); } @@ -219,7 +219,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); @@ -227,7 +227,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) { checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); @@ -270,7 +270,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); @@ -279,7 +279,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); @@ -288,7 +288,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); @@ -297,7 +297,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); @@ -306,7 +306,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); @@ -315,7 +315,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); @@ -323,7 +323,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); } diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index e9c195d80..ec9db7594 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -46,7 +46,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -55,7 +55,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -64,7 +64,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -73,7 +73,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(11.0/3.0, quantitativeResult4.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(11.0/3.0, quantitativeResult4.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -99,7 +99,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -108,7 +108,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.1522194965, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.1522194965, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -117,7 +117,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.32153724292835045, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.32153724292835045, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -151,7 +151,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -160,7 +160,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -169,7 +169,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 5be1cd015..1977803a5 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -48,7 +48,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -57,7 +57,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -66,7 +66,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -75,7 +75,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -84,7 +84,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -93,7 +93,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -102,7 +102,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -111,7 +111,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -145,7 +145,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -154,7 +154,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -163,7 +163,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -172,7 +172,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -181,7 +181,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -190,7 +190,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 69cfe01b0..ab991fa32 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -49,7 +49,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); @@ -58,7 +58,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); @@ -67,7 +67,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); @@ -76,7 +76,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); @@ -85,7 +85,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); @@ -94,7 +94,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); @@ -103,7 +103,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); } @@ -138,7 +138,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); @@ -147,7 +147,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); @@ -156,7 +156,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); @@ -165,7 +165,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); @@ -174,7 +174,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); } @@ -202,7 +202,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); } @@ -244,7 +244,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); @@ -253,7 +253,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); @@ -262,7 +262,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); @@ -271,7 +271,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); @@ -280,7 +280,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); @@ -289,7 +289,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); } diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index b01a87efa..81d410ab6 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -47,7 +47,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -56,7 +56,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -65,7 +65,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -74,7 +74,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -100,7 +100,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -109,7 +109,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -118,7 +118,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -152,7 +152,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -161,7 +161,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -170,7 +170,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index af1e54175..b5adab756 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -45,7 +45,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -54,7 +54,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -63,7 +63,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -72,7 +72,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -81,7 +81,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -90,7 +90,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -99,7 +99,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -108,7 +108,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -142,7 +142,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -151,7 +151,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -160,7 +160,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -169,7 +169,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -178,7 +178,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -187,7 +187,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856896106114934, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 487257138..a91eb0d30 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -45,7 +45,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -54,7 +54,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -63,7 +63,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -72,7 +72,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -98,7 +98,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -107,7 +107,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -116,7 +116,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -150,7 +150,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -159,7 +159,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -168,7 +168,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index c689a9edd..7cdf9ef25 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -45,7 +45,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -54,7 +54,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -63,7 +63,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -72,7 +72,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -81,7 +81,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -90,7 +90,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -99,7 +99,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -108,7 +108,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -142,7 +142,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -151,7 +151,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -160,7 +160,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -169,7 +169,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -178,7 +178,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -187,7 +187,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index 2fb6fe391..89a8f67b5 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -1,16 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/storage/dd/cudd/CuddDdManager.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" +#include "src/storage/dd/DdManager.h" #include "src/utility/solver.h" #include "src/settings/SettingsManager.h" #include "src/solver/SymbolicGameSolver.h" #include "src/settings/modules/NativeEquationSolverSettings.h" - TEST(FullySymbolicGameSolverTest, Solve) { // Create some variables. std::shared_ptr> manager(new storm::dd::DdManager()); @@ -26,45 +23,45 @@ TEST(FullySymbolicGameSolverTest, Solve) { std::set player2Variables({pl2.first}); // Construct simple game. - storm::dd::Add matrix = manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 2).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.6); - matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 1).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.4); + storm::dd::Add matrix = manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 2).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.6); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 1).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.4); - matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 2).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 1).toAdd() * manager->getConstant(0.2); - matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 3).toAdd() * manager->getEncoding(pl1.first, 0).toAdd() * manager->getEncoding(pl2.first, 1).toAdd() * manager->getConstant(0.8); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 2).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(0.2); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 3).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(0.8); - matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 3).toAdd() * manager->getEncoding(pl1.first, 1).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.5); - matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 4).toAdd() * manager->getEncoding(pl1.first, 1).toAdd() * manager->getEncoding(pl2.first, 0).toAdd() * manager->getConstant(0.5); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 3).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.5); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 4).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.5); - matrix += manager->getEncoding(state.first, 1).toAdd() * manager->getEncoding(state.second, 1).toAdd() * manager->getEncoding(pl1.first, 1).toAdd() * manager->getEncoding(pl2.first, 1).toAdd() * manager->getConstant(1); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 1).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(1); - std::unique_ptr> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory()); + std::unique_ptr> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory()); std::unique_ptr> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables); // Create solution and target state vector. - storm::dd::Add x = manager->getAddZero(); - storm::dd::Add b = manager->getEncoding(state.first, 2).toAdd() + manager->getEncoding(state.first, 4).toAdd(); + storm::dd::Add x = manager->template getAddZero(); + storm::dd::Add b = manager->getEncoding(state.first, 2).template toAdd() + manager->getEncoding(state.first, 4).template toAdd(); // Now solve the game with different strategies for the players. storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b); - result *= manager->getEncoding(state.first, 1).toAdd(); + result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); - x = manager->getAddZero(); + x = manager->getAddZero(); result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b); - result *= manager->getEncoding(state.first, 1).toAdd(); + result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.5, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); - x = manager->getAddZero(); + x = manager->getAddZero(); result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b); - result *= manager->getEncoding(state.first, 1).toAdd(); + result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.2, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); - x = manager->getAddZero(); + x = manager->getAddZero(); result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b); - result *= manager->getEncoding(state.first, 1).toAdd(); + result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); } \ No newline at end of file diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 9d86ad9f0..d4b578664 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -1,8 +1,8 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/exceptions/InvalidArgumentException.h" -#include "src/storage/dd/cudd/CuddDdManager.h" -#include "src/storage/dd/cudd/CuddAdd.h" +#include "src/storage/dd/DdManager.h" +#include "src/storage/dd/Add.h" #include "src/storage/dd/cudd/CuddOdd.h" #include "src/storage/dd/DdMetaVariable.h" #include "src/settings/SettingsManager.h" @@ -11,8 +11,8 @@ TEST(CuddDdManager, Constants) { std::shared_ptr> manager(new storm::dd::DdManager()); - storm::dd::Add zero; - ASSERT_NO_THROW(zero = manager->getAddZero()); + storm::dd::Add zero; + ASSERT_NO_THROW(zero = manager->template getAddZero()); EXPECT_EQ(0ul, zero.getNonZeroCount()); EXPECT_EQ(1ul, zero.getLeafCount()); @@ -20,8 +20,8 @@ TEST(CuddDdManager, Constants) { EXPECT_EQ(0, zero.getMin()); EXPECT_EQ(0, zero.getMax()); - storm::dd::Add one; - ASSERT_NO_THROW(one = manager->getAddOne()); + storm::dd::Add one; + ASSERT_NO_THROW(one = manager->template getAddOne()); EXPECT_EQ(1ul, one.getNonZeroCount()); EXPECT_EQ(1ul, one.getLeafCount()); @@ -29,8 +29,8 @@ TEST(CuddDdManager, Constants) { EXPECT_EQ(1, one.getMin()); EXPECT_EQ(1, one.getMax()); - storm::dd::Add two; - ASSERT_NO_THROW(two = manager->getConstant(2)); + storm::dd::Add two; + ASSERT_NO_THROW(two = manager->template getConstant(2)); EXPECT_EQ(1ul, two.getNonZeroCount()); EXPECT_EQ(1ul, two.getLeafCount()); @@ -72,8 +72,8 @@ TEST(CuddDdManager, EncodingTest) { EXPECT_EQ(1ul, encoding.getLeafCount()); // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. - EXPECT_EQ(6ul, encoding.toAdd().getNodeCount()); - EXPECT_EQ(2ul, encoding.toAdd().getLeafCount()); + EXPECT_EQ(6ul, encoding.template toAdd().getNodeCount()); + EXPECT_EQ(2ul, encoding.template toAdd().getLeafCount()); } TEST(CuddDdManager, RangeTest) { @@ -93,8 +93,8 @@ TEST(CuddDdManager, IdentityTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Add identity; - ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); + storm::dd::Add identity; + ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); EXPECT_EQ(9ul, identity.getNonZeroCount()); EXPECT_EQ(10ul, identity.getLeafCount()); @@ -104,33 +104,33 @@ TEST(CuddDdManager, IdentityTest) { TEST(CuddDd, OperatorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - EXPECT_TRUE(manager->getAddZero() == manager->getAddZero()); - EXPECT_FALSE(manager->getAddZero() == manager->getAddOne()); + EXPECT_TRUE(manager->template getAddZero() == manager->template getAddZero()); + EXPECT_FALSE(manager->template getAddZero() == manager->template getAddOne()); - EXPECT_FALSE(manager->getAddZero() != manager->getAddZero()); - EXPECT_TRUE(manager->getAddZero() != manager->getAddOne()); + EXPECT_FALSE(manager->template getAddZero() != manager->template getAddZero()); + EXPECT_TRUE(manager->template getAddZero() != manager->template getAddOne()); - storm::dd::Add dd1 = manager->getAddOne(); - storm::dd::Add dd2 = manager->getAddOne(); - storm::dd::Add dd3 = dd1 + dd2; - EXPECT_TRUE(dd3 == manager->getConstant(2)); + storm::dd::Add dd1 = manager->template getAddOne(); + storm::dd::Add dd2 = manager->template getAddOne(); + storm::dd::Add dd3 = dd1 + dd2; + EXPECT_TRUE(dd3 == manager->template getConstant(2)); - dd3 += manager->getAddZero(); - EXPECT_TRUE(dd3 == manager->getConstant(2)); + dd3 += manager->template getAddZero(); + EXPECT_TRUE(dd3 == manager->template getConstant(2)); - dd3 = dd1 * manager->getConstant(3); - EXPECT_TRUE(dd3 == manager->getConstant(3)); + dd3 = dd1 * manager->template getConstant(3); + EXPECT_TRUE(dd3 == manager->template getConstant(3)); - dd3 *= manager->getConstant(2); - EXPECT_TRUE(dd3 == manager->getConstant(6)); + dd3 *= manager->template getConstant(2); + EXPECT_TRUE(dd3 == manager->template getConstant(6)); dd3 = dd1 - dd2; EXPECT_TRUE(dd3.isZero()); - dd3 -= manager->getConstant(-2); - EXPECT_TRUE(dd3 == manager->getConstant(2)); + dd3 -= manager->template getConstant(-2); + EXPECT_TRUE(dd3 == manager->template getConstant(2)); - dd3 /= manager->getConstant(2); + dd3 /= manager->template getConstant(2); EXPECT_TRUE(dd3.isOne()); dd3 = !dd3; @@ -142,13 +142,13 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1 || dd2; EXPECT_TRUE(dd3.isOne()); - dd1 = manager->getIdentity(x.first); - dd2 = manager->getConstant(5); + dd1 = manager->template getIdentity(x.first); + dd2 = manager->template getConstant(5); dd3 = dd1.equals(dd2); EXPECT_EQ(1ul, dd3.getNonZeroCount()); - storm::dd::Add dd4 = dd1.notEquals(dd2); + storm::dd::Add dd4 = dd1.notEquals(dd2); EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd()); dd3 = dd1.less(dd2); @@ -163,22 +163,22 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1.greaterOrEqual(dd2); EXPECT_EQ(5ul, dd3.getNonZeroCount()); - dd3 = (manager->getEncoding(x.first, 2).toAdd()).ite(dd2, dd1); + dd3 = (manager->getEncoding(x.first, 2).template toAdd()).ite(dd2, dd1); dd4 = dd3.less(dd2); EXPECT_EQ(10ul, dd4.getNonZeroCount()); dd4 = dd3.minimum(dd1); - dd4 *= manager->getEncoding(x.first, 2).toAdd(); + dd4 *= manager->getEncoding(x.first, 2).template toAdd(); dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(2, dd4.getValue()); dd4 = dd3.maximum(dd1); - dd4 *= manager->getEncoding(x.first, 2).toAdd(); + dd4 *= manager->getEncoding(x.first, 2).template toAdd(); dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(5, dd4.getValue()); - dd1 = manager->getConstant(0.01); - dd2 = manager->getConstant(0.01 + 1e-6); + dd1 = manager->template getConstant(0.01); + dd2 = manager->template getConstant(0.01 + 1e-6); EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false)); EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6)); } @@ -186,43 +186,43 @@ TEST(CuddDd, OperatorTest) { TEST(CuddDd, AbstractionTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Add dd1; - storm::dd::Add dd2; - storm::dd::Add dd3; + storm::dd::Add dd1; + storm::dd::Add dd2; + storm::dd::Add dd3; - dd1 = manager->getIdentity(x.first); - dd2 = manager->getConstant(5); + dd1 = manager->template getIdentity(x.first); + dd2 = manager->template getConstant(5); dd3 = dd1.equals(dd2); storm::dd::Bdd dd3Bdd = dd3.toBdd(); EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.first})); EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); - EXPECT_EQ(1, dd3Bdd.toAdd().getMax()); + EXPECT_EQ(1, dd3Bdd.template toAdd().getMax()); dd3 = dd1.equals(dd2); - dd3 *= manager->getConstant(3); + dd3 *= manager->template getConstant(3); EXPECT_EQ(1ul, dd3.getNonZeroCount()); ASSERT_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.first})); EXPECT_TRUE(dd3Bdd.isOne()); dd3 = dd1.equals(dd2); - dd3 *= manager->getConstant(3); + dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); EXPECT_EQ(1ul, dd3.getNonZeroCount()); EXPECT_EQ(3, dd3.getMax()); dd3 = dd1.equals(dd2); - dd3 *= manager->getConstant(3); + dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first})); EXPECT_EQ(0ul, dd3.getNonZeroCount()); EXPECT_EQ(0, dd3.getMax()); dd3 = dd1.equals(dd2); - dd3 *= manager->getConstant(3); + dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); EXPECT_EQ(1ul, dd3.getNonZeroCount()); @@ -234,34 +234,34 @@ TEST(CuddDd, SwapTest) { std::pair x = manager->addMetaVariable("x", 1, 9); std::pair z = manager->addMetaVariable("z", 2, 8); - storm::dd::Add dd1; - storm::dd::Add dd2; + storm::dd::Add dd1; + storm::dd::Add dd2; - dd1 = manager->getIdentity(x.first); + dd1 = manager->template getIdentity(x.first); ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, x.second)})); - EXPECT_TRUE(dd1 == manager->getIdentity(x.second)); + EXPECT_TRUE(dd1 == manager->template getIdentity(x.second)); } TEST(CuddDd, MultiplyMatrixTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Add dd1 = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)); - storm::dd::Add dd2 = manager->getRange(x.second).toAdd(); - storm::dd::Add dd3; - dd1 *= manager->getConstant(2); + storm::dd::Add dd1 = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)); + storm::dd::Add dd2 = manager->getRange(x.second).template toAdd(); + storm::dd::Add dd3; + dd1 *= manager->template getConstant(2); ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second})); ASSERT_NO_THROW(dd3 = dd3.swapVariables({std::make_pair(x.first, x.second)})); - EXPECT_TRUE(dd3 == dd2 * manager->getConstant(2)); + EXPECT_TRUE(dd3 == dd2 * manager->template getConstant(2)); } TEST(CuddDd, GetSetValueTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Add dd1 = manager->getAddOne(); + storm::dd::Add dd1 = manager->template getAddOne(); ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); EXPECT_EQ(2ul, dd1.getLeafCount()); @@ -279,10 +279,10 @@ TEST(CuddDd, ForwardIteratorTest) { std::pair x = manager->addMetaVariable("x", 1, 9); std::pair y = manager->addMetaVariable("y", 0, 3); - storm::dd::Add dd; - ASSERT_NO_THROW(dd = manager->getRange(x.first).toAdd()); + storm::dd::Add dd; + ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd()); - storm::dd::DdForwardIterator it, ite; + storm::dd::AddIterator it, ite; ASSERT_NO_THROW(it = dd.begin()); ASSERT_NO_THROW(ite = dd.end()); std::pair valuationValuePair; @@ -294,8 +294,8 @@ TEST(CuddDd, ForwardIteratorTest) { } EXPECT_EQ(9ul, numberOfValuations); - dd = manager->getRange(x.first).toAdd(); - dd = dd.ite(manager->getAddOne(), manager->getAddOne()); + dd = manager->getRange(x.first).template toAdd(); + dd = dd.ite(manager->template getAddOne(), manager->template getAddOne()); ASSERT_NO_THROW(it = dd.begin()); ASSERT_NO_THROW(ite = dd.end()); numberOfValuations = 0; @@ -322,28 +322,28 @@ TEST(CuddDd, AddOddTest) { std::pair a = manager->addMetaVariable("a"); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Add dd = manager->getIdentity(x.first); + storm::dd::Add dd = manager->template getIdentity(x.first); storm::dd::Odd odd; ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); EXPECT_EQ(9ul, odd.getTotalOffset()); EXPECT_EQ(12ul, odd.getNodeCount()); std::vector ddAsVector; - ASSERT_NO_THROW(ddAsVector = dd.toVector()); + ASSERT_NO_THROW(ddAsVector = dd.toVector()); EXPECT_EQ(9ul, ddAsVector.size()); for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { EXPECT_TRUE(i+1 == ddAsVector[i]); } // Create a non-trivial matrix. - dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first).toAdd(); - dd += manager->getEncoding(x.first, 1).toAdd() * manager->getRange(x.second).toAdd() + manager->getEncoding(x.second, 1).toAdd() * manager->getRange(x.first).toAdd(); + dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); + dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); // Create the ODDs. storm::dd::Odd rowOdd; - ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange(x.first).toAdd())); + ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange(x.first).template toAdd())); storm::dd::Odd columnOdd; - ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange(x.second).toAdd())); + ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange(x.second).template toAdd())); // Try to translate the matrix. storm::storage::SparseMatrix matrix; @@ -353,7 +353,7 @@ TEST(CuddDd, AddOddTest) { EXPECT_EQ(9ul, matrix.getColumnCount()); EXPECT_EQ(25ul, matrix.getNonzeroEntryCount()); - dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); + dd = manager->getRange(x.first).template toAdd() * manager->getRange(x.second).template toAdd() * manager->getEncoding(a.first, 0).template toAdd().ite(dd, dd + manager->template getConstant(1)); ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); EXPECT_EQ(18ul, matrix.getRowCount()); EXPECT_EQ(9ul, matrix.getRowGroupCount()); @@ -366,25 +366,24 @@ TEST(CuddDd, BddOddTest) { std::pair a = manager->addMetaVariable("a"); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Add dd = manager->getIdentity(x.first); + storm::dd::Add dd = manager->template getIdentity(x.first); storm::dd::Odd odd; ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); EXPECT_EQ(9ul, odd.getTotalOffset()); EXPECT_EQ(12ul, odd.getNodeCount()); std::vector ddAsVector; - ASSERT_NO_THROW(ddAsVector = dd.toVector()); + ASSERT_NO_THROW(ddAsVector = dd.toVector()); EXPECT_EQ(9ul, ddAsVector.size()); for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { EXPECT_TRUE(i+1 == ddAsVector[i]); } - storm::dd::Add vectorAdd(manager, ddAsVector, odd, {x.first}); - EXPECT_EQ(dd, vectorAdd); + storm::dd::Add vectorAdd = storm::dd::Add::fromVector(manager, ddAsVector, odd, {x.first}); // Create a non-trivial matrix. - dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first).toAdd(); - dd += manager->getEncoding(x.first, 1).toAdd() * manager->getRange(x.second).toAdd() + manager->getEncoding(x.second, 1).toAdd() * manager->getRange(x.first).toAdd(); + dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); + dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); // Create the ODDs. storm::dd::Odd rowOdd; @@ -400,7 +399,7 @@ TEST(CuddDd, BddOddTest) { EXPECT_EQ(9ul, matrix.getColumnCount()); EXPECT_EQ(25ul, matrix.getNonzeroEntryCount()); - dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); + dd = manager->getRange(x.first).template toAdd() * manager->getRange(x.second).template toAdd() * manager->getEncoding(a.first, 0).template toAdd().ite(dd, dd + manager->template getConstant(1)); ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); EXPECT_EQ(18ul, matrix.getRowCount()); EXPECT_EQ(9ul, matrix.getRowGroupCount()); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 721f99c5f..d92b6e887 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -1,7 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/storage/dd/cudd/CuddDd.h" #include "src/parser/PrismParser.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" @@ -12,9 +11,9 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/utility/graph.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" -#include "src/storage/dd/cudd/CuddDdManager.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" +#include "src/storage/dd/DdManager.h" TEST(GraphTest, SymbolicProb01) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");