From 27e65d5669c35f76883f06f8a66f040ca650bdbf Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 3 Jul 2019 15:44:52 +0200 Subject: [PATCH] Added construction of the state remapping for elimination of non-Markovian states in MAs --- src/storm/models/sparse/MarkovAutomaton.cpp | 164 ++++++++++++++++---- src/storm/models/sparse/MarkovAutomaton.h | 2 + 2 files changed, 137 insertions(+), 29 deletions(-) diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 9d6869d84..c6cc5f19f 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -1,3 +1,5 @@ +#include + #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -16,7 +18,7 @@ namespace storm { namespace models { namespace sparse { - + template MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, @@ -25,7 +27,7 @@ namespace storm { : MarkovAutomaton(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels, true, markovianStates)) { // Intentionally left empty } - + template MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, @@ -34,23 +36,23 @@ namespace storm { : MarkovAutomaton(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), true, std::move(markovianStates))) { // Intentionally left empty } - + template MarkovAutomaton::MarkovAutomaton(storm::storage::sparse::ModelComponents const& components) : NondeterministicModel(ModelType::MarkovAutomaton, components), markovianStates(components.markovianStates.get()) { - + if (components.exitRates) { exitRates = components.exitRates.get(); } - + if (components.rateTransitions) { this->turnRatesToProbabilities(); } closed = this->checkIsClosed(); } - + template MarkovAutomaton::MarkovAutomaton(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::MarkovAutomaton, std::move(components)), markovianStates(std::move(components.markovianStates.get())) { - + if (components.exitRates) { exitRates = std::move(components.exitRates.get()); } @@ -60,52 +62,52 @@ namespace storm { } closed = this->checkIsClosed(); } - + template bool MarkovAutomaton::isClosed() const { return closed; } - + template bool MarkovAutomaton::isHybridState(storm::storage::sparse::state_type state) const { return isMarkovianState(state) && (this->getTransitionMatrix().getRowGroupSize(state) > 1); } - + template bool MarkovAutomaton::isMarkovianState(storm::storage::sparse::state_type state) const { return this->markovianStates.get(state); } - + template bool MarkovAutomaton::isProbabilisticState(storm::storage::sparse::state_type state) const { return !this->markovianStates.get(state); } - + template std::vector const& MarkovAutomaton::getExitRates() const { return this->exitRates; } - + template std::vector& MarkovAutomaton::getExitRates() { return this->exitRates; } - + template ValueType const& MarkovAutomaton::getExitRate(storm::storage::sparse::state_type state) const { return this->exitRates[state]; } - + template ValueType MarkovAutomaton::getMaximalExitRate() const { return storm::utility::vector::max_if(this->exitRates, this->markovianStates); } - + template storm::storage::BitVector const& MarkovAutomaton::getMarkovianStates() const { return this->markovianStates; } - + template void MarkovAutomaton::close() { if (!closed) { @@ -120,16 +122,16 @@ namespace storm { exitRates[state] = storm::utility::zero(); } } - + if (!keptChoices.full()) { *this = std::move(*storm::transformer::buildSubsystem(*this, storm::storage::BitVector(this->getNumberOfStates(), true), keptChoices, false).model->template as>()); } - + // Mark the automaton as closed. closed = true; } } - + template void MarkovAutomaton::turnRatesToProbabilities() { bool assertRates = (this->exitRates.size() == this->getNumberOfStates()); @@ -137,7 +139,7 @@ namespace storm { STORM_LOG_THROW(this->exitRates.empty(), storm::exceptions::InvalidArgumentException, "The specified exit rate vector has an unexpected size."); this->exitRates.reserve(this->getNumberOfStates()); } - + storm::utility::ConstantsComparator comparator; for (uint_fast64_t state = 0; state< this->getNumberOfStates(); ++state) { uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state]; @@ -163,12 +165,12 @@ namespace storm { } } } - + template bool MarkovAutomaton::isConvertibleToCtmc() const { return isClosed() && markovianStates.full(); } - + template bool MarkovAutomaton::hasOnlyTrivialNondeterminism() const { // Check every state @@ -185,7 +187,7 @@ namespace storm { } return true; } - + template bool MarkovAutomaton::checkIsClosed() const { for (auto state : markovianStates) { @@ -195,7 +197,7 @@ namespace storm { } return true; } - + template std::shared_ptr> MarkovAutomaton::convertToCtmc() const { if (isClosed() && markovianStates.full()) { @@ -265,7 +267,109 @@ namespace storm { return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling)); } - + template + std::shared_ptr> + MarkovAutomaton::eliminateNonmarkovianStates() const { + if (isClosed() && markovianStates.full()) { + storm::storage::sparse::ModelComponents components( + this->getTransitionMatrix(), this->getStateLabeling(), this->getRewardModels(), false); + components.exitRates = this->getExitRates(); + if (this->hasChoiceLabeling()) { + components.choiceLabeling = this->getChoiceLabeling(); + } + if (this->hasStateValuations()) { + components.stateValuations = this->getStateValuations(); + } + if (this->hasChoiceOrigins()) { + components.choiceOrigins = this->getChoiceOrigins(); + } + return std::make_shared>(std::move(components)); + } + + std::map stateRemapping; + std::set statesToKeep; + std::queue changedStates; + std::queue queue; + + storm::storage::SparseMatrix backwards = this->getBackwardTransitions(); + + // Determine the state remapping + // TODO Consider state labels + for (uint_fast64_t base_state = 0; base_state < this->getNumberOfStates(); ++base_state) { + STORM_LOG_ASSERT(!this->isHybridState(base_state), "Base state is hybrid."); + if (this->isMarkovianState(base_state)) { + queue.push(base_state); + + while (!queue.empty()) { + auto currState = queue.front(); + queue.pop(); + // Get predecessors from matrix + typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow( + currState); + for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); + entryIt != entryIte; ++entryIt) { + uint_fast64_t predecessor = entryIt->getColumn(); + if (!this->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { + if (!stateRemapping.count(predecessor)) { + stateRemapping[predecessor] = base_state; + queue.push(predecessor); + } else if (stateRemapping[predecessor] != base_state) { + stateRemapping.erase(predecessor); + statesToKeep.insert(predecessor); + changedStates.push(predecessor); + } + } + } + } + } + } + + // Correct the mapping with the states which have to be kept + while (!changedStates.empty()) { + uint_fast64_t base_state = changedStates.front(); + queue.push(base_state); + + while (!queue.empty()) { + auto currState = queue.front(); + queue.pop(); + // Get predecessors from matrix + typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow( + currState); + for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); + entryIt != entryIte; ++entryIt) { + uint_fast64_t predecessor = entryIt->getColumn(); + if (!this->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { + if (!stateRemapping.count(predecessor)) { + stateRemapping[predecessor] = base_state; + queue.push(predecessor); + } else if (stateRemapping[predecessor] != base_state) { + stateRemapping.erase(predecessor); + statesToKeep.insert(predecessor); + changedStates.push(predecessor); + } + } + } + } + + changedStates.pop(); + } + + // At this point, we hopefully have a valid mapping which eliminates a lot of states + + STORM_PRINT("Remapping \n") + for (auto entry : stateRemapping) { + STORM_PRINT(std::to_string(entry.first) << " -> " << std::to_string(entry.second) << "\n") + } + STORM_PRINT("Remapped States: " << stateRemapping.size() << "\n") + // TODO test some examples, especially ones containing non-determinism + + // Build the new matrix + // TODO + + return nullptr; + } + + template void MarkovAutomaton::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); @@ -274,13 +378,15 @@ namespace storm { out << "Max. Rate.: \t" << this->getMaximalExitRate() << std::endl; this->printModelInformationFooterToStream(out); } - - + + template class MarkovAutomaton; #ifdef STORM_HAVE_CARL + template class MarkovAutomaton; - + template class MarkovAutomaton>; + template class MarkovAutomaton; #endif } // namespace sparse diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index b5a7f347f..45ac81a75 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -147,6 +147,8 @@ namespace storm { * @return The resulting CTMC. */ std::shared_ptr> convertToCtmc() const; + + std::shared_ptr> eliminateNonmarkovianStates() const; virtual void printModelInformationToStream(std::ostream& out) const override;