diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index a831a8528..995bc296e 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -63,7 +63,7 @@ public: std::shared_ptr> toSparseMatrix() { LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program."); - this->computeReachableStateSpace2(); + this->buildMatrix2(); this->computeReachableStateSpace(); std::shared_ptr> resultMatrix = this->buildMatrix(); @@ -254,19 +254,94 @@ private: } } - void computeReachableStateSpace2() { + /*! + * Create matrix from intermediate mapping, assuming it is a dtmc model. + * @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())); + result->initialize(numberOfTransitions); + for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { + //if (intermediate[state].size() > 1) WARNING; + double factor = 1.0 / intermediate[state].size(); + std::map map; + for (auto choice : intermediate[state]) { + for (auto elem : choice) { + map[elem.first] += elem.second * factor; + } + } + for (auto it : map) { + result->addNextValue(state, it.first, it.second); + } + + } + result->finalize(); + return result; + } + + /*! + * Create matrix from intermediate mapping, assuming it is a mdp model. + * @param intermediate Intermediate representation of transition mapping. + * @return result matrix. + */ + template + std::shared_ptr> buildMDPMatrix(std::map>> intermediate, uint_fast64_t choices) { + std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size(), choices)); + result->initialize(numberOfTransitions); + uint_fast64_t nextRow = 0; + for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { + for (auto choice : intermediate[state]) { + for (auto it : choice) { + result->addNextValue(nextRow, it.first, it.second); + } + nextRow++; + } + } + result->finalize(); + return result; + } + + template + std::shared_ptr> buildMatrix2() { this->prepareAuxiliaryDatastructures(); this->allStates.clear(); this->stateToIndexMap.clear(); + uint_fast64_t choices; + std::map>> intermediate; for (uint_fast64_t curIndex = this->getOrAddStateId(this->buildInitialState()); curIndex < this->allStates.size(); curIndex++) { - std::list> choices; - this->addUnlabeledTransitions(this->allStates[curIndex], choices); - std::cout << "Output:" << std::endl; - for (auto it: choices) this->dump(it); + this->addUnlabeledTransitions(this->allStates[curIndex], intermediate[curIndex]); + + choices += intermediate[curIndex].size(); + if (intermediate[curIndex].size() == 0) { + // This is a deadlock state. + if (storm::settings::instance()->isSet("fix-deadlocks")) { + this->numberOfTransitions++; + intermediate[curIndex].emplace_back(); + intermediate[curIndex].back()[curIndex] = 1; + } else { + LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state."); + throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state."; + } + } + } + + switch (this->program->getModelType()) { + case storm::ir::Program::DTMC: + case storm::ir::Program::CTMC: + return this->buildDTMCMatrix(intermediate); + case storm::ir::Program::MDP: + case storm::ir::Program::CTMDP: + 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; } - std::cout << "got " << this->allStates.size() << " states" << std::endl; + return std::shared_ptr>(nullptr); } void computeReachableStateSpace() {