diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index b315aa2c0..527cb3868 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -45,7 +45,7 @@ namespace storm { STORM_LOG_ASSERT(this->_producedChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?"); STORM_LOG_ASSERT(this->_memoryTransitions.is_initialized(), "Trying to extract the DA transition structure but none is available. Was there a computation call before?"); STORM_LOG_ASSERT(this->_memoryInitialStates.is_initialized(), "Trying to extract the initial states of the DA but there are none available. Was there a computation call before?"); - STORM_LOG_ASSERT(this->_dontCareStates.is_initialized(), "Trying to extract the dontCare states of the Scheduler but there are none available. Was there a computation call before?"); + STORM_LOG_ASSERT(this->_dontCareStates.is_initialized(), "Trying to extract the Scheduler-dontCare states but there are none available. Was there a computation call before?"); // Create a memory structure for the MDP scheduler with memory. If hasRelevantStates is set, we only consider initial model states relevant. @@ -147,7 +147,7 @@ namespace storm { } for (auto const& conjunction : dnf) { - // determine the set of states of the subMDP that can satisfy the condition, remove all states that would violate Fins in the conjunction + // Determine the set of states of the subMDP that can satisfy the condition, remove all states that would violate Fins in the conjunction. storm::storage::BitVector allowed(transitionMatrix.getRowGroupCount(), true); STORM_LOG_INFO("Handle conjunction " << i); @@ -182,7 +182,7 @@ namespace storm { STORM_LOG_DEBUG(" Allowed states: " << allowed); - // compute MECs in the allowed fragment + // Compute MECs in the allowed fragment storm::storage::MaximalEndComponentDecomposition mecs(transitionMatrix, backwardTransitions, allowed); allMECs += mecs.size(); for (const auto& mec : mecs) { @@ -387,7 +387,6 @@ namespace storm { } } - } } } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 8b85a07de..3d7c21abe 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -25,8 +25,8 @@ namespace storm { public: /*! - * The type of the product automaton (DTMC or MDP) that is used during the computation. - */ + * The type of the product automaton (DTMC or MDP) that is used during the computation. + */ using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::type; /*! diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 51a3f40e8..268fb3b0b 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -248,7 +248,7 @@ namespace storm { // Print memory updates if(!isMemorylessScheduler()) { - out << std::setw(8); + out << std::setw(widthOfStates) << ""; for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; bool firstUpdate = true; @@ -258,10 +258,9 @@ namespace storm { } else { stateString << ", "; } - stateString << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - //out << ", model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = ?) "; - } - } + stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; + // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; + } stateString << std::endl; } @@ -275,11 +274,6 @@ namespace storm { } out << "___________________________________________________________________" << std::endl; - // TODO only for tests: - if(!isMemorylessScheduler()) { - out << memoryStructure->toString(); - out << std::endl; - } } template <> @@ -289,44 +283,78 @@ namespace storm { template void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { - //TODO not defined for memory and unreachable states are not considered STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); - STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers with memory not implemented."); storm::json output; for (uint64_t state = 0; state < schedulerChoices.front().size(); ++state) { // Check whether the state is skipped if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { continue; } - storm::json stateChoicesJson; - if (model && model->hasStateValuations()) { - stateChoicesJson["s"] = model->getStateValuations().template toJson(state); - } else { - stateChoicesJson["s"] = state; - } - auto const& choice = schedulerChoices.front()[state]; - storm::json choicesJson; - if (choice.isDefined()) { - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; - storm::json choiceJson; - if (model && model->hasChoiceOrigins() && model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) { - choiceJson["origin"] = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex); - } - if (model && model->hasChoiceLabeling()) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex); - choiceJson["labels"] = std::vector(choiceLabels.begin(), choiceLabels.end()); + + for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { + // Ignore dontCare states + if ((!isMemorylessScheduler()) && isDontCare(state, memoryState)) { + continue; + } + + storm::json stateChoicesJson; + if (model && model->hasStateValuations()) { + stateChoicesJson["s"] = model->getStateValuations().template toJson(state); + } else { + stateChoicesJson["s"] = state; + } + + if (!isMemorylessScheduler()) { + stateChoicesJson["m"] = memoryState; + } + + auto const &choice = schedulerChoices[memoryState][state]; + storm::json choicesJson; + if (choice.isDefined()) { + for (auto const &choiceProbPair : choice.getChoiceAsDistribution()) { + uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; + storm::json choiceJson; + if (model && model->hasChoiceOrigins() && + model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != + model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) { + choiceJson["origin"] = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex); + } + if (model && model->hasChoiceLabeling()) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex); + choiceJson["labels"] = std::vector(choiceLabels.begin(), + choiceLabels.end()); + } + choiceJson["index"] = globalChoiceIndex; + choiceJson["prob"] = storm::utility::convertNumber( + choiceProbPair.second); + + // Memory updates + if(!isMemorylessScheduler()) { + choiceJson["memory-updates"] = std::vector>(); + uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; + for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { + storm::json updateJson; + // next model state + if (model && model->hasStateValuations()) { + updateJson["s'"] = model->getStateValuations().template toJson(entryIt->getColumn()); + } else { + updateJson["s'"] = entryIt->getColumn(); + } + // next memory state + updateJson["m'"] = this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()); + choiceJson["memory-updates"].push_back(std::move(updateJson)); + } + } + + choicesJson.push_back(std::move(choiceJson)); } - choiceJson["index"] = globalChoiceIndex; - choiceJson["prob"] = storm::utility::convertNumber(choiceProbPair.second); - choicesJson.push_back(std::move(choiceJson)); + } else { + choicesJson = "undefined"; } - } else { - choicesJson = "undefined"; + stateChoicesJson["c"] = std::move(choicesJson); + output.push_back(std::move(stateChoicesJson)); } - stateChoicesJson["c"] = std::move(choicesJson); - output.push_back(std::move(stateChoicesJson)); } out << output.dump(4); }