diff --git a/benchmark_dft.py b/benchmark_dft.py index 8e9a5462b..edfc88bda 100644 --- a/benchmark_dft.py +++ b/benchmark_dft.py @@ -20,6 +20,7 @@ benchmarks = [ ("deathegg", False, [46.667, 1]), ("fdep", False, [0.666667, 1]), ("fdep2", False, [2, 1]), + ("fdep3", False, [2.5, 1]), #("ftpp_complex", False, [0, 1]), # Compute #("ftpp_large", False, [0, 1]), # Compute #("ftpp_standard", False, [0, 1]), # Compute diff --git a/examples/dft/fdep3.dft b/examples/dft/fdep3.dft new file mode 100644 index 000000000..3815c9973 --- /dev/null +++ b/examples/dft/fdep3.dft @@ -0,0 +1,5 @@ +toplevel "A"; +"A" and "B" "C" "F"; +"F" fdep "B" "C"; +"B" lambda=0.4 dorm=0; +"C" lambda=0.8 dorm=0; diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index c95957248..c757af1a0 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -5,6 +5,8 @@ #include "src/adapters/CarlAdapter.h" #include "src/storage/FlexibleSparseMatrix.h" #include "src/models/sparse/Dtmc.h" +#include "src/solver/stateelimination/MAEliminator.h" +#include "src/utility/vector.h" namespace storm { namespace models { @@ -238,7 +240,57 @@ namespace storm { template std::shared_ptr> MarkovAutomaton::convertToCTMC() { - assert(false) + STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix()); + STORM_LOG_TRACE("Markovian states: " << getMarkovianStates()); + + // Eliminate all probabilistic states by state elimination + // Initialize + storm::storage::FlexibleSparseMatrix flexibleMatrix(this->getTransitionMatrix()); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(this->getTransitionMatrix().transpose()); + storm::solver::stateelimination::MAEliminator> stateEliminator(flexibleMatrix, flexibleBackwardTransitions); + + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + assert(!this->isHybridState(state)); + if (this->isProbabilisticState(state)) { + // Eliminate this probabilistic state + stateEliminator.eliminateState(state, true); + STORM_LOG_TRACE("Flexible matrix after eliminating state " << state << ":" << std::endl << flexibleMatrix); + } + } + + // Create the rate matrix for the CTMC + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, false); + // Remember state to keep + storm::storage::BitVector keepStates(this->getNumberOfStates(), true); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + if (storm::utility::isZero(flexibleMatrix.getRowSum(state))) { + // State is eliminated and can be discarded + keepStates.set(state, false); + } else { + assert(this->isMarkovianState(state)); + // Copy transitions + for (uint_fast64_t row = flexibleMatrix.getRowGroupIndices()[state]; row < flexibleMatrix.getRowGroupIndices()[state + 1]; ++row) { + for (auto const& entry : flexibleMatrix.getRow(row)) { + // Convert probabilities into rates + transitionMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue() * exitRates[state]); + } + } + } + } + + storm::storage::SparseMatrix rateMatrix = transitionMatrixBuilder.build(); + rateMatrix = rateMatrix.getSubmatrix(false, keepStates, keepStates, false); + STORM_LOG_TRACE("New CTMC matrix:" << std::endl << rateMatrix); + // Construct CTMC + storm::models::sparse::StateLabeling stateLabeling = this->getStateLabeling().getSubLabeling(keepStates); + boost::optional> optionalChoiceLabeling = this->getOptionalChoiceLabeling(); + if (optionalChoiceLabeling) { + optionalChoiceLabeling = storm::utility::vector::filterVector(optionalChoiceLabeling.get(), keepStates); + } + //TODO update reward models according to kept states + std::unordered_map rewardModels = this->getRewardModels(); + + return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)); } diff --git a/src/solver/stateelimination/MAEliminator.cpp b/src/solver/stateelimination/MAEliminator.cpp new file mode 100644 index 000000000..7a26e995c --- /dev/null +++ b/src/solver/stateelimination/MAEliminator.cpp @@ -0,0 +1,45 @@ +#include "src/solver/stateelimination/MAEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + MAEliminator::MAEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions) : StateEliminator(transitionMatrix, backwardTransitions){ + } + + template + void MAEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + // Do nothing + } + + template + void MAEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + // Do nothing + } + + template + void MAEliminator::updatePriority(storm::storage::sparse::state_type const& state) { + // Do nothing + } + + template + bool MAEliminator::filterPredecessor(storm::storage::sparse::state_type const& state) { + assert(false); + } + + template + bool MAEliminator::isFilterPredecessor() const { + return false; + } + + + template class MAEliminator>; + +#ifdef STORM_HAVE_CARL + template class MAEliminator>; +#endif + + } // namespace stateelimination + } // namespace storage +} // namespace storm diff --git a/src/solver/stateelimination/MAEliminator.h b/src/solver/stateelimination/MAEliminator.h new file mode 100644 index 000000000..d4db284c3 --- /dev/null +++ b/src/solver/stateelimination/MAEliminator.h @@ -0,0 +1,32 @@ +#ifndef STORM_SOLVER_STATEELIMINATION_MAELIMINATOR_H_ +#define STORM_SOLVER_STATEELIMINATION_MAELIMINATOR_H_ + +#include "src/solver/stateelimination/StateEliminator.h" + +namespace storm { + namespace solver { + namespace stateelimination { + + template + class MAEliminator : public StateEliminator { + + typedef typename SparseModelType::ValueType ValueType; + + public: + MAEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); + + // Instantiaton of Virtual methods + void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override; + void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override; + void updatePriority(storm::storage::sparse::state_type const& state) override; + bool filterPredecessor(storm::storage::sparse::state_type const& state) override; + bool isFilterPredecessor() const override; + + private: + }; + + } // namespace stateelimination + } // namespace storage +} // namespace storm + +#endif // STORM_SOLVER_STATEELIMINATION_MAELIMINATOR_H_ diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index 03fcf3d57..60422dc08 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -96,6 +96,15 @@ namespace storm { return rowGroupIndices[group + 1] - rowGroupIndices[group]; } } + + template + ValueType FlexibleSparseMatrix::getRowSum(index_type row) const { + ValueType sum = storm::utility::zero(); + for (auto const& element : getRow(row)) { + sum += element.getValue(); + } + return sum; + } template void FlexibleSparseMatrix::updateDimensions() { diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h index d7e74f062..28100e0a2 100644 --- a/src/storage/FlexibleSparseMatrix.h +++ b/src/storage/FlexibleSparseMatrix.h @@ -128,6 +128,14 @@ namespace storm { * @return The number of rows that belong to the given row group. */ index_type getRowGroupSize(index_type group) const; + + /*! + * Computes the sum of the entries in a given row. + * + * @param row The row that is to be summed. + * @return The sum of the selected row. + */ + value_type getRowSum(index_type row) const; /*! * Recomputes the number of columns and the number of non-zero entries.