diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index e71f8e4b9..ad1f5d449 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -14,6 +14,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/logic/AtomicLabelFormula.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm/transformer/NonMarkovianChainTransformer.h" namespace storm { @@ -653,8 +654,9 @@ namespace storm { } if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC - // TODO: change components which were not moved accordingly - model = ma->convertToCtmc(); + // TODO apply transformer to all MAs + model = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( + ma); } else { model = ma; } diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index be443199e..85f6b5d21 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -1,5 +1,4 @@ #include -#include #include "storm/models/sparse/MarkovAutomaton.h" @@ -268,202 +267,6 @@ namespace storm { return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling)); } - template - std::shared_ptr> - MarkovAutomaton::eliminateNonmarkovianStates() const { - // TODO reward models - - STORM_LOG_WARN("State elimination is currently not label preserving!"); - 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 eliminationMapping; - 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 (!eliminationMapping.count(predecessor)) { - eliminationMapping[predecessor] = base_state; - queue.push(predecessor); - } else if (eliminationMapping[predecessor] != base_state) { - eliminationMapping.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 (!eliminationMapping.count(predecessor)) { - eliminationMapping[predecessor] = base_state; - queue.push(predecessor); - } else if (eliminationMapping[predecessor] != base_state) { - eliminationMapping.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("Elimination Mapping" << std::endl) - for (auto entry : eliminationMapping) { - STORM_PRINT(std::to_string(entry.first) << " -> " << std::to_string(entry.second) << std::endl) - }*/ - STORM_PRINT("Eliminating " << eliminationMapping.size() << " states" << std::endl) - - // TODO explore if one can construct elimination mapping and state remapping in one step - - // Construct a mapping of old state space to new one - std::vector stateRemapping(this->getNumberOfStates(), -1); - uint_fast64_t currentNewState = 0; - for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { - if (eliminationMapping.count(state) > 0) { - if (stateRemapping[eliminationMapping[state]] == uint_fast64_t(-1)) { - stateRemapping[eliminationMapping[state]] = currentNewState; - stateRemapping[state] = currentNewState; - ++currentNewState; - queue.push(eliminationMapping[state]); - } else { - stateRemapping[state] = stateRemapping[eliminationMapping[state]]; - } - } else if (stateRemapping[state] == uint_fast64_t(-1)) { - stateRemapping[state] = currentNewState; - queue.push(state); - ++currentNewState; - } - } - - // Build the new MA - storm::storage::SparseMatrix newTransitionMatrix; - storm::models::sparse::StateLabeling newStateLabeling( - this->getNumberOfStates() - eliminationMapping.size()); - storm::storage::BitVector newMarkovianStates(this->getNumberOfStates() - eliminationMapping.size(), - false); - std::vector newExitRates; - //TODO choice labeling - boost::optional choiceLabeling; - - // Initialize the matrix builder and helper variables - storm::storage::SparseMatrixBuilder matrixBuilder = storm::storage::SparseMatrixBuilder( - 0, 0, 0, false, true, 0); - uint_fast64_t currentRow = 0; - uint_fast64_t state = 0; - while (!queue.empty()) { - state = queue.front(); - queue.pop(); - - for (auto const &label : this->getLabelsOfState(state)) { - if (!newStateLabeling.containsLabel(label)) { - newStateLabeling.addLabel(label); - } - - newStateLabeling.addLabelToState(label, stateRemapping[state]); - } - - // Use a set to not include redundant rows - std::set> rowSet; - for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowGroupSize(state); ++row) { - std::map transitions; - for (typename storm::storage::SparseMatrix::const_iterator itEntry = this->getTransitionMatrix().getRow( - state, row).begin(); - itEntry != this->getTransitionMatrix().getRow(state, row).end(); ++itEntry) { - uint_fast64_t newId = stateRemapping[itEntry->getColumn()]; - if (transitions.count(newId) == 0) { - transitions[newId] = itEntry->getValue(); - } else { - transitions[newId] += itEntry->getValue(); - } - } - rowSet.insert(transitions); - } - - // correctly set rates - auto rate = storm::utility::zero(); - - if (this->isMarkovianState(state)) { - newMarkovianStates.set(stateRemapping[state], true); - rate = this->exitRates.at(state); - } - - newExitRates.push_back(rate); - // Build matrix - matrixBuilder.newRowGroup(currentRow); - for (auto const &row : rowSet) { - for (auto const &transition : row) { - matrixBuilder.addNextValue(currentRow, transition.first, transition.second); - //STORM_PRINT(stateRemapping[state] << "->" << transition.first << " : " << transition.second << std::endl) - } - ++currentRow; - } - } - newTransitionMatrix = matrixBuilder.build(); - - storm::storage::sparse::ModelComponents newComponents = storm::storage::sparse::ModelComponents( - std::move(newTransitionMatrix), std::move(newStateLabeling)); - - newComponents.rateTransitions = false; - newComponents.markovianStates = std::move(newMarkovianStates); - newComponents.exitRates = std::move(newExitRates); - - return std::make_shared>( - std::move(newComponents)); - } - template void MarkovAutomaton::printModelInformationToStream(std::ostream& out) const { diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index 45ac81a75..c7ca80f35 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -148,7 +148,6 @@ namespace storm { */ std::shared_ptr> convertToCtmc() const; - std::shared_ptr> eliminateNonmarkovianStates() const; virtual void printModelInformationToStream(std::ostream& out) const override; diff --git a/src/storm/transformer/NonMarkovianChainTransformer.cpp b/src/storm/transformer/NonMarkovianChainTransformer.cpp new file mode 100644 index 000000000..1bc460ba5 --- /dev/null +++ b/src/storm/transformer/NonMarkovianChainTransformer.cpp @@ -0,0 +1,233 @@ +#include + +#include "NonMarkovianChainTransformer.h" + +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/constants.h" +#include "storm/utility/ConstantsComparator.h" +#include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/utility/graph.h" + +namespace storm { + namespace transformer { + + template + std::shared_ptr> + NonMarkovianChainTransformer::eliminateNonmarkovianStates( + std::shared_ptr> ma, + bool preserveLabels) { + // TODO reward models + + STORM_LOG_WARN("State elimination is currently not label preserving!"); + STORM_LOG_WARN("Reward Models and Choice Labelings are ignored!"); + if (ma->isClosed() && ma->getMarkovianStates().full()) { + storm::storage::sparse::ModelComponents components( + ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false); + components.exitRates = ma->getExitRates(); + if (ma->hasChoiceLabeling()) { + components.choiceLabeling = ma->getChoiceLabeling(); + } + if (ma->hasStateValuations()) { + components.stateValuations = ma->getStateValuations(); + } + if (ma->hasChoiceOrigins()) { + components.choiceOrigins = ma->getChoiceOrigins(); + } + return std::make_shared>( + std::move(components)); + } + + std::map eliminationMapping; + std::set statesToKeep; + std::queue changedStates; + std::queue queue; + + storm::storage::SparseMatrix backwards = ma->getBackwardTransitions(); + + // Determine the state remapping + // TODO Consider state labels + for (uint_fast64_t base_state = 0; base_state < ma->getNumberOfStates(); ++base_state) { + STORM_LOG_ASSERT(!ma->isHybridState(base_state), "Base state is hybrid."); + if (ma->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 (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { + if (!eliminationMapping.count(predecessor)) { + eliminationMapping[predecessor] = base_state; + queue.push(predecessor); + } else if (eliminationMapping[predecessor] != base_state) { + eliminationMapping.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 (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { + if (!eliminationMapping.count(predecessor)) { + eliminationMapping[predecessor] = base_state; + queue.push(predecessor); + } else if (eliminationMapping[predecessor] != base_state) { + eliminationMapping.erase(predecessor); + statesToKeep.insert(predecessor); + changedStates.push(predecessor); + } + } + } + } + + changedStates.pop(); + } + + // At ma point, we hopefully have a valid mapping which eliminates a lot of states + + /*STORM_PRINT("Elimination Mapping" << std::endl) + for (auto entry : eliminationMapping) { + STORM_PRINT(std::to_string(entry.first) << " -> " << std::to_string(entry.second) << std::endl) + }*/ + STORM_PRINT("Eliminating " << eliminationMapping.size() << " states" << std::endl) + + // TODO explore if one can construct elimination mapping and state remapping in one step + + // Construct a mapping of old state space to new one + std::vector stateRemapping(ma->getNumberOfStates(), -1); + uint_fast64_t currentNewState = 0; + for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) { + if (eliminationMapping.count(state) > 0) { + if (stateRemapping[eliminationMapping[state]] == uint_fast64_t(-1)) { + stateRemapping[eliminationMapping[state]] = currentNewState; + stateRemapping[state] = currentNewState; + ++currentNewState; + queue.push(eliminationMapping[state]); + } else { + stateRemapping[state] = stateRemapping[eliminationMapping[state]]; + } + } else if (stateRemapping[state] == uint_fast64_t(-1)) { + stateRemapping[state] = currentNewState; + queue.push(state); + ++currentNewState; + } + } + + // Build the new MA + storm::storage::SparseMatrix newTransitionMatrix; + storm::models::sparse::StateLabeling newStateLabeling( + ma->getNumberOfStates() - eliminationMapping.size()); + storm::storage::BitVector newMarkovianStates(ma->getNumberOfStates() - eliminationMapping.size(), + false); + std::vector newExitRates; + //TODO choice labeling + boost::optional choiceLabeling; + + // Initialize the matrix builder and helper variables + storm::storage::SparseMatrixBuilder matrixBuilder = storm::storage::SparseMatrixBuilder( + 0, 0, 0, false, true, 0); + uint_fast64_t currentRow = 0; + uint_fast64_t state = 0; + while (!queue.empty()) { + state = queue.front(); + queue.pop(); + + for (auto const &label : ma->getLabelsOfState(state)) { + if (!newStateLabeling.containsLabel(label)) { + newStateLabeling.addLabel(label); + } + + newStateLabeling.addLabelToState(label, stateRemapping[state]); + } + + // Use a set to not include redundant rows + std::set> rowSet; + for (uint_fast64_t row = 0; row < ma->getTransitionMatrix().getRowGroupSize(state); ++row) { + std::map transitions; + for (typename storm::storage::SparseMatrix::const_iterator itEntry = ma->getTransitionMatrix().getRow( + state, row).begin(); + itEntry != ma->getTransitionMatrix().getRow(state, row).end(); ++itEntry) { + uint_fast64_t newId = stateRemapping[itEntry->getColumn()]; + if (transitions.count(newId) == 0) { + transitions[newId] = itEntry->getValue(); + } else { + transitions[newId] += itEntry->getValue(); + } + } + rowSet.insert(transitions); + } + + // correctly set rates + auto rate = storm::utility::zero(); + + if (ma->isMarkovianState(state)) { + newMarkovianStates.set(stateRemapping[state], true); + rate = ma->getExitRates().at(state); + } + + newExitRates.push_back(rate); + // Build matrix + matrixBuilder.newRowGroup(currentRow); + for (auto const &row : rowSet) { + for (auto const &transition : row) { + matrixBuilder.addNextValue(currentRow, transition.first, transition.second); + //STORM_PRINT(stateRemapping[state] << "->" << transition.first << " : " << transition.second << std::endl) + } + ++currentRow; + } + } + newTransitionMatrix = matrixBuilder.build(); + + storm::storage::sparse::ModelComponents newComponents = storm::storage::sparse::ModelComponents( + std::move(newTransitionMatrix), std::move(newStateLabeling)); + + newComponents.rateTransitions = false; + newComponents.markovianStates = std::move(newMarkovianStates); + newComponents.exitRates = std::move(newExitRates); + auto model = std::make_shared>( + std::move(newComponents)); + if (model->isConvertibleToCtmc()) { + return model->convertToCtmc(); + } else { + return model; + } + } + + + template + class NonMarkovianChainTransformer; + +#ifdef STORM_HAVE_CARL + + template + class NonMarkovianChainTransformer; + +#endif + } +} + diff --git a/src/storm/transformer/NonMarkovianChainTransformer.h b/src/storm/transformer/NonMarkovianChainTransformer.h new file mode 100644 index 000000000..ae6759a94 --- /dev/null +++ b/src/storm/transformer/NonMarkovianChainTransformer.h @@ -0,0 +1,27 @@ +#include "storm/models/sparse/MarkovAutomaton.h" + +namespace storm { + namespace transformer { + /** + * Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov Automata + */ + template> + class NonMarkovianChainTransformer { + public: + /** + * Generates a model with the same basic behavior as the input, but eliminates non-Markovian chains. + * If no non-determinism occurs, a CTMC is generated. + * + * @param ma the input Markov Automaton + * @param preserveLabels if set, the procedure considers the labels of non-Markovian states when eliminating states + * @return a reference to the new Mmodel after eliminating non-Markovian states + */ + static std::shared_ptr< + models::sparse::Model < ValueType, RewardModelType>> eliminateNonmarkovianStates(std::shared_ptr< + models::sparse::MarkovAutomaton < ValueType, RewardModelType>> ma, + bool preserveLabels = true + ); + }; + } +} +