Browse Source
Added symbolic models and made DD-based model generator build the correct instances.
Added symbolic models and made DD-based model generator build the correct instances.
Former-commit-id: c054401cfd
main
dehnert
11 years ago
20 changed files with 900 additions and 57 deletions
-
3CMakeLists.txt
-
34src/builder/DdPrismModelBuilder.cpp
-
15src/builder/DdPrismModelBuilder.h
-
10src/builder/ExplicitPrismModelBuilder.cpp
-
2src/builder/ExplicitPrismModelBuilder.h
-
7src/models/ModelBase.h
-
2src/models/sparse/Model.cpp
-
1src/models/sparse/Model.h
-
2src/models/sparse/NondeterministicModel.cpp
-
30src/models/symbolic/DeterministicModel.cpp
-
63src/models/symbolic/DeterministicModel.h
-
29src/models/symbolic/Dtmc.cpp
-
61src/models/symbolic/Dtmc.h
-
30src/models/symbolic/Mdp.cpp
-
65src/models/symbolic/Mdp.h
-
137src/models/symbolic/Model.cpp
-
238src/models/symbolic/Model.h
-
60src/models/symbolic/NondeterministicModel.cpp
-
86src/models/symbolic/NondeterministicModel.h
-
82test/functional/builder/DdPrismModelBuilderTest.cpp
@ -0,0 +1,30 @@ |
|||
#include "src/models/symbolic/DeterministicModel.h"
|
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
template<storm::dd::DdType Type> |
|||
DeterministicModel<Type>::DeterministicModel(storm::models::ModelType const& modelType, |
|||
std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix) |
|||
: Model<Type>(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
// Explicitly instantiate the template class.
|
|||
template class DeterministicModel<storm::dd::DdType::CUDD>; |
|||
|
|||
} // namespace symbolic
|
|||
} // namespace models
|
|||
} // namespace storm
|
|||
@ -0,0 +1,63 @@ |
|||
#ifndef STORM_MODELS_SYMBOLIC_DETERMINISTICMODEL_H_ |
|||
#define STORM_MODELS_SYMBOLIC_DETERMINISTICMODEL_H_ |
|||
|
|||
#include "src/models/symbolic/Model.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
/*! |
|||
* Base class for all deterministic symbolic models. |
|||
*/ |
|||
template<storm::dd::DdType Type> |
|||
class DeterministicModel : public Model<Type> { |
|||
public: |
|||
DeterministicModel(DeterministicModel<Type> const& other) = default; |
|||
DeterministicModel& operator=(DeterministicModel<Type> const& other) = default; |
|||
|
|||
#ifndef WINDOWS |
|||
DeterministicModel(DeterministicModel<Type>&& other) = default; |
|||
DeterministicModel& operator=(DeterministicModel<Type>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Constructs a model from the given data. |
|||
* |
|||
* @param modelType The type of the model. |
|||
* @param manager The manager responsible for the decision diagrams. |
|||
* @param reachableStates A DD representing the reachable states. |
|||
* @param initialStates A DD representing the initial states of the model. |
|||
* @param transitionMatrix The matrix representing the transitions in the model. |
|||
* @param rowVariables The set of row meta variables used in the DDs. |
|||
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row |
|||
* meta variables. |
|||
* @param columVariables The set of column meta variables used in the DDs. |
|||
* @param columnExpressionAdapter An object that can be used to translate expressions in terms of the |
|||
* column meta variables. |
|||
* @param rowColumnMetaVariablePairs All pairs of row/column meta variables. |
|||
* @param labelToExpressionMap A mapping from label names to their defining expressions. |
|||
* @param optionalStateRewardVector The reward values associated with the states. |
|||
* @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
DeterministicModel(storm::models::ModelType const& modelType, |
|||
std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>()); |
|||
}; |
|||
|
|||
} // namespace symbolic |
|||
} // namespace models |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_SYMBOLIC_DETERMINISTICMODEL_H_ */ |
|||
@ -0,0 +1,29 @@ |
|||
#include "src/models/symbolic/Dtmc.h"
|
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
template<storm::dd::DdType Type> |
|||
Dtmc<Type>::Dtmc(std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix) |
|||
: DeterministicModel<Type>(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
// Explicitly instantiate the template class.
|
|||
template class Dtmc<storm::dd::DdType::CUDD>; |
|||
|
|||
} // namespace symbolic
|
|||
} // namespace models
|
|||
} // namespace storm
|
|||
@ -0,0 +1,61 @@ |
|||
#ifndef STORM_MODELS_SYMBOLIC_DTMC_H_ |
|||
#define STORM_MODELS_SYMBOLIC_DTMC_H_ |
|||
|
|||
#include "src/models/symbolic/DeterministicModel.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
/*! |
|||
* This class represents a discrete-time Markov chain. |
|||
*/ |
|||
template<storm::dd::DdType Type> |
|||
class Dtmc : public DeterministicModel<Type> { |
|||
public: |
|||
Dtmc(Dtmc<Type> const& other) = default; |
|||
Dtmc& operator=(Dtmc<Type> const& other) = default; |
|||
|
|||
#ifndef WINDOWS |
|||
Dtmc(Dtmc<Type>&& other) = default; |
|||
Dtmc& operator=(Dtmc<Type>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Constructs a model from the given data. |
|||
* |
|||
* @param manager The manager responsible for the decision diagrams. |
|||
* @param reachableStates A DD representing the reachable states. |
|||
* @param initialStates A DD representing the initial states of the model. |
|||
* @param transitionMatrix The matrix representing the transitions in the model. |
|||
* @param rowVariables The set of row meta variables used in the DDs. |
|||
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row |
|||
* meta variables. |
|||
* @param columVariables The set of column meta variables used in the DDs. |
|||
* @param columnExpressionAdapter An object that can be used to translate expressions in terms of the |
|||
* column meta variables. |
|||
* @param rowColumnMetaVariablePairs All pairs of row/column meta variables. |
|||
* @param labelToExpressionMap A mapping from label names to their defining expressions. |
|||
* @param optionalStateRewardVector The reward values associated with the states. |
|||
* @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
Dtmc(std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>()); |
|||
}; |
|||
|
|||
} // namespace symbolic |
|||
} // namespace models |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_SYMBOLIC_DTMC_H_ */ |
|||
@ -0,0 +1,30 @@ |
|||
#include "src/models/symbolic/Mdp.h"
|
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
template<storm::dd::DdType Type> |
|||
Mdp<Type>::Mdp(std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::set<storm::expressions::Variable> const& nondeterminismVariables, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix) |
|||
: NondeterministicModel<Type>(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
// Explicitly instantiate the template class.
|
|||
template class Mdp<storm::dd::DdType::CUDD>; |
|||
|
|||
} // namespace symbolic
|
|||
} // namespace models
|
|||
} // namespace storm
|
|||
@ -0,0 +1,65 @@ |
|||
#ifndef STORM_MODELS_SYMBOLIC_MDP_H_ |
|||
#define STORM_MODELS_SYMBOLIC_MDP_H_ |
|||
|
|||
#include "src/models/symbolic/NondeterministicModel.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
/*! |
|||
* This class represents a discrete-time Markov decision process. |
|||
*/ |
|||
template<storm::dd::DdType Type> |
|||
class Mdp : public NondeterministicModel<Type> { |
|||
public: |
|||
Mdp(Mdp<Type> const& other) = default; |
|||
Mdp& operator=(Mdp<Type> const& other) = default; |
|||
|
|||
#ifndef WINDOWS |
|||
Mdp(Mdp<Type>&& other) = default; |
|||
Mdp& operator=(Mdp<Type>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Constructs a model from the given data. |
|||
* |
|||
* @param modelType The type of the model. |
|||
* @param manager The manager responsible for the decision diagrams. |
|||
* @param reachableStates A DD representing the reachable states. |
|||
* @param initialStates A DD representing the initial states of the model. |
|||
* @param transitionMatrix The matrix representing the transitions in the model. |
|||
* @param rowVariables The set of row meta variables used in the DDs. |
|||
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row |
|||
* meta variables. |
|||
* @param columVariables The set of column meta variables used in the DDs. |
|||
* @param columnExpressionAdapter An object that can be used to translate expressions in terms of the |
|||
* column meta variables. |
|||
* @param rowColumnMetaVariablePairs All pairs of row/column meta variables. |
|||
* @param nondeterminismVariables The meta variables used to encode the nondeterminism in the model. |
|||
* @param labelToExpressionMap A mapping from label names to their defining expressions. |
|||
* @param optionalStateRewardVector The reward values associated with the states. |
|||
* @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
Mdp(std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::set<storm::expressions::Variable> const& nondeterminismVariables, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>()); |
|||
|
|||
}; |
|||
|
|||
} // namespace symbolic |
|||
} // namespace models |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_SYMBOLIC_MDP_H_ */ |
|||
@ -0,0 +1,137 @@ |
|||
#include "src/models/symbolic/Model.h"
|
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
template<storm::dd::DdType Type> |
|||
Model<Type>::Model(storm::models::ModelType const& modelType, |
|||
std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix) |
|||
: ModelBase(modelType), manager(manager), reachableStates(reachableStates), initialStates(initialStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), columnExpressionAdapter(columnExpressionAdapter), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), stateRewardVector(optionalStateRewardVector), transitionRewardMatrix(optionalTransitionRewardMatrix) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
uint_fast64_t Model<Type>::getNumberOfStates() const { |
|||
return reachableStates.getNonZeroCount(); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
uint_fast64_t Model<Type>::getNumberOfTransitions() const { |
|||
return transitionMatrix.getNonZeroCount(); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type> const& Model<Type>::getReachableStates() const { |
|||
return reachableStates; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type> const& Model<Type>::getInitialStates() const { |
|||
return initialStates; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type> Model<Type>::getStates(std::string const& label) const { |
|||
return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type> Model<Type>::getStates(storm::expressions::Expression const& expression) const { |
|||
return rowExpressionAdapter->translateExpression(expression); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
bool Model<Type>::hasLabel(std::string const& label) const { |
|||
return labelToExpressionMap.find(label) != labelToExpressionMap.end(); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type> const& Model<Type>::getTransitionMatrix() const { |
|||
return transitionMatrix; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type>& Model<Type>::getTransitionMatrix() { |
|||
return transitionMatrix; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type> const& Model<Type>::getTransitionRewardMatrix() const { |
|||
return transitionRewardMatrix.get(); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type>& Model<Type>::getTransitionRewardMatrix() { |
|||
return transitionRewardMatrix.get(); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
storm::dd::Dd<Type> const& Model<Type>::getStateRewardVector() const { |
|||
return stateRewardVector.get(); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
bool Model<Type>::hasStateRewards() const { |
|||
return static_cast<bool>(stateRewardVector); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
bool Model<Type>::hasTransitionRewards() const { |
|||
return static_cast<bool>(transitionRewardMatrix); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
std::size_t Model<Type>::getSizeInBytes() const { |
|||
return sizeof(*this) + sizeof(DdNode) * (reachableStates.getNodeCount() + initialStates.getNodeCount() + transitionMatrix.getNodeCount()); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
std::set<storm::expressions::Variable> const& Model<Type>::getRowVariables() const { |
|||
return rowVariables; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
std::set<storm::expressions::Variable> const& Model<Type>::getColumnVariables() const { |
|||
return columnVariables; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
void Model<Type>::setTransitionMatrix(storm::dd::Dd<Type> const& transitionMatrix) { |
|||
this->transitionMatrix = transitionMatrix; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
std::map<std::string, storm::expressions::Expression> const& Model<Type>::getLabelToExpressionMap() const { |
|||
return labelToExpressionMap; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
void Model<Type>::printModelInformationToStream(std::ostream& out) const { |
|||
out << "-------------------------------------------------------------- " << std::endl; |
|||
out << "Model type: \t\t" << this->getType() << " (symbolic)" << std::endl; |
|||
out << "States: \t\t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)" << std::endl; |
|||
out << "Transitions: \t\t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)" << std::endl; |
|||
out << "Variables: \t\t" << "rows:" << this->rowVariables.size() << ", columns: " << this->columnVariables.size() << std::endl; |
|||
for (auto const& label : labelToExpressionMap) { |
|||
out << "\t" << label.first << std::endl; |
|||
} |
|||
out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl; |
|||
out << "-------------------------------------------------------------- " << std::endl; |
|||
} |
|||
|
|||
// Explicitly instantiate the template class.
|
|||
template class Model<storm::dd::DdType::CUDD>; |
|||
} // namespace symbolic
|
|||
} // namespace models
|
|||
} // namespace storm
|
|||
@ -0,0 +1,238 @@ |
|||
#ifndef STORM_MODELS_SYMBOLIC_MODEL_H_ |
|||
#define STORM_MODELS_SYMBOLIC_MODEL_H_ |
|||
|
|||
#include <memory> |
|||
#include <set> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/storage/expressions/Expression.h" |
|||
#include "src/storage/expressions/Variable.h" |
|||
#include "src/adapters/DdExpressionAdapter.h" |
|||
#include "src/storage/dd/CuddDd.h" |
|||
#include "src/storage/dd/CuddDdManager.h" |
|||
#include "src/models/ModelBase.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
/*! |
|||
* Base class for all symbolic models. |
|||
*/ |
|||
template<storm::dd::DdType Type> |
|||
class Model : public storm::models::ModelBase { |
|||
public: |
|||
Model(Model<Type> const& other) = default; |
|||
Model& operator=(Model<Type> const& other) = default; |
|||
|
|||
#ifndef WINDOWS |
|||
Model(Model<Type>&& other) = default; |
|||
Model& operator=(Model<Type>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Constructs a model from the given data. |
|||
* |
|||
* @param modelType The type of the model. |
|||
* @param manager The manager responsible for the decision diagrams. |
|||
* @param reachableStates A DD representing the reachable states. |
|||
* @param initialStates A DD representing the initial states of the model. |
|||
* @param transitionMatrix The matrix representing the transitions in the model. |
|||
* @param rowVariables The set of row meta variables used in the DDs. |
|||
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row |
|||
* meta variables. |
|||
* @param columVariables The set of column meta variables used in the DDs. |
|||
* @param columnExpressionAdapter An object that can be used to translate expressions in terms of the |
|||
* column meta variables. |
|||
* @param rowColumnMetaVariablePairs All pairs of row/column meta variables. |
|||
* @param labelToExpressionMap A mapping from label names to their defining expressions. |
|||
* @param optionalStateRewardVector The reward values associated with the states. |
|||
* @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
Model(storm::models::ModelType const& modelType, |
|||
std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>()); |
|||
|
|||
virtual uint_fast64_t getNumberOfStates() const override; |
|||
|
|||
virtual uint_fast64_t getNumberOfTransitions() const override; |
|||
|
|||
/*! |
|||
* Retrieves the reachable states of the model. |
|||
* |
|||
* @return The reachble states of the model. |
|||
*/ |
|||
storm::dd::Dd<Type> const& getReachableStates() const; |
|||
|
|||
/*! |
|||
* Retrieves the initial states of the model. |
|||
* |
|||
* @return The initial states of the model. |
|||
*/ |
|||
storm::dd::Dd<Type> const& getInitialStates() const; |
|||
|
|||
/*! |
|||
* Returns the sets of states labeled with the given label. |
|||
* |
|||
* @param label The label for which to get the labeled states. |
|||
* @return The set of states labeled with the requested label in the form of a bit vector. |
|||
*/ |
|||
storm::dd::Dd<Type> getStates(std::string const& label) const; |
|||
|
|||
/*! |
|||
* Returns the set of states labeled satisfying the given expression (that must be of boolean type). |
|||
* |
|||
* @param expression The expression that needs to hold in the states. |
|||
* @return The set of states labeled satisfying the given expression. |
|||
*/ |
|||
storm::dd::Dd<Type> getStates(storm::expressions::Expression const& expression) const; |
|||
|
|||
/*! |
|||
* Retrieves whether the given label is a valid label in this model. |
|||
* |
|||
* @param label The label to be checked for validity. |
|||
* @return True if the given label is valid in this model. |
|||
*/ |
|||
bool hasLabel(std::string const& label) const; |
|||
|
|||
/*! |
|||
* Retrieves the matrix representing the transitions of the model. |
|||
* |
|||
* @return A matrix representing the transitions of the model. |
|||
*/ |
|||
storm::dd::Dd<Type> const& getTransitionMatrix() const; |
|||
|
|||
/*! |
|||
* Retrieves the matrix representing the transitions of the model. |
|||
* |
|||
* @return A matrix representing the transitions of the model. |
|||
*/ |
|||
storm::dd::Dd<Type>& getTransitionMatrix(); |
|||
|
|||
/*! |
|||
* Retrieves the matrix representing the transition rewards of the model. Note that calling this method |
|||
* is only valid if the model has transition rewards. |
|||
* |
|||
* @return The matrix representing the transition rewards of the model. |
|||
*/ |
|||
storm::dd::Dd<Type> const& getTransitionRewardMatrix() const; |
|||
|
|||
/*! |
|||
* Retrieves the matrix representing the transition rewards of the model. Note that calling this method |
|||
* is only valid if the model has transition rewards. |
|||
* |
|||
* @return The matrix representing the transition rewards of the model. |
|||
*/ |
|||
storm::dd::Dd<Type>& getTransitionRewardMatrix(); |
|||
|
|||
/*! |
|||
* Retrieves a vector representing the state rewards of the model. Note that calling this method is only |
|||
* valid if the model has state rewards. |
|||
* |
|||
* @return A vector representing the state rewards of the model. |
|||
*/ |
|||
storm::dd::Dd<Type> const& getStateRewardVector() const; |
|||
|
|||
/*! |
|||
* Retrieves whether this model has state rewards. |
|||
* |
|||
* @return True iff this model has state rewards. |
|||
*/ |
|||
bool hasStateRewards() const; |
|||
|
|||
/*! |
|||
* Retrieves whether this model has transition rewards. |
|||
* |
|||
* @return True iff this model has transition rewards. |
|||
*/ |
|||
bool hasTransitionRewards() const; |
|||
|
|||
/*! |
|||
* Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices. |
|||
* |
|||
* @return The meta variables used to encode the rows of the transition matrix and the vector indices. |
|||
*/ |
|||
std::set<storm::expressions::Variable> const& getRowVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the meta variables used to encode the columns of the transition matrix and the vector indices. |
|||
* |
|||
* @return The meta variables used to encode the columns of the transition matrix and the vector indices. |
|||
*/ |
|||
std::set<storm::expressions::Variable> const& getColumnVariables() const; |
|||
|
|||
virtual std::size_t getSizeInBytes() const override; |
|||
|
|||
virtual void printModelInformationToStream(std::ostream& out) const override; |
|||
|
|||
protected: |
|||
|
|||
/*! |
|||
* Sets the transition matrix of the model. |
|||
* |
|||
* @param transitionMatrix The new transition matrix of the model. |
|||
*/ |
|||
void setTransitionMatrix(storm::dd::Dd<Type> const& transitionMatrix); |
|||
|
|||
/*! |
|||
* Retrieves the mapping of labels to their defining expressions. |
|||
* |
|||
* @returns The mapping of labels to their defining expressions. |
|||
*/ |
|||
std::map<std::string, storm::expressions::Expression> const& getLabelToExpressionMap() const; |
|||
|
|||
private: |
|||
// The manager responsible for the decision diagrams. |
|||
std::shared_ptr<storm::dd::DdManager<Type>> manager; |
|||
|
|||
// A vector representing the reachable states of the model. |
|||
storm::dd::Dd<Type> reachableStates; |
|||
|
|||
// A vector representing the initial states of the model. |
|||
storm::dd::Dd<Type> initialStates; |
|||
|
|||
// A matrix representing transition relation. |
|||
storm::dd::Dd<Type> transitionMatrix; |
|||
|
|||
// The meta variables used to encode the rows of the transition matrix. |
|||
std::set<storm::expressions::Variable> rowVariables; |
|||
|
|||
// An adapter that can translate expressions to DDs over the row meta variables. |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter; |
|||
|
|||
// The meta variables used to encode the columns of the transition matrix. |
|||
std::set<storm::expressions::Variable> columnVariables; |
|||
|
|||
// An adapter that can translate expressions to DDs over the column meta variables. |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter; |
|||
|
|||
// A vector holding all pairs of row and column meta variable pairs. This is used to swap the variables |
|||
// in the DDs from row to column variables and vice versa. |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs; |
|||
|
|||
// A mapping from labels to expressions defining them. |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap; |
|||
|
|||
// If set, a vector representing the rewards of the states. |
|||
boost::optional<storm::dd::Dd<Type>> stateRewardVector; |
|||
|
|||
// If set, a matrix representing the rewards of transitions. |
|||
boost::optional<storm::dd::Dd<Type>> transitionRewardMatrix; |
|||
}; |
|||
|
|||
} // namespace symbolic |
|||
} // namespace models |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_SYMBOLIC_MODEL_H_ */ |
|||
@ -0,0 +1,60 @@ |
|||
#include "src/models/symbolic/NondeterministicModel.h"
|
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
template<storm::dd::DdType Type> |
|||
NondeterministicModel<Type>::NondeterministicModel(storm::models::ModelType const& modelType, |
|||
std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::set<storm::expressions::Variable> const& nondeterminismVariables, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector, |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix) |
|||
: Model<Type>(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix), nondeterminismVariables(nondeterminismVariables) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
uint_fast64_t NondeterministicModel<Type>::getNumberOfChoices() const { |
|||
std::set<storm::expressions::Variable> rowAndNondeterminsmVariables; |
|||
std::set_union(this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), this->getRowVariables().begin(), this->getRowVariables().end(), std::inserter(rowAndNondeterminsmVariables, rowAndNondeterminsmVariables.begin())); |
|||
|
|||
storm::dd::Dd<Type> tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).sumAbstract(rowAndNondeterminsmVariables); |
|||
return static_cast<uint_fast64_t>(tmp.getValue()); |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
std::set<storm::expressions::Variable> const& NondeterministicModel<Type>::getNondeterminismVariables() const { |
|||
return nondeterminismVariables; |
|||
} |
|||
|
|||
template<storm::dd::DdType Type> |
|||
void NondeterministicModel<Type>::printModelInformationToStream(std::ostream& out) const { |
|||
out << "-------------------------------------------------------------- " << std::endl; |
|||
out << "Model type: \t\t" << this->getType() << " (symbolic)" << std::endl; |
|||
out << "States: \t\t" << this->getNumberOfStates() << " (" << this->getReachableStates().getNodeCount() << " nodes)" << std::endl; |
|||
out << "Transitions: \t\t" << this->getNumberOfTransitions() << " (" << this->getTransitionMatrix().getNodeCount() << " nodes)" << std::endl; |
|||
out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl; |
|||
out << "Variables: \t\t" << "rows:" << this->getRowVariables().size() << ", columns: " << this->getColumnVariables().size() << ", nondeterminism: " << this->getNondeterminismVariables().size() << std::endl; |
|||
for (auto const& label : this->getLabelToExpressionMap()) { |
|||
out << "\t" << label.first << std::endl; |
|||
} |
|||
out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl; |
|||
out << "-------------------------------------------------------------- " << std::endl; |
|||
} |
|||
|
|||
// Explicitly instantiate the template class.
|
|||
template class NondeterministicModel<storm::dd::DdType::CUDD>; |
|||
|
|||
} // namespace symbolic
|
|||
} // namespace models
|
|||
} // namespace storm
|
|||
@ -0,0 +1,86 @@ |
|||
#ifndef STORM_MODELS_SYMBOLIC_NONDETERMINISTICMODEL_H_ |
|||
#define STORM_MODELS_SYMBOLIC_NONDETERMINISTICMODEL_H_ |
|||
|
|||
#include "src/models/symbolic/Model.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace symbolic { |
|||
|
|||
/*! |
|||
* Base class for all nondeterministic symbolic models. |
|||
*/ |
|||
template<storm::dd::DdType Type> |
|||
class NondeterministicModel : public Model<Type> { |
|||
public: |
|||
NondeterministicModel(NondeterministicModel<Type> const& other) = default; |
|||
NondeterministicModel& operator=(NondeterministicModel<Type> const& other) = default; |
|||
|
|||
#ifndef WINDOWS |
|||
NondeterministicModel(NondeterministicModel<Type>&& other) = default; |
|||
NondeterministicModel& operator=(NondeterministicModel<Type>&& other) = default; |
|||
#endif |
|||
|
|||
/*! |
|||
* Constructs a model from the given data. |
|||
* |
|||
* @param modelType The type of the model. |
|||
* @param manager The manager responsible for the decision diagrams. |
|||
* @param reachableStates A DD representing the reachable states. |
|||
* @param initialStates A DD representing the initial states of the model. |
|||
* @param transitionMatrix The matrix representing the transitions in the model. |
|||
* @param rowVariables The set of row meta variables used in the DDs. |
|||
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row |
|||
* meta variables. |
|||
* @param columVariables The set of column meta variables used in the DDs. |
|||
* @param columnExpressionAdapter An object that can be used to translate expressions in terms of the |
|||
* column meta variables. |
|||
* @param rowColumnMetaVariablePairs All pairs of row/column meta variables. |
|||
* @param nondeterminismVariables The meta variables used to encode the nondeterminism in the model. |
|||
* @param labelToExpressionMap A mapping from label names to their defining expressions. |
|||
* @param optionalStateRewardVector The reward values associated with the states |
|||
* @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
NondeterministicModel(storm::models::ModelType const& modelType, |
|||
std::shared_ptr<storm::dd::DdManager<Type>> manager, |
|||
storm::dd::Dd<Type> reachableStates, |
|||
storm::dd::Dd<Type> initialStates, |
|||
storm::dd::Dd<Type> transitionMatrix, |
|||
std::set<storm::expressions::Variable> const& rowVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> rowExpressionAdapter, |
|||
std::set<storm::expressions::Variable> const& columnVariables, |
|||
std::shared_ptr<storm::adapters::DdExpressionAdapter<Type>> columnExpressionAdapter, |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, |
|||
std::set<storm::expressions::Variable> const& nondeterminismVariables, |
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(), |
|||
boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>()); |
|||
|
|||
/*! |
|||
* Retrieves the number of nondeterministic choices in the model. |
|||
* |
|||
* @return The number of nondeterministic choices in the model. |
|||
*/ |
|||
uint_fast64_t getNumberOfChoices() const; |
|||
|
|||
/*! |
|||
* Retrieves the meta variables used to encode the nondeterminism in the model. |
|||
* |
|||
* @return The meta variables used to encode the nondeterminism in the model. |
|||
*/ |
|||
std::set<storm::expressions::Variable> const& getNondeterminismVariables() const; |
|||
|
|||
virtual void printModelInformationToStream(std::ostream& out) const override; |
|||
|
|||
private: |
|||
|
|||
// The meta variables encoding the nondeterminism in the model. |
|||
std::set<storm::expressions::Variable> nondeterminismVariables; |
|||
}; |
|||
|
|||
} // namespace symbolic |
|||
} // namespace models |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_SYMBOLIC_NONDETERMINISTICMODEL_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue