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

Some changes in anticipation of integrating MEDDLY. 

Former-commit-id: 0f7a71ec9b
tempestpy_adaptions
dehnert 11 years ago
parent
45486600f7
commit
6a2d75d68d
5 changed files with 197 additions and 196 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storage/dd/CuddDdManager.h
  2. 52
      src/storage/dd/CuddDdMetaVariable.cpp
  3. 138
      src/storage/dd/CuddDdMetaVariable.h
  4. 65
      src/storage/dd/DdMetaVariable.cpp
  5. 136
      src/storage/dd/DdMetaVariable.h

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

@ -4,7 +4,7 @@
#include <unordered_map> #include <unordered_map>
#include "src/storage/dd/DdManager.h" #include "src/storage/dd/DdManager.h"
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/dd/CuddDdMetaVariable.h"
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"
// Include the C++-interface of CUDD. // Include the C++-interface of CUDD.

52
src/storage/dd/CuddDdMetaVariable.cpp
View File

@ -0,0 +1,52 @@
#include "src/storage/dd/CuddDdMetaVariable.h"
#include "src/storage/dd/CuddDdManager.h"
namespace storm {
namespace dd {
DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
// Create the cube of all variables of this meta variable.
for (auto const& ddVariable : this->ddVariables) {
this->cube *= ddVariable;
}
}
DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
// Create the cube of all variables of this meta variable.
for (auto const& ddVariable : this->ddVariables) {
this->cube *= ddVariable;
}
}
std::string const& DdMetaVariable<DdType::CUDD>::getName() const {
return this->name;
}
typename DdMetaVariable<DdType::CUDD>::MetaVariableType DdMetaVariable<DdType::CUDD>::getType() const {
return this->type;
}
int_fast64_t DdMetaVariable<DdType::CUDD>::getLow() const {
return this->low;
}
int_fast64_t DdMetaVariable<DdType::CUDD>::getHigh() const {
return this->high;
}
std::size_t DdMetaVariable<DdType::CUDD>::getNumberOfDdVariables() const {
return this->ddVariables.size();
}
std::shared_ptr<DdManager<DdType::CUDD>> DdMetaVariable<DdType::CUDD>::getDdManager() const {
return this->manager;
}
std::vector<Dd<DdType::CUDD>> const& DdMetaVariable<DdType::CUDD>::getDdVariables() const {
return this->ddVariables;
}
Dd<DdType::CUDD> const& DdMetaVariable<DdType::CUDD>::getCube() const {
return this->cube;
}
}
}

138
src/storage/dd/CuddDdMetaVariable.h
View File

@ -0,0 +1,138 @@
#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_
#define STORM_STORAGE_DD_DDMETAVARIABLE_H_
#include <memory>
#include <vector>
#include <cstdint>
#include <string>
#include "utility/OsDetection.h"
#include "src/storage/dd/CuddDd.h"
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/expressions/Expression.h"
namespace storm {
namespace dd {
// Forward-declare the DdManager class.
template<DdType Type> class DdManager;
template<>
class DdMetaVariable<DdType::CUDD> {
public:
// Declare the DdManager class as friend so it can access the internals of a meta variable.
friend class DdManager<DdType::CUDD>;
friend class Dd<DdType::CUDD>;
friend class DdForwardIterator<DdType::CUDD>;
// An enumeration for all legal types of meta variables.
enum class MetaVariableType { Bool, Int };
/*!
* Creates an integer meta variable with the given name and range bounds.
*
* @param name The name of the meta variable.
* @param low The lowest value of the range of the variable.
* @param high The highest value of the range of the variable.
* @param ddVariables The vector of variables used to encode this variable.
* @param manager A pointer to the manager that is responsible for this meta variable.
*/
DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
/*!
* Creates a boolean meta variable with the given name.
* @param name The name of the meta variable.
* @param ddVariables The vector of variables used to encode this variable.
* @param manager A pointer to the manager that is responsible for this meta variable.
*/
DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
// Explictly generate all default versions of copy/move constructors/assignments.
DdMetaVariable(DdMetaVariable const& other) = default;
DdMetaVariable& operator=(DdMetaVariable const& other) = default;
#ifndef WINDOWS
DdMetaVariable(DdMetaVariable&& other) = default;
DdMetaVariable& operator=(DdMetaVariable&& other) = default;
#endif
/*!
* Retrieves the name of the meta variable.
*
* @return The name of the variable.
*/
std::string const& getName() const;
/*!
* Retrieves the type of the meta variable.
*
* @return The type of the meta variable.
*/
MetaVariableType getType() const;
/*!
* Retrieves the lowest value of the range of the variable.
*
* @return The lowest value of the range of the variable.
*/
int_fast64_t getLow() const;
/*!
* Retrieves the highest value of the range of the variable.
*
* @return The highest value of the range of the variable.
*/
int_fast64_t getHigh() const;
/*!
* Retrieves the manager that is responsible for this meta variable.
*
* A pointer to the manager that is responsible for this meta variable.
*/
std::shared_ptr<DdManager<DdType::CUDD>> getDdManager() const;
/*!
* Retrieves the number of DD variables for this meta variable.
*
* @return The number of DD variables for this meta variable.
*/
std::size_t getNumberOfDdVariables() const;
private:
/*!
* Retrieves the variables used to encode the meta variable.
*
* @return A vector of variables used to encode the meta variable.
*/
std::vector<Dd<DdType::CUDD>> const& getDdVariables() const;
/*!
* Retrieves the cube of all variables that encode this meta variable.
*
* @return The cube of all variables that encode this meta variable.
*/
Dd<DdType::CUDD> const& getCube() const;
// The name of the meta variable.
std::string name;
// The type of the variable.
MetaVariableType type;
// The lowest value of the range of the variable.
int_fast64_t low;
// The highest value of the range of the variable.
int_fast64_t high;
// The vector of variables that are used to encode the meta variable.
std::vector<Dd<DdType::CUDD>> ddVariables;
// The cube consisting of all variables that encode the meta variable.
Dd<DdType::CUDD> cube;
// A pointer to the manager responsible for this meta variable.
std::shared_ptr<DdManager<DdType::CUDD>> manager;
};
}
}
#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */

65
src/storage/dd/DdMetaVariable.cpp
View File

@ -1,65 +0,0 @@
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/dd/CuddDdManager.h"
namespace storm {
namespace dd {
template<DdType Type>
DdMetaVariable<Type>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
// Create the cube of all variables of this meta variable.
for (auto const& ddVariable : this->ddVariables) {
this->cube *= ddVariable;
}
}
template<DdType Type>
DdMetaVariable<Type>::DdMetaVariable(std::string const& name, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
// Create the cube of all variables of this meta variable.
for (auto const& ddVariable : this->ddVariables) {
this->cube *= ddVariable;
}
}
template<DdType Type>
std::string const& DdMetaVariable<Type>::getName() const {
return this->name;
}
template<DdType Type>
typename DdMetaVariable<Type>::MetaVariableType DdMetaVariable<Type>::getType() const {
return this->type;
}
template<DdType Type>
int_fast64_t DdMetaVariable<Type>::getLow() const {
return this->low;
}
template<DdType Type>
int_fast64_t DdMetaVariable<Type>::getHigh() const {
return this->high;
}
template<DdType Type>
std::size_t DdMetaVariable<Type>::getNumberOfDdVariables() const {
return this->ddVariables.size();
}
template<DdType Type>
std::shared_ptr<DdManager<Type>> DdMetaVariable<Type>::getDdManager() const {
return this->manager;
}
template<DdType Type>
std::vector<Dd<Type>> const& DdMetaVariable<Type>::getDdVariables() const {
return this->ddVariables;
}
template<DdType Type>
Dd<Type> const& DdMetaVariable<Type>::getCube() const {
return this->cube;
}
// Explicitly instantiate DdMetaVariable.
template class DdMetaVariable<DdType::CUDD>;
}
}

136
src/storage/dd/DdMetaVariable.h
View File

@ -1,137 +1,13 @@
#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_
#define STORM_STORAGE_DD_DDMETAVARIABLE_H_
#ifndef STORM_STORAGE_DD_DDMETAVARIBLE_H_
#define STORM_STORAGE_DD_DDMETAVARIBLE_H_
#include <memory>
#include <vector>
#include <cstdint>
#include <string>
#include "utility/OsDetection.h"
#include "src/storage/dd/CuddDd.h"
#include "src/storage/expressions/Expression.h"
#include "src/storage/dd/DdType.h"
namespace storm { namespace storm {
namespace dd { namespace dd {
// Forward-declare the DdManager class.
template<DdType Type> class DdManager;
template <DdType Type>
class DdMetaVariable {
public:
// Declare the DdManager class as friend so it can access the internals of a meta variable.
friend class DdManager<Type>;
friend class Dd<Type>;
friend class DdForwardIterator<Type>;
// An enumeration for all legal types of meta variables.
enum class MetaVariableType { Bool, Int };
/*!
* Creates an integer meta variable with the given name and range bounds.
*
* @param name The name of the meta variable.
* @param low The lowest value of the range of the variable.
* @param high The highest value of the range of the variable.
* @param ddVariables The vector of variables used to encode this variable.
* @param manager A pointer to the manager that is responsible for this meta variable.
*/
DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager);
/*!
* Creates a boolean meta variable with the given name.
* @param name The name of the meta variable.
* @param ddVariables The vector of variables used to encode this variable.
* @param manager A pointer to the manager that is responsible for this meta variable.
*/
DdMetaVariable(std::string const& name, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager);
// Explictly generate all default versions of copy/move constructors/assignments.
DdMetaVariable(DdMetaVariable const& other) = default;
DdMetaVariable& operator=(DdMetaVariable const& other) = default;
#ifndef WINDOWS
DdMetaVariable(DdMetaVariable&& other) = default;
DdMetaVariable& operator=(DdMetaVariable&& other) = default;
#endif
/*!
* Retrieves the name of the meta variable.
*
* @return The name of the variable.
*/
std::string const& getName() const;
/*!
* Retrieves the type of the meta variable.
*
* @return The type of the meta variable.
*/
MetaVariableType getType() const;
/*!
* Retrieves the lowest value of the range of the variable.
*
* @return The lowest value of the range of the variable.
*/
int_fast64_t getLow() const;
/*!
* Retrieves the highest value of the range of the variable.
*
* @return The highest value of the range of the variable.
*/
int_fast64_t getHigh() const;
/*!
* Retrieves the manager that is responsible for this meta variable.
*
* A pointer to the manager that is responsible for this meta variable.
*/
std::shared_ptr<DdManager<Type>> getDdManager() const;
/*!
* Retrieves the number of DD variables for this meta variable.
*
* @return The number of DD variables for this meta variable.
*/
std::size_t getNumberOfDdVariables() const;
private:
/*!
* Retrieves the variables used to encode the meta variable.
*
* @return A vector of variables used to encode the meta variable.
*/
std::vector<Dd<Type>> const& getDdVariables() const;
/*!
* Retrieves the cube of all variables that encode this meta variable.
*
* @return The cube of all variables that encode this meta variable.
*/
Dd<Type> const& getCube() const;
// The name of the meta variable.
std::string name;
// The type of the variable.
MetaVariableType type;
// The lowest value of the range of the variable.
int_fast64_t low;
// The highest value of the range of the variable.
int_fast64_t high;
// The vector of variables that are used to encode the meta variable.
std::vector<Dd<Type>> ddVariables;
// The cube consisting of all variables that encode the meta variable.
Dd<Type> cube;
// A pointer to the manager responsible for this meta variable.
std::shared_ptr<DdManager<Type>> manager;
};
// Declare DdMetaVariable class so we can then specialize it for the different DD types.
template<DdType Type> class DdMetaVariable;
} }
} }
#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */
#endif /* STORM_STORAGE_DD_DDMETAVARIBLE_H_ */
Write Preview
Loading…
Cancel
Save