diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index d0fa84495..c166f7536 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/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()) { diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index ad89354f3..e758f209b 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -407,6 +407,34 @@ namespace storm { return noDyn; } + template + size_t DFT::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 std::string DFT::getElementsString() const { std::stringstream stream; @@ -796,9 +824,99 @@ namespace storm { template void DFT::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. diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index aed02807d..8999ef6ea 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -94,6 +94,8 @@ namespace storm { } size_t nrDynamicElements() const; + + size_t nrStaticElements() const; size_t getTopLevelIndex() const { return mTopLevelIndex;