diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 7a12ad4a7..bbb03f61c 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -672,7 +672,7 @@ namespace storm { maComponents.exitRates = std::move(modelComponents.exitRates); ma = std::make_shared>(std::move(maComponents)); } - if (ma->isConvertibleToCtmc()) { + if (ma->hasOnlyTrivialNondeterminism()) { model = ma->convertToCtmc(); } else { model = ma; diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 36c743b6a..94d6f0775 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -151,28 +151,18 @@ namespace { } TYPED_TEST(DftModelCheckerTest, FdepMTTF) { + double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft"); + EXPECT_FLOAT_EQ(result, 2); + result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft"); + EXPECT_FLOAT_EQ(result, 2.5); + if (this->getConfig().useMod) { STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"), storm::exceptions::NotSupportedException); -STORM_SILENT_EXPECT_THROW(this-> -analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/fdep2.dft"), storm::exceptions::NotSupportedException); -STORM_SILENT_EXPECT_THROW(this-> -analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/fdep3.dft"), storm::exceptions::NotSupportedException); STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft"), storm::exceptions::NotSupportedException); STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"), storm::exceptions::NotSupportedException); } else { -double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/fdep.dft"); + double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"); EXPECT_FLOAT_EQ(result, 2 / 3.0); -result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/fdep2.dft"); -EXPECT_FLOAT_EQ(result, -2); -result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/fdep3.dft"); -EXPECT_FLOAT_EQ(result, -2.5); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft"); EXPECT_FLOAT_EQ(result, 1); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"); @@ -183,24 +173,14 @@ EXPECT_FLOAT_EQ(result, TYPED_TEST(DftModelCheckerTest, PdepMTTF) { double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft"); EXPECT_FLOAT_EQ(result, 8 / 3.0); + result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft"); + EXPECT_FLOAT_EQ(result, 38 / 15.0); + result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft"); + EXPECT_FLOAT_EQ(result, 67 / 24.0); if (this->getConfig().useMod) { -STORM_SILENT_EXPECT_THROW(this-> -analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/pdep2.dft"), storm::exceptions::NotSupportedException); -STORM_SILENT_EXPECT_THROW(this-> -analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/pdep3.dft"), storm::exceptions::NotSupportedException); STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"), storm::exceptions::NotSupportedException); } else { -result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/pdep2.dft"); -EXPECT_FLOAT_EQ(result, -38 / 15.0); -result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/pdep3.dft"); -EXPECT_FLOAT_EQ(result, -67 / 24.0); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"); EXPECT_EQ(result, storm::utility::infinity()); } @@ -243,21 +223,8 @@ EXPECT_FLOAT_EQ(result, EXPECT_FLOAT_EQ(result, storm::utility::infinity()); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft"); EXPECT_FLOAT_EQ(result, storm::utility::infinity()); -if (this-> - -getConfig() - -.useMod){ -STORM_SILENT_EXPECT_THROW(this-> -analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/seq6.dft"), storm::exceptions::NotSupportedException); -} -else { -result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR -"/dft/seq6.dft"); -EXPECT_FLOAT_EQ(result, -30000); -} + result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft"); + EXPECT_FLOAT_EQ(result,30000); } TYPED_TEST(DftModelCheckerTest, Symmetry) {