From 239caf57eb8cc7f08baa018223e2b8354516fc0b Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 24 Feb 2015 15:50:11 +0100 Subject: [PATCH] Added symbolic models and made DD-based model generator build the correct instances. Former-commit-id: c054401cfd2c724ba3f9e9392ef00eb4281e81d2 --- CMakeLists.txt | 3 +- src/builder/DdPrismModelBuilder.cpp | 34 +-- src/builder/DdPrismModelBuilder.h | 15 +- src/builder/ExplicitPrismModelBuilder.cpp | 10 +- src/builder/ExplicitPrismModelBuilder.h | 2 +- src/models/ModelBase.h | 7 + src/models/sparse/Model.cpp | 2 +- src/models/sparse/Model.h | 1 + src/models/sparse/NondeterministicModel.cpp | 2 +- src/models/symbolic/DeterministicModel.cpp | 30 +++ src/models/symbolic/DeterministicModel.h | 63 +++++ src/models/symbolic/Dtmc.cpp | 29 +++ src/models/symbolic/Dtmc.h | 61 +++++ src/models/symbolic/Mdp.cpp | 30 +++ src/models/symbolic/Mdp.h | 65 +++++ src/models/symbolic/Model.cpp | 137 ++++++++++ src/models/symbolic/Model.h | 238 ++++++++++++++++++ src/models/symbolic/NondeterministicModel.cpp | 60 +++++ src/models/symbolic/NondeterministicModel.h | 86 +++++++ .../builder/DdPrismModelBuilderTest.cpp | 82 ++++-- 20 files changed, 900 insertions(+), 57 deletions(-) create mode 100644 src/models/symbolic/DeterministicModel.cpp create mode 100644 src/models/symbolic/DeterministicModel.h create mode 100644 src/models/symbolic/Dtmc.cpp create mode 100644 src/models/symbolic/Dtmc.h create mode 100644 src/models/symbolic/Mdp.cpp create mode 100644 src/models/symbolic/Mdp.h create mode 100644 src/models/symbolic/Model.cpp create mode 100644 src/models/symbolic/Model.h create mode 100644 src/models/symbolic/NondeterministicModel.cpp create mode 100644 src/models/symbolic/NondeterministicModel.h diff --git a/CMakeLists.txt b/CMakeLists.txt index a11f9d1fc..70bfb736c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -269,6 +269,7 @@ file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/mod file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) file(GLOB STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) file(GLOB_RECURSE STORM_MODELS_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/models/sparse/*.h ${PROJECT_SOURCE_DIR}/src/models/sparse/*.cpp) +file(GLOB_RECURSE STORM_MODELS_SYMBOLIC_FILES ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.h ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.cpp) file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) @@ -290,7 +291,6 @@ file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/perf # Additional include files like the storm-config.h file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) - # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) @@ -307,6 +307,7 @@ source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES}) source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(models\\sparse FILES ${STORM_MODELS_SPARSE_FILES}) +source_group(models\\symbolic FILES ${STORM_MODELS_SYMBOLIC_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 592df613d..be779489e 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1,5 +1,8 @@ #include "src/builder/DdPrismModelBuilder.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/Mdp.h" + #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/settings/SettingsManager.h" @@ -574,7 +577,7 @@ namespace storm { } template - std::pair, storm::dd::Dd> DdPrismModelBuilder::translateProgram(storm::prism::Program const& program, Options const& options) { + std::shared_ptr> DdPrismModelBuilder::translateProgram(storm::prism::Program const& program, Options const& options) { // There might be nondeterministic variables. In that case the program must be prepared before translating. storm::prism::Program preparedProgram; if (options.constantDefinitions) { @@ -600,13 +603,11 @@ namespace storm { } preparedProgram = preparedProgram.substituteConstants(); -// std::cout << "translated prog: " << preparedProgram << std::endl; // Start by initializing the structure used for storing all information needed during the model generation. // In particular, this creates the meta variables used to encode the model. GenerationInformation generationInfo(preparedProgram); - auto totalTimeStart = std::chrono::high_resolution_clock::now(); std::pair, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); storm::dd::Dd transitionMatrix = transitionMatrixModulePair.first; ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second; @@ -632,19 +633,10 @@ namespace storm { stateAndTransitionRewards = createRewardDecisionDiagrams(generationInfo, rewardModel, globalModule, transitionMatrix); } - auto totalTimeEnd = std::chrono::high_resolution_clock::now(); - std::cout << "building matrices and vectors took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; - // Cut the transition matrix to the reachable fragment of the state space. - totalTimeStart = std::chrono::high_resolution_clock::now(); - storm::dd::Dd reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix); - totalTimeEnd = std::chrono::high_resolution_clock::now(); - std::cout << "reachability took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; - - totalTimeStart = std::chrono::high_resolution_clock::now(); + storm::dd::Dd initialStates = createInitialStatesDecisionDiagram(generationInfo); + storm::dd::Dd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrix); transitionMatrix *= reachableStates.toMtbdd(); - totalTimeEnd = std::chrono::high_resolution_clock::now(); - std::cout << "cutting trans to reachable took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Dd statesWithTransition = transitionMatrix.notZero(); @@ -674,9 +666,19 @@ namespace storm { } } - std::cout << reachableStates.getNonZeroCount() << " states and " << transitionMatrix.getNonZeroCount() << " transitions." << std::endl; + // Build the labels that can be accessed as a shortcut. + std::map labelToExpressionMapping; + for (auto const& label : program.getLabels()) { + labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression()); + } - return std::make_pair(reachableStates, transitionMatrix); + if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { + return std::unique_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional>())); + } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { + return std::unique_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional>())); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); + } } template diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index e621cf5ca..d9619710f 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -4,6 +4,7 @@ #include #include +#include "src/models/symbolic/Model.h" #include "src/logic/Formulas.h" #include "src/storage/prism/Program.h" #include "src/adapters/DdExpressionAdapter.h" @@ -55,11 +56,13 @@ namespace storm { }; /*! - * Translates the given program into a model that stores the transition relation as a decision diagram. + * Translates the given program into a symbolic model (i.e. one that stores the transition relation as a + * decision diagram). * * @param program The program to translate. + * @return A pointer to the resulting model. */ - static std::pair, storm::dd::Dd> translateProgram(storm::prism::Program const& program, Options const& options = Options()); + static std::shared_ptr> translateProgram(storm::prism::Program const& program, Options const& options = Options()); private: // This structure can store the decision diagrams representing a particular action. @@ -132,8 +135,8 @@ namespace storm { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); - rowExpressionAdapter = std::unique_ptr>(new storm::adapters::DdExpressionAdapter(*manager, variableToRowMetaVariableMap)); - columnExpressionAdapter = std::unique_ptr>(new storm::adapters::DdExpressionAdapter(*manager, variableToColumnMetaVariableMap)); + rowExpressionAdapter = std::shared_ptr>(new storm::adapters::DdExpressionAdapter(*manager, variableToRowMetaVariableMap)); + columnExpressionAdapter = std::shared_ptr>(new storm::adapters::DdExpressionAdapter(*manager, variableToColumnMetaVariableMap)); } // The program that is currently translated. @@ -145,12 +148,12 @@ namespace storm { // The meta variables for the row encoding. std::set rowMetaVariables; std::map variableToRowMetaVariableMap; - std::unique_ptr> rowExpressionAdapter; + std::shared_ptr> rowExpressionAdapter; // The meta variables for the column encoding. std::set columnMetaVariables; std::map variableToColumnMetaVariableMap; - std::unique_ptr> columnExpressionAdapter; + std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 43a8ea6fd..8ba671a94 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -91,7 +91,7 @@ namespace storm { } template - std::unique_ptr> ExplicitPrismModelBuilder::translateProgram(storm::prism::Program program, Options const& options) { + std::shared_ptr> ExplicitPrismModelBuilder::translateProgram(storm::prism::Program program, Options const& options) { // Start by defining the undefined constants in the model. storm::prism::Program preparedProgram; if (options.constantDefinitions) { @@ -166,16 +166,16 @@ namespace storm { ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options); - std::unique_ptr> result; + std::shared_ptr> result; switch (program.getModelType()) { case storm::prism::Program::ModelType::DTMC: - result = std::unique_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::CTMC: - result = std::unique_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::MDP: - result = std::unique_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model from probabilistic program: cannot handle this model type."); diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index b70524569..c88932eb5 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -172,7 +172,7 @@ namespace storm { * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ - static std::unique_ptr> translateProgram(storm::prism::Program program, Options const& options = Options()); + static std::shared_ptr> translateProgram(storm::prism::Program program, Options const& options = Options()); private: static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); diff --git a/src/models/ModelBase.h b/src/models/ModelBase.h index cc8b31ccf..c72a2c8df 100644 --- a/src/models/ModelBase.h +++ b/src/models/ModelBase.h @@ -69,6 +69,13 @@ namespace storm { */ virtual std::size_t getSizeInBytes() const = 0; + /*! + * Prints information about the model to the specified stream. + * + * @param out The stream the information is to be printed to. + */ + virtual void printModelInformationToStream(std::ostream& out) const = 0; + private: // The type of the model. ModelType modelType; diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 5dd29c3b6..62b3e68ce 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -199,7 +199,7 @@ namespace storm { template void Model::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; - out << "Model type: \t\t" << this->getType() << std::endl; + out << "Model type: \t\t" << this->getType() << " (sparse)" << std::endl; out << "States: \t\t" << this->getNumberOfStates() << std::endl; out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; this->getStateLabeling().printLabelingInformationToStream(out); diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 3c8f56fd2..55658935d 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -73,6 +73,7 @@ namespace storm { */ template storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const; + /*! * Retrieves the backward transition relation of the model, i.e. a set of transitions between states * that correspond to the reversed transition relation of this model. diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index e1db2d19f..01868ea17 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -42,7 +42,7 @@ namespace storm { template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; - out << "Model type: \t\t" << this->getType() << std::endl; + out << "Model type: \t\t" << this->getType() << " (sparse)" << std::endl; out << "States: \t\t" << this->getNumberOfStates() << std::endl; out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl; diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp new file mode 100644 index 000000000..64aca24ab --- /dev/null +++ b/src/models/symbolic/DeterministicModel.cpp @@ -0,0 +1,30 @@ +#include "src/models/symbolic/DeterministicModel.h" + +namespace storm { + namespace models { + namespace symbolic { + + template + DeterministicModel::DeterministicModel(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::map labelToExpressionMap, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { + // Intentionally left empty. + } + + // Explicitly instantiate the template class. + template class DeterministicModel; + + } // namespace symbolic + } // namespace models +} // namespace storm \ No newline at end of file diff --git a/src/models/symbolic/DeterministicModel.h b/src/models/symbolic/DeterministicModel.h new file mode 100644 index 000000000..274d2818a --- /dev/null +++ b/src/models/symbolic/DeterministicModel.h @@ -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 + class DeterministicModel : public Model { + public: + DeterministicModel(DeterministicModel const& other) = default; + DeterministicModel& operator=(DeterministicModel const& other) = default; + +#ifndef WINDOWS + DeterministicModel(DeterministicModel&& other) = default; + DeterministicModel& operator=(DeterministicModel&& 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> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::map labelToExpressionMap = std::map(), + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + }; + + } // namespace symbolic + } // namespace models +} // namespace storm + +#endif /* STORM_MODELS_SYMBOLIC_DETERMINISTICMODEL_H_ */ diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp new file mode 100644 index 000000000..5c28f063f --- /dev/null +++ b/src/models/symbolic/Dtmc.cpp @@ -0,0 +1,29 @@ +#include "src/models/symbolic/Dtmc.h" + +namespace storm { + namespace models { + namespace symbolic { + + template + Dtmc::Dtmc(std::shared_ptr> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::map labelToExpressionMap, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : DeterministicModel(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; + + } // namespace symbolic + } // namespace models +} // namespace storm \ No newline at end of file diff --git a/src/models/symbolic/Dtmc.h b/src/models/symbolic/Dtmc.h new file mode 100644 index 000000000..b9c12e86e --- /dev/null +++ b/src/models/symbolic/Dtmc.h @@ -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 + class Dtmc : public DeterministicModel { + public: + Dtmc(Dtmc const& other) = default; + Dtmc& operator=(Dtmc const& other) = default; + +#ifndef WINDOWS + Dtmc(Dtmc&& other) = default; + Dtmc& operator=(Dtmc&& 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> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::map labelToExpressionMap = std::map(), + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + }; + + } // namespace symbolic + } // namespace models +} // namespace storm + +#endif /* STORM_MODELS_SYMBOLIC_DTMC_H_ */ diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp new file mode 100644 index 000000000..36462c072 --- /dev/null +++ b/src/models/symbolic/Mdp.cpp @@ -0,0 +1,30 @@ +#include "src/models/symbolic/Mdp.h" + +namespace storm { + namespace models { + namespace symbolic { + + template + Mdp::Mdp(std::shared_ptr> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map labelToExpressionMap, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : NondeterministicModel(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; + + } // namespace symbolic + } // namespace models +} // namespace storm \ No newline at end of file diff --git a/src/models/symbolic/Mdp.h b/src/models/symbolic/Mdp.h new file mode 100644 index 000000000..587bdfac7 --- /dev/null +++ b/src/models/symbolic/Mdp.h @@ -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 + class Mdp : public NondeterministicModel { + public: + Mdp(Mdp const& other) = default; + Mdp& operator=(Mdp const& other) = default; + +#ifndef WINDOWS + Mdp(Mdp&& other) = default; + Mdp& operator=(Mdp&& 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> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map labelToExpressionMap = std::map(), + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + + }; + + } // namespace symbolic + } // namespace models +} // namespace storm + +#endif /* STORM_MODELS_SYMBOLIC_MDP_H_ */ diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp new file mode 100644 index 000000000..1af5c2b6a --- /dev/null +++ b/src/models/symbolic/Model.cpp @@ -0,0 +1,137 @@ +#include "src/models/symbolic/Model.h" + +namespace storm { + namespace models { + namespace symbolic { + template + Model::Model(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::map labelToExpressionMap, + boost::optional> const& optionalStateRewardVector, + boost::optional> 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 + uint_fast64_t Model::getNumberOfStates() const { + return reachableStates.getNonZeroCount(); + } + + template + uint_fast64_t Model::getNumberOfTransitions() const { + return transitionMatrix.getNonZeroCount(); + } + + template + storm::dd::Dd const& Model::getReachableStates() const { + return reachableStates; + } + + template + storm::dd::Dd const& Model::getInitialStates() const { + return initialStates; + } + + template + storm::dd::Dd Model::getStates(std::string const& label) const { + return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)); + } + + template + storm::dd::Dd Model::getStates(storm::expressions::Expression const& expression) const { + return rowExpressionAdapter->translateExpression(expression); + } + + template + bool Model::hasLabel(std::string const& label) const { + return labelToExpressionMap.find(label) != labelToExpressionMap.end(); + } + + template + storm::dd::Dd const& Model::getTransitionMatrix() const { + return transitionMatrix; + } + + template + storm::dd::Dd& Model::getTransitionMatrix() { + return transitionMatrix; + } + + template + storm::dd::Dd const& Model::getTransitionRewardMatrix() const { + return transitionRewardMatrix.get(); + } + + template + storm::dd::Dd& Model::getTransitionRewardMatrix() { + return transitionRewardMatrix.get(); + } + + template + storm::dd::Dd const& Model::getStateRewardVector() const { + return stateRewardVector.get(); + } + + template + bool Model::hasStateRewards() const { + return static_cast(stateRewardVector); + } + + template + bool Model::hasTransitionRewards() const { + return static_cast(transitionRewardMatrix); + } + + template + std::size_t Model::getSizeInBytes() const { + return sizeof(*this) + sizeof(DdNode) * (reachableStates.getNodeCount() + initialStates.getNodeCount() + transitionMatrix.getNodeCount()); + } + + template + std::set const& Model::getRowVariables() const { + return rowVariables; + } + + template + std::set const& Model::getColumnVariables() const { + return columnVariables; + } + + template + void Model::setTransitionMatrix(storm::dd::Dd const& transitionMatrix) { + this->transitionMatrix = transitionMatrix; + } + + template + std::map const& Model::getLabelToExpressionMap() const { + return labelToExpressionMap; + } + + template + void Model::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; + } // namespace symbolic + } // namespace models +} // namespace storm \ No newline at end of file diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h new file mode 100644 index 000000000..0f8a91c64 --- /dev/null +++ b/src/models/symbolic/Model.h @@ -0,0 +1,238 @@ +#ifndef STORM_MODELS_SYMBOLIC_MODEL_H_ +#define STORM_MODELS_SYMBOLIC_MODEL_H_ + +#include +#include +#include + +#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 + class Model : public storm::models::ModelBase { + public: + Model(Model const& other) = default; + Model& operator=(Model const& other) = default; + +#ifndef WINDOWS + Model(Model&& other) = default; + Model& operator=(Model&& 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> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::map labelToExpressionMap = std::map(), + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + + 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 const& getReachableStates() const; + + /*! + * Retrieves the initial states of the model. + * + * @return The initial states of the model. + */ + storm::dd::Dd 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 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 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 const& getTransitionMatrix() const; + + /*! + * Retrieves the matrix representing the transitions of the model. + * + * @return A matrix representing the transitions of the model. + */ + storm::dd::Dd& 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 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& 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 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 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 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 const& transitionMatrix); + + /*! + * Retrieves the mapping of labels to their defining expressions. + * + * @returns The mapping of labels to their defining expressions. + */ + std::map const& getLabelToExpressionMap() const; + + private: + // The manager responsible for the decision diagrams. + std::shared_ptr> manager; + + // A vector representing the reachable states of the model. + storm::dd::Dd reachableStates; + + // A vector representing the initial states of the model. + storm::dd::Dd initialStates; + + // A matrix representing transition relation. + storm::dd::Dd transitionMatrix; + + // The meta variables used to encode the rows of the transition matrix. + std::set rowVariables; + + // An adapter that can translate expressions to DDs over the row meta variables. + std::shared_ptr> rowExpressionAdapter; + + // The meta variables used to encode the columns of the transition matrix. + std::set columnVariables; + + // An adapter that can translate expressions to DDs over the column meta variables. + std::shared_ptr> 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> rowColumnMetaVariablePairs; + + // A mapping from labels to expressions defining them. + std::map labelToExpressionMap; + + // If set, a vector representing the rewards of the states. + boost::optional> stateRewardVector; + + // If set, a matrix representing the rewards of transitions. + boost::optional> transitionRewardMatrix; + }; + + } // namespace symbolic + } // namespace models +} // namespace storm + +#endif /* STORM_MODELS_SYMBOLIC_MODEL_H_ */ diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp new file mode 100644 index 000000000..ad2db49d9 --- /dev/null +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -0,0 +1,60 @@ +#include "src/models/symbolic/NondeterministicModel.h" + +namespace storm { + namespace models { + namespace symbolic { + + template + NondeterministicModel::NondeterministicModel(storm::models::ModelType const& modelType, + std::shared_ptr> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map labelToExpressionMap, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix), nondeterminismVariables(nondeterminismVariables) { + // Intentionally left empty. + } + + template + uint_fast64_t NondeterministicModel::getNumberOfChoices() const { + std::set rowAndNondeterminsmVariables; + std::set_union(this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), this->getRowVariables().begin(), this->getRowVariables().end(), std::inserter(rowAndNondeterminsmVariables, rowAndNondeterminsmVariables.begin())); + + storm::dd::Dd tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).sumAbstract(rowAndNondeterminsmVariables); + return static_cast(tmp.getValue()); + } + + template + std::set const& NondeterministicModel::getNondeterminismVariables() const { + return nondeterminismVariables; + } + + template + void NondeterministicModel::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; + + } // namespace symbolic + } // namespace models +} // namespace storm \ No newline at end of file diff --git a/src/models/symbolic/NondeterministicModel.h b/src/models/symbolic/NondeterministicModel.h new file mode 100644 index 000000000..7b0470ead --- /dev/null +++ b/src/models/symbolic/NondeterministicModel.h @@ -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 + class NondeterministicModel : public Model { + public: + NondeterministicModel(NondeterministicModel const& other) = default; + NondeterministicModel& operator=(NondeterministicModel const& other) = default; + +#ifndef WINDOWS + NondeterministicModel(NondeterministicModel&& other) = default; + NondeterministicModel& operator=(NondeterministicModel&& 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> manager, + storm::dd::Dd reachableStates, + storm::dd::Dd initialStates, + storm::dd::Dd transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& nondeterminismVariables, + std::map labelToExpressionMap = std::map(), + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + + /*! + * 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 const& getNondeterminismVariables() const; + + virtual void printModelInformationToStream(std::ostream& out) const override; + + private: + + // The meta variables encoding the nondeterminism in the model. + std::set nondeterminismVariables; + }; + + } // namespace symbolic + } // namespace models +} // namespace storm + +#endif /* STORM_MODELS_SYMBOLIC_NONDETERMINISTICMODEL_H_ */ diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index 67ae4d1ac..20dfb8361 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -1,8 +1,8 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include - +#include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/Mdp.h" #include "src/storage/dd/CuddDd.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" @@ -10,59 +10,89 @@ TEST(DdPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - std::pair, storm::dd::Dd> model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(13, model.first.getNonZeroCount()); - EXPECT_EQ(20, model.second.getNonZeroCount()); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(13, model->getNumberOfStates()); + EXPECT_EQ(20, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(677, model.first.getNonZeroCount()); - EXPECT_EQ(867, model.second.getNonZeroCount()); + EXPECT_EQ(677, model->getNumberOfStates()); + EXPECT_EQ(867, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(8607, model.first.getNonZeroCount()); - EXPECT_EQ(15113, model.second.getNonZeroCount()); + EXPECT_EQ(8607, model->getNumberOfStates()); + EXPECT_EQ(15113, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(273, model.first.getNonZeroCount()); - EXPECT_EQ(397, model.second.getNonZeroCount()); + EXPECT_EQ(273, model->getNumberOfStates()); + EXPECT_EQ(397, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(1728, model.first.getNonZeroCount()); - EXPECT_EQ(2505, model.second.getNonZeroCount()); + EXPECT_EQ(1728, model->getNumberOfStates()); + EXPECT_EQ(2505, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - std::pair, storm::dd::Dd> model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(169, model.first.getNonZeroCount()); - EXPECT_EQ(436, model.second.getNonZeroCount()); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(169, mdp->getNumberOfStates()); + EXPECT_EQ(436, mdp->getNumberOfTransitions()); + EXPECT_EQ(254, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(364, model.first.getNonZeroCount()); - EXPECT_EQ(654, model.second.getNonZeroCount()); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + EXPECT_EQ(364, mdp->getNumberOfStates()); + EXPECT_EQ(654, mdp->getNumberOfTransitions()); + EXPECT_EQ(573, mdp->getNumberOfChoices()); + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(272, model.first.getNonZeroCount()); - EXPECT_EQ(492, model.second.getNonZeroCount()); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(272, mdp->getNumberOfStates()); + EXPECT_EQ(492, mdp->getNumberOfTransitions()); + EXPECT_EQ(400, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(1038, model.first.getNonZeroCount()); - EXPECT_EQ(1282, model.second.getNonZeroCount()); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(1038, mdp->getNumberOfStates()); + EXPECT_EQ(1282, mdp->getNumberOfTransitions()); + EXPECT_EQ(1054, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(4093, model.first.getNonZeroCount()); - EXPECT_EQ(5585, model.second.getNonZeroCount()); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(4093, mdp->getNumberOfStates()); + EXPECT_EQ(5585, mdp->getNumberOfTransitions()); + EXPECT_EQ(5519, mdp->getNumberOfChoices()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); - EXPECT_EQ(37, model.first.getNonZeroCount()); - EXPECT_EQ(59, model.second.getNonZeroCount()); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(37, mdp->getNumberOfStates()); + EXPECT_EQ(59, mdp->getNumberOfTransitions()); + EXPECT_EQ(59, mdp->getNumberOfChoices()); } \ No newline at end of file