More detailed DFT statistics

src/storm-dft-cli/storm-dft.cpp

@@ -42,9 +42,7 @@ void processOptions() {
     }
 
     if (dftIOSettings.isDisplayStatsSet()) {
-        std::cout << "=============DFT Statistics==============" << std::endl;
         dft->writeStatsToStream(std::cout);
-        std::cout << "=========================================" << std::endl;
     }
 
     if (dftIOSettings.isExportToJson()) {

src/storm-dft/storage/dft/DFT.cpp

@@ -407,6 +407,34 @@ namespace storm {
             return noDyn;
         }
 
+        template<typename ValueType>
+        size_t DFT<ValueType>::nrStaticElements() const {
+            size_t noStatic = 0;
+            for (auto const& elem : mElements) {
+                switch (elem->type()) {
+                    case DFTElementType::AND:
+                    case DFTElementType::OR:
+                    case DFTElementType::VOT:
+                        ++noStatic;
+                        break;
+                    case DFTElementType::BE:
+                    case DFTElementType::CONSTF:
+                    case DFTElementType::CONSTS:
+                    case DFTElementType::PAND:
+                    case DFTElementType::SPARE:
+                    case DFTElementType::POR:
+                    case DFTElementType::SEQ:
+                    case DFTElementType::MUTEX:
+                    case DFTElementType::PDEP:
+                        break;
+                    default:
+                        STORM_LOG_ASSERT(false, "DFT element type " << elem->type() << " not known.");
+                        break;
+                }
+            }
+            return noStatic;
+        }
+
         template<typename ValueType>
         std::string DFT<ValueType>::getElementsString() const {
             std::stringstream stream;
@@ -796,9 +824,99 @@ namespace storm {
 
         template<typename ValueType>
         void DFT<ValueType>::writeStatsToStream(std::ostream& stream) const {
+            // Count individual types of elements
+            size_t noBE = 0;
+            size_t noAnd = 0;
+            size_t noOr = 0;
+            size_t noVot = 0;
+            size_t noPand = 0;
+            size_t noPor = 0;
+            size_t noSpare = 0;
+            size_t noDependency = 0;
+            size_t noRestriction = 0;
+            for (auto const& elem : mElements) {
+                switch (elem->type()) {
+                    case DFTElementType::BE:
+                    case DFTElementType::CONSTF:
+                    case DFTElementType::CONSTS:
+                        ++noBE;
+                        break;
+                    case DFTElementType::AND:
+                        ++noAnd;
+                        break;
+                    case DFTElementType::OR:
+                        ++noOr;
+                        break;
+                    case DFTElementType::VOT:
+                        ++noVot;
+                        break;
+                    case DFTElementType::PAND:
+                        ++noPand;
+                        break;
+                    case DFTElementType::POR:
+                        ++noPor;
+                        break;
+                    case DFTElementType::SPARE:
+                        ++noSpare;
+                        break;
+                    case DFTElementType::PDEP:
+                        ++noDependency;
+                        break;
+                    case DFTElementType::SEQ:
+                    case DFTElementType::MUTEX:
+                        ++noRestriction;
+                        break;
+                    default:
+                        STORM_LOG_ASSERT(false, "DFT element type " << elem->type() << " not known.");
+                        break;
+                }
+            }
+            size_t noStatic = nrStaticElements();
+            size_t noDynamic = nrDynamicElements();
+
+            // Check whether numbers are correct
+            STORM_LOG_ASSERT(noBE == nrBasicElements(), "No. of BEs does not match.");
+            STORM_LOG_ASSERT(noSpare == mNrOfSpares, "No. of SPAREs does not match.");
+            STORM_LOG_ASSERT(noDependency == mDependencies.size(), "No. of Dependencies does not match.");
+            STORM_LOG_ASSERT(noAnd + noOr + noVot == noStatic, "No. of static gates does not match.");
+            STORM_LOG_ASSERT(noPand + noPor + noSpare + noDependency + noRestriction == noDynamic, "No. of dynamic gates does not match.");
+            STORM_LOG_ASSERT(noBE + noStatic + noDynamic == nrElements(), "No. of elements does not match.");
+
+            // Print output
+            stream << "=============DFT Statistics==============" << std::endl;
             stream << "Number of BEs: " << nrBasicElements() << std::endl;
-            stream << "Number of dynamic elements: " << nrDynamicElements() << std::endl;
+            stream << "Number of static elements: " << noStatic << std::endl;
+            stream << "Number of dynamic elements: " << noDynamic << std::endl;
             stream << "Number of elements: " << nrElements() << std::endl;
+            stream << "-----------------------------------------" << std::endl;
+            if (noBE > 0) {
+                stream << "Number of BEs: " << noBE << std::endl;
+            }
+            if (noAnd > 0) {
+                stream << "Number of AND gates: " << noAnd << std::endl;
+            }
+            if (noOr > 0) {
+                stream << "Number of OR gates: " << noOr << std::endl;
+            }
+            if (noVot > 0) {
+                stream << "Number of VOT gates: " << noVot << std::endl;
+            }
+            if (noPand > 0) {
+                stream << "Number of PAND gates: " << noPand << std::endl;
+            }
+            if (noPor > 0) {
+                stream << "Number of POR gates: " << noPor << std::endl;
+            }
+            if (noSpare > 0) {
+                stream << "Number of SPARE gates: " << noSpare << std::endl;
+            }
+            if (noDependency > 0) {
+                stream << "Number of Dependencies: " << noDependency << std::endl;
+            }
+            if (noRestriction > 0) {
+                stream << "Number of Restrictions: " << noRestriction << std::endl;
+            }
+            stream << "=========================================" << std::endl;
         }
         
         // Explicitly instantiate the class.

src/storm-dft/storage/dft/DFT.h

@@ -95,6 +95,8 @@ namespace storm {
 
             size_t nrDynamicElements() const;
 
+            size_t nrStaticElements() const;
+            
             size_t getTopLevelIndex() const {
                 return mTopLevelIndex;
             }