Build Markov Automaton instead of CTMC

Former-commit-id: 26c299ad34

src/builder/ExplicitDFTModelBuilder.cpp

@@ -1,5 +1,5 @@
 #include "src/builder/ExplicitDFTModelBuilder.h"
-#include <src/models/sparse/Ctmc.h>
+#include <src/models/sparse/MarkovAutomaton.h>
 #include <src/utility/constants.h>
 #include <src/exceptions/UnexpectedException.h>
 #include <map>
@@ -7,13 +7,13 @@
 namespace storm {
     namespace builder {
 
-        template <typename ValueType, typename RewardModelType, typename IndexType>
-        ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
+        template <typename ValueType>
+        ExplicitDFTModelBuilder<ValueType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
             // Intentionally left empty.
         }
 
-        template<typename ValueType, typename RewardModelType, typename IndexType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
+        template <typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildMA() {
             // Initialize
             DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, newIndex++);
             mStates.findOrAdd(state->status(), state);
@@ -21,15 +21,17 @@ namespace storm {
             std::queue<DFTStatePointer> stateQueue;
             stateQueue.push(state);
 
-            bool deterministicModel = true;
+            bool deterministicModel = false;
+            ModelComponents modelComponents;
+            std::vector<uint_fast64_t> tmpMarkovianStates;
             storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
 
             // Begin model generation
-            exploreStates(stateQueue, transitionMatrixBuilder);
+            exploreStates(stateQueue, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
             STORM_LOG_DEBUG("Generated " << mStates.size() << " states");
 
-            // Build CTMC
-            ModelComponents modelComponents;
+            // Build Markov Automaton
+            modelComponents.markovianStates = storm::storage::BitVector(mStates.size(), tmpMarkovianStates);
             // Build transition matrix
             modelComponents.transitionMatrix = transitionMatrixBuilder.build();
             STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix);
@@ -65,15 +67,17 @@ namespace storm {
                 }
             }
 
-            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model;
-            model = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)));
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates));
             model->printModelInformationToStream(std::cout);
             return model;
         }
 
-        template<typename ValueType, typename RewardModelType, typename IndexType>
-        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder) {
+        template <typename ValueType>
+        void ExplicitDFTModelBuilder<ValueType>::exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
 
+            assert(exitRates.empty());
+            assert(markovianStates.empty());
+            // TODO Matthias: set Markovian states
             std::map<size_t, ValueType> outgoingTransitions;
 
             while (!stateQueue.empty()) {
@@ -90,6 +94,8 @@ namespace storm {
                 if (mDft.hasFailed(state) || mDft.isFailsafe(state)) {
                     transitionMatrixBuilder.addNextValue(state->getId(), state->getId(), storm::utility::one<ValueType>());
                     STORM_LOG_TRACE("Added self loop for " << state->getId());
+                    exitRates.push_back(storm::utility::one<ValueType>());
+                    assert(exitRates.size()-1 == state->getId());
                     // No further exploration required
                     continue;
                 } else {
@@ -169,20 +175,23 @@ namespace storm {
                 } // end while failing BE
 
                 // Add all transitions
+                ValueType exitRate = storm::utility::zero<ValueType>();
                 for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it)
                 {
                     transitionMatrixBuilder.addNextValue(state->getId(), it->first, it->second);
+                    exitRate += it->second;
                 }
+                exitRates.push_back(exitRate);
+                assert(exitRates.size()-1 == state->getId());
 
             } // end while queue
         }
 
         // Explicitly instantiate the class.
-        template class ExplicitDFTModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
+        template class ExplicitDFTModelBuilder<double>;
 
 #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>;
+        template class ExplicitDFTModelBuilder<storm::RationalFunction>;
 #endif
 
     } // namespace builder

src/builder/ExplicitDFTModelBuilder.h

@@ -16,7 +16,7 @@
 namespace storm {
     namespace builder {
 
-        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
+        template<typename ValueType>
         class ExplicitDFTModelBuilder {
 
             using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
@@ -33,8 +33,11 @@ namespace storm {
                 // The state labeling.
                 storm::models::sparse::StateLabeling stateLabeling;
 
-                // The reward models associated with the model.
-                std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels;
+                // The Markovian states.
+                storm::storage::BitVector markovianStates;
+
+                // The exit rates.
+                std::vector<ValueType> exitRates;
 
                 // A vector that stores a labeling for each choice.
                 boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
@@ -50,10 +53,10 @@ namespace storm {
                 // 2^nrBE is upper bound for state space
             }
 
-            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildCTMC();
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildMA();
 
         private:
-            void exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
+            void exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
 
         };
     }

src/storage/dft/DFTBuilder.h

@@ -69,15 +69,12 @@ namespace storm {
                 }
 
                 for (size_t i = 1; i < children.size(); ++i) {
-                    // TODO Matthias: better code
-                    std::stringstream stream;
-                    stream << name << "_" << i;
-                    std::string s = stream.str();
-                    if(mElements.count(s) != 0) {
+                    std::string nameFdep = name + "_" + std::to_string(i);
+                    if(mElements.count(nameFdep) != 0) {
                         // Element with that name already exists.
                         return false;
                     }
-                    DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, s, trigger, children[i], storm::utility::one<ValueType>());
+                    DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameFdep, trigger, children[i], storm::utility::one<ValueType>());
                     mElements[element->name()] = element;
                     mDependencies.push_back(element);
                 }

src/storm-dyftee.cpp

@@ -6,7 +6,7 @@
 #include "utility/storm.h"
 
 /*!
- * Load DFT from filename, build corresponding CTMC and check against given property.
+ * Load DFT from filename, build corresponding Markov Automaton and check against given property.
  *
  * @param filename Path to DFT file in Galileo format.
  * @param property PCTC formula capturing the property to check.
@@ -19,21 +19,21 @@ void analyzeDFT(std::string filename, std::string property) {
     storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
     std::cout << "Built data structure" << std::endl;
 
-    // Building CTMC
-    std::cout << "Building CTMC..." << std::endl;
+    // Building Markov Automaton
+    std::cout << "Building Markov Automaton..." << std::endl;
     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft);
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildCTMC();
-    std::cout << "Built CTMC" << std::endl;
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildMA();
+    std::cout << "Built Markov Automaton" << std::endl;
 
     // Model checking
     std::cout << "Model checking..." << std::endl;
     std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit(property);
     assert(formulas.size() == 1);
-    std::unique_ptr<storm::modelchecker::CheckResult> resultCtmc(storm::verifySparseModel(model, formulas[0]));
-    assert(resultCtmc);
+    std::unique_ptr<storm::modelchecker::CheckResult> resultMA(storm::verifySparseModel(model, formulas[0]));
+    assert(resultMA);
     std::cout << "Result: ";
-    resultCtmc->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
-    std::cout << *resultCtmc << std::endl;
+    resultMA->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+    std::cout << *resultMA << std::endl;
 }
 
 /*!