MA to CTMC for trivial nondeterminism

Former-commit-id: 8a342f032e

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

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;

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 <typename ValueType, typename RewardModelType>
             std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> MarkovAutomaton<ValueType, RewardModelType>::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<ValueType> flexibleMatrix(this->getTransitionMatrix());
+                storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(this->getTransitionMatrix().transpose());
+                storm::solver::stateelimination::MAEliminator<storm::models::sparse::Dtmc<ValueType>> 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<ValueType> 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<ValueType> 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<std::vector<LabelSet>> optionalChoiceLabeling = this->getOptionalChoiceLabeling();
+                if (optionalChoiceLabeling) {
+                    optionalChoiceLabeling = storm::utility::vector::filterVector(optionalChoiceLabeling.get(), keepStates);
+                }
+                //TODO update reward models according to kept states
+                std::unordered_map<std::string, RewardModelType> rewardModels = this->getRewardModels();
+                
+                return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling));
             }
 
             

src/solver/stateelimination/MAEliminator.cpp

@@ -0,0 +1,45 @@
+#include "src/solver/stateelimination/MAEliminator.h"
+
+namespace storm {
+    namespace solver {
+        namespace stateelimination {
+            
+            template<typename SparseModelType>
+            MAEliminator<SparseModelType>::MAEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions){
+            }
+            
+            template<typename SparseModelType>
+            void MAEliminator<SparseModelType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
+                // Do nothing
+            }
+       
+            template<typename SparseModelType>
+            void MAEliminator<SparseModelType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
+                // Do nothing
+            }
+            
+            template<typename SparseModelType>
+            void MAEliminator<SparseModelType>::updatePriority(storm::storage::sparse::state_type const& state) {
+                // Do nothing
+            }
+            
+            template<typename SparseModelType>
+            bool MAEliminator<SparseModelType>::filterPredecessor(storm::storage::sparse::state_type const& state) {
+                assert(false);
+            }
+            
+            template<typename SparseModelType>
+            bool MAEliminator<SparseModelType>::isFilterPredecessor() const {
+                return false;
+            }
+            
+            
+            template class MAEliminator<storm::models::sparse::Dtmc<double>>;
+            
+#ifdef STORM_HAVE_CARL
+            template class MAEliminator<storm::models::sparse::Dtmc<storm::RationalFunction>>;
+#endif
+            
+        } // namespace stateelimination
+    } // namespace storage
+} // namespace storm

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<typename SparseModelType>
+            class MAEliminator : public StateEliminator<SparseModelType> {
+
+                typedef typename SparseModelType::ValueType ValueType;
+
+            public:
+                MAEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& 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_

src/storage/FlexibleSparseMatrix.cpp

@@ -96,6 +96,15 @@ namespace storm {
                 return rowGroupIndices[group + 1] - rowGroupIndices[group];
             }
         }
+        
+        template<typename ValueType>
+        ValueType FlexibleSparseMatrix<ValueType>::getRowSum(index_type row) const {
+            ValueType sum = storm::utility::zero<ValueType>();
+            for (auto const& element : getRow(row)) {
+                sum += element.getValue();
+            }
+            return sum;
+        }
 
         template<typename ValueType>
         void FlexibleSparseMatrix<ValueType>::updateDimensions() {

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.