Build transition matrix for FT

Former-commit-id: 2ffb55295a

src/builder/ExplicitDFTModelBuilder.cpp

@@ -3,16 +3,53 @@
 namespace storm {
     namespace builder {
 
-        void ExplicitDFTModelBuilder::exploreStateSuccessors(storm::storage::DFTState const &state) {
+        template<typename ValueType, typename RewardModelType, typename IndexType>
+        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
+            // Initialize
+            storm::storage::DFTState state(mDft, newIndex++);
+            mStates.insert(state);
+
+            std::queue<storm::storage::DFTState> stateQueue;
+            stateQueue.push(state);
+
+            bool deterministicModel = true;
+            storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
+
+            // Begin model generation
+            exploreStates(stateQueue, transitionMatrixBuilder);
+            //std::cout << "Generated " << mStates.size() << " states" << std::endl;
+
+            // Build CTMC
+            transitionMatrix = transitionMatrixBuilder.build();
+            //std::cout << "TransitionMatrix: " << std::endl;
+            //std::cout << transitionMatrix << std::endl;
+            // TODO Matthias: build CTMC
+        }
+
+        template<typename ValueType, typename RewardModelType, typename IndexType>
+        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
+
+            std::vector<std::pair<size_t, ValueType>> outgoingTransitions;
+
+            while (!stateQueue.empty()) {
+                // Initialization
+                outgoingTransitions.clear();
+                ValueType sum = 0;
+
+                // Consider next state
+                storm::storage::DFTState state = stateQueue.front();
+                stateQueue.pop();
+
                 size_t smallest = 0;
 
+                // Let BE fail
                 while (smallest < state.nrFailableBEs()) {
                     //std::cout << "exploring from: " << mDft.getStateString(state) << std::endl;
 
                     storm::storage::DFTState newState(state);
-                std::pair<std::shared_ptr<storm::storage::DFTBE<double>>, bool> nextBE = newState.letNextBEFail(smallest++);
+                    std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBE = newState.letNextBEFail(smallest++);
                     if (nextBE.first == nullptr) {
-                    //std::cout << "break" << std::endl;
+                        std::cout << "break" << std::endl;
                         break;
 
                     }
@@ -45,12 +82,14 @@ namespace storm {
                     if (it == mStates.end()) {
                         // New state
                         newState.setId(newIndex++);
-                    mStates.insert(newState);
+                        auto itInsert = mStates.insert(newState);
+                        assert(itInsert.second);
+                        it = itInsert.first;
                         //std::cout << "New state " << mDft.getStateString(newState) << std::endl;
 
                         // Recursive call
                         if (!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) {
-                        exploreStateSuccessors(newState);
+                            stateQueue.push(newState);
                         } else {
                             if (mDft.hasFailed(newState)) {
                                 //std::cout << "Failed " << mDft.getStateString(newState) << std::endl;
@@ -63,9 +102,33 @@ namespace storm {
                         // State already exists
                         //std::cout << "State " << mDft.getStateString(*it) << " already exists" << std::endl;
                     }
+
+                    // Set transition
+                    ValueType prob = nextBE.first->activeFailureRate();
+                    outgoingTransitions.push_back(std::make_pair(it->getId(), prob));
+                    sum += prob;
+                } // end while failing BE
+
+                // Add all transitions
+                for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it)
+                {
+                    ValueType rate = it->second / sum;
+                    transitionMatrixBuilder.addNextValue(state.getId(), it->first, rate);
+                    //std::cout << "Added transition from " << state.getId() << " to " << it->first << " with " << rate << std::endl;
                 }
+
+            } // end while queue
         }
 
+        // Explicitly instantiate the class.
+        template
+        class ExplicitDFTModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
+
+#ifdef STORM_HAVE_CARL
+        template class ExplicitDFTModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
+        template class ExplicitDFTModelBuilder<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>, uint32_t>;
+#endif
+
     } // namespace builder
 } // namespace storm
 

src/builder/ExplicitDFTModelBuilder.h

@@ -3,32 +3,42 @@
 
 #include "../storage/dft/DFT.h"
 
+#include <src/models/sparse/StateLabeling.h>
+#include <src/models/sparse/StandardRewardModel.h>
+#include <src/storage/SparseMatrix.h>
+#include <boost/container/flat_set.hpp>
+#include <boost/optional/optional.hpp>
+#include <stack>
 #include <unordered_set>
 
 namespace storm {
     namespace builder {
+
+        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
         class ExplicitDFTModelBuilder {
             storm::storage::DFT const &mDft;
             std::unordered_set<storm::storage::DFTState> mStates;
             size_t newIndex = 0;
-            //std::stack<std::shared_ptr<storm::storage::DFTState>> mStack;
+
+            // The transition matrix.
+            storm::storage::SparseMatrix<ValueType> transitionMatrix;
+
+            // The state labeling.
+            storm::models::sparse::StateLabeling stateLabeling;
+
+            // A vector that stores a labeling for each choice.
+            boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
 
         public:
             ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) {
 
             }
 
-            void buildCTMC() {
-                // Construct starting start
-                storm::storage::DFTState state(mDft, newIndex++);
-                mStates.insert(state);
-                // Begin model generation
-                exploreStateSuccessors(state);
-                std::cout << "Generated " << mStates.size() << " states" << std::endl;
-            }
+            void buildCTMC();
 
         private:
-            void exploreStateSuccessors(storm::storage::DFTState const &state);
+            void exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
+
         };
     }
 }

src/storage/dft/DFTElements.h

@@ -262,14 +262,14 @@ namespace storm {
         
        
 
-        template<typename FailureRateType>
+        template<typename ValueType>
         class DFTBE : public DFTElement {
 
 
-            FailureRateType mActiveFailureRate;
-            FailureRateType mPassiveFailureRate;
+            ValueType mActiveFailureRate;
+            ValueType mPassiveFailureRate;
         public:
-            DFTBE(size_t id, std::string const& name, FailureRateType failureRate, FailureRateType dormancyFactor) :
+            DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) :
             DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
             {
                 
@@ -279,11 +279,11 @@ namespace storm {
                 return 0;
             }
 
-            FailureRateType const& activeFailureRate() const {
+            ValueType const& activeFailureRate() const {
                 return mActiveFailureRate;
             }
 
-            FailureRateType const& passiveFailureRate() const {
+            ValueType const& passiveFailureRate() const {
                 return mPassiveFailureRate;
             }
         

src/storm-dyftee.cpp

@@ -21,7 +21,7 @@ int main(int argc, char** argv) {
     dft.printSpareModules();
 
     std::cout << "Building CTMC..." << std::endl;
-    storm::builder::ExplicitDFTModelBuilder builder(dft);
+    storm::builder::ExplicitDFTModelBuilder<double> builder(dft);
     builder.buildCTMC();
     std::cout << "Built CTMC" << std::endl;
 
@@ -29,4 +29,3 @@ int main(int argc, char** argv) {
     //TODO check CTMC
     //std::cout << "Checked model" << std::endl;
 }
-