Fix in DFTs to translate MAs to CTMCs again

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -672,7 +672,7 @@ namespace storm {
                     maComponents.exitRates = std::move(modelComponents.exitRates);
                     ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                 }
-                if (ma->isConvertibleToCtmc()) {
+                if (ma->hasOnlyTrivialNondeterminism()) {
                     model = ma->convertToCtmc();
                 } else {
                     model = ma;

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<double>());
         }
@@ -243,21 +223,8 @@ EXPECT_FLOAT_EQ(result,
         EXPECT_FLOAT_EQ(result, storm::utility::infinity<double>());
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft");
         EXPECT_FLOAT_EQ(result, storm::utility::infinity<double>());
-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) {