diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index a0595e7be..93d8a60f2 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -54,7 +54,6 @@ namespace storm { STORM_LOG_THROW(!sawType, storm::exceptions::WrongFormatException, "Type declared twice"); type = storm::models::getModelType(line.substr(7)); STORM_LOG_TRACE("Model type: " << type); - STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)"); STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported."); sawType = true; @@ -107,15 +106,21 @@ namespace storm { // Initialize auto modelComponents = std::make_shared>(); bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton); + bool continousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton); storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, nonDeterministic, 0); modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); std::vector> stateRewards; - + if (continousTime) { + modelComponents->exitRates = std::vector(stateSize); + if (type == storm::models::ModelType::MarkovAutomaton) { + modelComponents->markovianStates = storm::storage::BitVector(stateSize); + } + } // We parse rates for continuous time models. if (type == storm::models::ModelType::Ctmc) { modelComponents->rateTransitions = true; } - + // Iterate over all lines std::string line; size_t row = 0; @@ -131,34 +136,66 @@ namespace storm { } else { ++state; } - line = line.substr(6); - size_t parsedId; - size_t posId = line.find(" "); - if (posId != std::string::npos) { - parsedId = NumberParser::parse(line.substr(0, posId)); - - // Parse rewards and labels - line = line.substr(posId+1); - // Check for rewards - if (boost::starts_with(line, "[")) { - // Rewards found - size_t posEndReward = line.find(']'); - STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); - std::string rewardsStr = line.substr(1, posEndReward-1); - STORM_LOG_TRACE("State rewards: " << rewardsStr); - std::vector rewards; - boost::split(rewards, rewardsStr, boost::is_any_of(",")); - if (stateRewards.size() < rewards.size()) { - stateRewards.resize(rewards.size(), std::vector(stateSize, storm::utility::zero())); - } - auto stateRewardsIt = stateRewards.begin(); - for (auto const& rew : rewards) { - (*stateRewardsIt)[state] = valueParser.parseValue(rew); - ++stateRewardsIt; - } - line = line.substr(posEndReward+1); + STORM_LOG_TRACE("New state " << state); + + // Parse state id + line = line.substr(6); // Remove "state " + std::string curString = line; + size_t posEnd = line.find(" "); + if (posEnd != std::string::npos) { + curString = line.substr(0, posEnd); + line = line.substr(posEnd+1); + } else { + line = ""; + } + size_t parsedId = NumberParser::parse(curString); + STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond."); + if (nonDeterministic) { + STORM_LOG_TRACE("new Row Group starts at " << row << "."); + builder.newRowGroup(row); + } + + if (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton) { + // Parse exit rate for CTMC or MA + STORM_LOG_THROW(boost::starts_with(line, "!"), storm::exceptions::WrongFormatException, "Exit rate missing."); + line = line.substr(1); //Remove "!" + curString = line; + posEnd = line.find(" "); + if (posEnd != std::string::npos) { + curString = line.substr(0, posEnd); + line = line.substr(posEnd+1); + } else { + line = ""; + } + ValueType exitRate = valueParser.parseValue(curString); + if (type == storm::models::ModelType::MarkovAutomaton && !storm::utility::isZero(exitRate)) { + modelComponents->markovianStates.get().set(state); + } + STORM_LOG_TRACE("Exit rate " << exitRate); + modelComponents->exitRates.get()[state] = exitRate; + } + + if (boost::starts_with(line, "[")) { + // Parse rewards + size_t posEndReward = line.find(']'); + STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); + std::string rewardsStr = line.substr(1, posEndReward-1); + STORM_LOG_TRACE("State rewards: " << rewardsStr); + std::vector rewards; + boost::split(rewards, rewardsStr, boost::is_any_of(",")); + if (stateRewards.size() < rewards.size()) { + stateRewards.resize(rewards.size(), std::vector(stateSize, storm::utility::zero())); } - // Check for labels + auto stateRewardsIt = stateRewards.begin(); + for (auto const& rew : rewards) { + (*stateRewardsIt)[state] = valueParser.parseValue(rew); + ++stateRewardsIt; + } + line = line.substr(posEndReward+1); + } + + // Parse labels + if (!line.empty()) { std::vector labels; boost::split(labels, line, boost::is_any_of(" ")); for (std::string label : labels) { @@ -166,18 +203,10 @@ namespace storm { modelComponents->stateLabeling.addLabel(label); } modelComponents->stateLabeling.addLabelToState(label, state); - STORM_LOG_TRACE("New label: " << label); + STORM_LOG_TRACE("New label: '" << label << "'"); } - } else { - // Only state id given - parsedId = NumberParser::parse(line); - } - STORM_LOG_TRACE("New state " << state); - STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond."); - if (nonDeterministic) { - STORM_LOG_TRACE("new Row Group starts at " << row << "."); - builder.newRowGroup(row); } + } else if (boost::starts_with(line, "\taction ")) { // New action if (firstAction) { diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index 43c34b3ce..9953a4108 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -21,20 +21,17 @@ namespace storm { // Notice that for CTMCs we write the rate matrix instead of probabilities // Initialize - storm::models::ModelType type = sparseModel->getType(); std::vector exitRates; // Only for CTMCs and MAs. - if(sparseModel->getType() == storm::models::ModelType::Ctmc) { + if (sparseModel->getType() == storm::models::ModelType::Ctmc) { exitRates = sparseModel->template as>()->getExitRateVector(); - } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { - type = storm::models::ModelType::Mdp; - STORM_LOG_WARN("Markov automaton is exported as MDP (indication of Markovian choices is not supported in DRN format)."); + } else if (sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { exitRates = sparseModel->template as>()->getExitRates(); } // Write header os << "// Exported by storm" << std::endl; os << "// Original model type: " << sparseModel->getType() << std::endl; - os << "@type: " << type << std::endl; + os << "@type: " << sparseModel->getType() << std::endl; os << "@parameters" << std::endl; if (parameters.empty()) { for (std::string const& parameter : getParameters(sparseModel)) { @@ -60,6 +57,11 @@ namespace storm { for (typename storm::storage::SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { os << "state " << group; + // Write exit rates for CTMCs and MAs + if (!exitRates.empty()) { + os << " !" << exitRates.at(group); + } + // Write state rewards bool first = true; for (auto const& rewardModelEntry : sparseModel->getRewardModels()) {