diff --git a/resources/examples/testfiles/dft/const_be_test.dft b/resources/examples/testfiles/dft/const_be_test.dft new file mode 100644 index 000000000..1f5721275 --- /dev/null +++ b/resources/examples/testfiles/dft/const_be_test.dft @@ -0,0 +1,8 @@ +toplevel "A"; +"A" and "I" "J" "K" "L"; +"DEP1" fdep "I" "J" "K"; + +"I" prob=1; +"J" prob=1; +"K" prob=1; +"L" lambda=1.0 dorm=0.5; diff --git a/src/test/storm-dft/api/DftTransformatorTest.cpp b/src/test/storm-dft/api/DftTransformatorTest.cpp new file mode 100644 index 000000000..97646fd83 --- /dev/null +++ b/src/test/storm-dft/api/DftTransformatorTest.cpp @@ -0,0 +1,69 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm-dft/api/storm-dft.h" +#include "storm-dft/transformations/DftTransformator.h" + +namespace { + + TEST(DftTransformatorTest, UniqueConstantFailedTest) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/const_be_test.dft"; + std::shared_ptr> originalDft = storm::api::loadDFTGalileoFile(file); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> transformedDft = dftTransformator.transformUniqueFailedBe( + *originalDft); + + auto bes = transformedDft->getBasicElements(); + uint64_t constBeFailedCount = 0; + uint64_t constBeFailsafeCount = 0; + for (auto &be : bes) { + if (be->type() == storm::storage::DFTElementType::BE_CONST) { + if (be->canFail()) { + ++constBeFailedCount; + } else { + ++constBeFailsafeCount; + } + } + } + + EXPECT_EQ(1ul, constBeFailedCount); + EXPECT_EQ(3ul, constBeFailsafeCount); + } + + TEST(DftTransformatorTest, BinaryFDEPTest) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"; + std::shared_ptr> originalDft = storm::api::loadDFTGalileoFile(file); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> transformedDft = dftTransformator.transformBinaryFDEPs( + *originalDft); + + uint64_t dependencyCount = transformedDft->getDependencies().size(); + + EXPECT_EQ(2ul, dependencyCount); + } + + TEST(DftTransformatorTest, PDEPTransformTest) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"; + std::shared_ptr> originalDft = storm::api::loadDFTGalileoFile(file); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> transformedDft = dftTransformator.transformBinaryFDEPs( + *originalDft); + + uint64_t fdepCount = 0; + uint64_t pdepCount = 0; + + for (auto depIndex : transformedDft->getDependencies()) { + auto dep = transformedDft->getDependency(depIndex); + if (dep->probability() == 1) { + ++fdepCount; + } else { + ++pdepCount; + } + } + + EXPECT_EQ(1ul, pdepCount); + EXPECT_EQ(2ul, fdepCount); + EXPECT_EQ(4ul, transformedDft->nrBasicElements()); + } + +} \ No newline at end of file