Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixed issues with DFT representant computation #605

Merged
merged 1 commit into from
Sep 4, 2024
Merged

Fixed issues with DFT representant computation #605

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions resources/examples/testfiles/dft/modules3.dft
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
10 changes: 9 additions & 1 deletion src/storm-dft/storage/DFT.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)));
Expand Down Expand Up @@ -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);
Expand Down
2 changes: 2 additions & 0 deletions src/test/storm-dft/api/DftModelCheckerTest.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
Loading