diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 4a5cec58c..8b8e5dee3 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -11,6 +11,15 @@ #include "src/storage/SparseMatrix.h" #include "src/utility/Settings.h" +#include "src/ir/RewardModel.h" +#include "src/ir/StateReward.h" +#include "src/ir/TransitionReward.h" + +#include "src/models/AbstractModel.h" +#include "src/models/Dtmc.h" +#include "src/models/Ctmc.h" +#include "src/models/Mdp.h" + #include #include #include @@ -25,6 +34,7 @@ typedef std::pair, std::vector> StateType; #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" +#include "ir/Program.h" extern log4cplus::Logger logger; namespace storm { @@ -60,11 +70,51 @@ public: } - template - std::shared_ptr> toSparseMatrix() { + std::shared_ptr toModel(std::string const & rewardModelName = "") { + + std::shared_ptr> matrix = this->toSparseMatrix(); + + std::shared_ptr stateLabeling = this->getStateLabeling(this->program->getLabels()); + std::shared_ptr> stateRewards = nullptr; + std::shared_ptr> transitionRewardMatrix = nullptr; + + if (rewardModelName != "") { + storm::ir::RewardModel rewardModel = this->program->getRewardModel(rewardModelName); + stateRewards = this->getStateRewards(rewardModel.getStateRewards()); + } + + switch (this->program->getModelType()) + { +/* std::shared_ptr> probabilityMatrix, + std::shared_ptr stateLabeling, + std::shared_ptr> stateRewards = nullptr, + std::shared_ptr> transitionRewardMatrix = nullptr +*/ + case storm::ir::Program::DTMC: + return std::shared_ptr(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); + break; + case storm::ir::Program::CTMC: + return std::shared_ptr(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); + break; + case storm::ir::Program::MDP: + return std::shared_ptr(new storm::models::Mdp(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); + break; + case storm::ir::Program::CTMDP: + // Todo + //return std::shared_ptr(new storm::models::Ctmdp(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); + break; + default: + // ERROR + break; + } + + return std::shared_ptr(nullptr); + } + + std::shared_ptr> toSparseMatrix() { LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program."); - std::shared_ptr> resultMatrix = this->buildMatrix(); + std::shared_ptr> resultMatrix = this->buildMatrix(); LOG4CPLUS_INFO(logger, "Created sparse matrix with " << resultMatrix->getRowCount() << " reachable states and " << resultMatrix->getNonZeroEntryCount() << " transitions."); @@ -81,6 +131,31 @@ private: static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) { std::get<1>(*state)[index] = value; } + + std::shared_ptr> getStateRewards(std::vector const & rewards) { + std::shared_ptr> results(new std::vector(this->allStates.size())); + for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { + for (auto reward: rewards) { + (*results)[index] = reward.getReward(this->allStates[index]); + } + } + return results; + } + + std::shared_ptr getStateLabeling(std::map> labels) { + std::shared_ptr results(new storm::models::AtomicPropositionsLabeling(this->allStates.size(), labels.size())); + for (auto it: labels) { + results->addAtomicProposition(it.first); + } + for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { + for (auto label: labels) { + if (label.second->getValueAsBool(this->allStates[index])) { + results->addAtomicPropositionToState(label.first, index); + } + } + } + return results; + } /*! * Initializes all internal variables. @@ -362,9 +437,8 @@ private: * @param intermediate Intermediate representation of transition mapping. * @return result matrix. */ - template - std::shared_ptr> buildDTMCMatrix(std::map>> intermediate) { - std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size())); + std::shared_ptr> buildDTMCMatrix(std::map>> intermediate) { + std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size())); // this->numberOfTransitions is meaningless, as we combine all choices into one for each state. // Hence, we compute the correct number of transitions now. uint_fast64_t numberOfTransitions = 0; @@ -409,10 +483,9 @@ private: * @param choices Overall number of choices for all nodes. * @return result matrix. */ - template - std::shared_ptr> buildMDPMatrix(std::map>> intermediate, uint_fast64_t choices) { + std::shared_ptr> buildMDPMatrix(std::map>> intermediate, uint_fast64_t choices) { std::cout << "Building MDP matrix with " << this->numberOfTransitions << " transitions." << std::endl; - std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size(), choices)); + std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size(), choices)); // Build matrix. result->initialize(this->numberOfTransitions); uint_fast64_t nextRow = 0; @@ -434,8 +507,7 @@ private: * Afterwards, we transform this map into the actual matrix. * @return result matrix. */ - template - std::shared_ptr> buildMatrix() { + std::shared_ptr> buildMatrix() { this->prepareAuxiliaryDatastructures(); this->allStates.clear(); this->stateToIndexMap.clear(); @@ -467,16 +539,16 @@ private: switch (this->program->getModelType()) { case storm::ir::Program::DTMC: case storm::ir::Program::CTMC: - return this->buildDTMCMatrix(intermediate); + return this->buildDTMCMatrix(intermediate); case storm::ir::Program::MDP: case storm::ir::Program::CTMDP: - return this->buildMDPMatrix(intermediate, choices); + return this->buildMDPMatrix(intermediate, choices); default: LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: We can't handle this model type."); throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: We can't handle this model type."; break; } - return std::shared_ptr>(nullptr); + return std::shared_ptr>(nullptr); } /*!