Fixed issues with DFT representant computation

volkm · Sep 4, 2024 · 8bae7c1 · 8bae7c1
1 parent d61ad71
commit 8bae7c1
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 1 deletion.
diff --git a/resources/examples/testfiles/dft/modules3.dft b/resources/examples/testfiles/dft/modules3.dft
@@ -0,0 +1,7 @@
+toplevel "T";
+"T" or "M" "S";
+"M" and "A" "B";
+"S" wsp "C" "B";
+"A" lambda=1.0 dorm=0.0;
+"B" lambda=1.0 dorm=0.0;
+"C" lambda=1.0 dorm=0.0;
diff --git a/src/storm-dft/storage/DFT.cpp b/src/storm-dft/storage/DFT.cpp
@@ -39,7 +39,6 @@ DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& t
                 for (size_t modelem : module) {
                     if (mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) {
                         sparesAndBes.insert(modelem);
-                        mRepresentants.insert(std::make_pair(modelem, spareReprs->id()));
                     }
                 }
                 mModules.insert(std::make_pair(spareReprs->id(), storm::dft::storage::DftModule(spareReprs->id(), sparesAndBes)));
@@ -85,6 +84,15 @@ DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& t
     }
     mModules.insert(std::make_pair(mTopLevelIndex, topModule));
 
+    // Set representants for all spare modules
+    for (auto const& module : mModules) {
+        if (module.first != mTopLevelIndex) {
+            for (auto const& index : module.second.getElements()) {
+                mRepresentants.insert(std::make_pair(index, module.first));
+            }
+        }
+    }
+
     // Reserve space for failed spares
     ++mMaxSpareChildCount;
     mStateVectorSize = DFTStateGenerationInfo::getStateVectorSize(nrElements(), mNrOfSpares, mNrRepresentatives, mMaxSpareChildCount);

diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -233,6 +233,8 @@ TYPED_TEST(DftModelCheckerTest, SpareMTTF) {
     EXPECT_NEAR(result, 249 / 52.0, this->precision());  // DFTCalc has result of 4.33779 due to different semantics of nested spares
     result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare_dc.dft");
     EXPECT_NEAR(result, 78311 / 182700.0, this->precision());
+    result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/modules3.dft");
+    EXPECT_NEAR(result, 7 / 6.0, this->precision());
 }
 
 TYPED_TEST(DftModelCheckerTest, SeqMTTF) {