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

Started writing functional tests for DD abstraction layer and fixed some bugs on the way. 

Former-commit-id: 8a2fc118be
tempestpy_adaptions
dehnert 11 years ago
parent
2fcb12e875
commit
a4fec9f080
5 changed files with 114 additions and 8 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storage/dd/CuddDd.cpp
  2. 2
      src/storage/dd/CuddDd.h
  3. 47
      src/storage/dd/CuddDdManager.cpp
  4. 15
      src/storage/dd/CuddDdManager.h
  5. 54
      test/functional/storage/CuddDdTest.cpp

4
src/storage/dd/CuddDd.cpp
View File

@ -263,12 +263,12 @@ namespace storm {
double Dd<CUDD>::getMin() const {
ADD constantMinAdd = this->getCuddAdd().FindMin();
return static_cast<double>(Cudd_V(constantMinAdd));
return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
}
double Dd<CUDD>::getMax() const {
ADD constantMaxAdd = this->getCuddAdd().FindMax();
return static_cast<double>(Cudd_V(constantMaxAdd));
return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
}
void Dd<CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) {

2
src/storage/dd/CuddDd.h
View File

@ -390,7 +390,7 @@ namespace storm {
* @param cuddAdd The CUDD ADD to store.
* @param
*/
Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames);
Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames = std::set<std::string>());
// A pointer to the manager responsible for this DD.
std::shared_ptr<DdManager<CUDD>> ddManager;

47
src/storage/dd/CuddDdManager.cpp
View File

@ -1,8 +1,11 @@
#include <cmath>
#include <algorithm>
#include "src/storage/dd/CuddDdManager.h"
#include "src/exceptions/InvalidArgumentException.h"
#include <iostream>
namespace storm {
namespace dd {
DdManager<CUDD>::DdManager() : metaVariableMap(), cuddManager() {
@ -10,15 +13,15 @@ namespace storm {
}
Dd<CUDD> DdManager<CUDD>::getOne() {
return Dd<CUDD>(this->shared_from_this(), cuddManager.addOne(), {""});
return Dd<CUDD>(this->shared_from_this(), cuddManager.addOne());
}
Dd<CUDD> DdManager<CUDD>::getZero() {
return Dd<CUDD>(this->shared_from_this(), cuddManager.addZero(), {""});
return Dd<CUDD>(this->shared_from_this(), cuddManager.addZero());
}
Dd<CUDD> DdManager<CUDD>::getConstant(double value) {
return Dd<CUDD>(this->shared_from_this(), cuddManager.constant(value), {""});
return Dd<CUDD>(this->shared_from_this(), cuddManager.constant(value));
}
Dd<CUDD> DdManager<CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
@ -53,6 +56,12 @@ namespace storm {
}
void DdManager<CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
// Check whether a meta variable already exists.
if (this->containsMetaVariable(name)) {
throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists.";
}
// Check that the range is legal.
if (high == low) {
throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements.";
}
@ -68,13 +77,33 @@ namespace storm {
}
void DdManager<CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) {
// Make sure that at least one meta variable is added.
if (names.size() == 0) {
throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables.";
}
// Check that there are no duplicate names in the given name vector.
std::vector<std::string> nameCopy(names);
std::sort(nameCopy.begin(), nameCopy.end());
if (std::adjacent_find(nameCopy.begin(), nameCopy.end()) != nameCopy.end()) {
throw storm::exceptions::InvalidArgumentException() << "Cannot add duplicate meta variables.";
}
// Check that the range is legal.
if (high == low) {
throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements.";
}
// Check whether a meta variable already exists.
for (auto const& metaVariableName : names) {
if (this->containsMetaVariable(metaVariableName)) {
throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << metaVariableName << "' already exists.";
}
}
// Add the variables in interleaved order.
std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low)));
std::vector<std::vector<Dd<CUDD>>> variables;
std::vector<std::vector<Dd<CUDD>>> variables(names.size());
for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
for (uint_fast64_t i = 0; i < names.size(); ++i) {
variables[i].emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]}));
@ -90,7 +119,7 @@ namespace storm {
DdMetaVariable<CUDD> const& DdManager<CUDD>::getMetaVariable(std::string const& metaVariableName) const {
auto const& nameVariablePair = metaVariableMap.find(metaVariableName);
if (nameVariablePair == metaVariableMap.end()) {
if (!this->containsMetaVariable(metaVariableName)) {
throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name.";
}
@ -105,6 +134,14 @@ namespace storm {
return result;
}
std::size_t DdManager<CUDD>::getNumberOfMetaVariables() const {
return this->metaVariableMap.size();
}
bool DdManager<CUDD>::containsMetaVariable(std::string const& metaVariableName) const {
return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end();
}
Cudd& DdManager<CUDD>::getCuddManager() {
return this->cuddManager;
}

15
src/storage/dd/CuddDdManager.h
View File

@ -106,6 +106,21 @@ namespace storm {
*/
std::set<std::string> getAllMetaVariableNames() const;
/*!
* Retrieves the number of meta variables that are contained in this manager.
*
* @return The number of meta variables contained in this manager.
*/
std::size_t getNumberOfMetaVariables() const;
/*!
* Retrieves whether the given meta variable name is already in use.
*
* @param metaVariableName The meta variable name whose membership to query.
* @return True if the given meta variable name is managed by this manager.
*/
bool containsMetaVariable(std::string const& metaVariableName) const;
private:
/*!
* Retrieves the underlying CUDD manager.

54
test/functional/storage/CuddDdTest.cpp
View File

@ -0,0 +1,54 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddDd.h"
#include "src/storage/dd/DdMetaVariable.h"
TEST(CuddDdManager, Constants) {
std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
storm::dd::Dd<storm::dd::CUDD> zero;
ASSERT_NO_THROW(zero = manager->getZero());
EXPECT_EQ(0, zero.getNonZeroCount());
EXPECT_EQ(1, zero.getLeafCount());
EXPECT_EQ(1, zero.getNodeCount());
EXPECT_EQ(0, zero.getMin());
EXPECT_EQ(0, zero.getMax());
storm::dd::Dd<storm::dd::CUDD> one;
ASSERT_NO_THROW(one = manager->getOne());
EXPECT_EQ(1, one.getNonZeroCount());
EXPECT_EQ(1, one.getLeafCount());
EXPECT_EQ(1, one.getNodeCount());
EXPECT_EQ(1, one.getMin());
EXPECT_EQ(1, one.getMax());
storm::dd::Dd<storm::dd::CUDD> two;
ASSERT_NO_THROW(two = manager->getConstant(2));
EXPECT_EQ(1, two.getNonZeroCount());
EXPECT_EQ(1, two.getLeafCount());
EXPECT_EQ(1, two.getNodeCount());
EXPECT_EQ(2, two.getMin());
EXPECT_EQ(2, two.getMax());
}
TEST(CuddDdManager, AddMetaVariableTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
EXPECT_EQ(1, manager->getNumberOfMetaVariables());
std::vector<std::string> names = {"x", "x'"};
ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException);
names = {"y", "y"};
ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException);
names = {"y", "y'"};
ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3));
EXPECT_EQ(3, manager->getNumberOfMetaVariables());
}
Write Preview
Loading…
Cancel
Save