Added tests for SMT encoding

resources/examples/testfiles/dft/spareTwoModules.dft

@@ -0,0 +1,8 @@
+toplevel "A";
+"A" or "B" "C";
+"B" wsp "K" "J" "I";
+"C" wsp "L" "J" "I";
+"I" lambda=0.5 dorm=0.5;
+"J" lambda=1 dorm=0.5;
+"K" lambda=0.5 dorm=0.5;
+"L" lambda=0.5 dorm=0.5;

src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@@ -119,8 +119,8 @@ namespace storm {
                 }
             }
 
-            // Constraint (8)
-            addClaimingConstraints();
+            // Constraint (8) intentionally commented out for testing purposes
+            //addClaimingConstraints();
 
             // Handle dependencies
             addMarkovianConstraints();
@@ -505,10 +505,8 @@ namespace storm {
         }
 
         uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) {
+            STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail");
             STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
-            if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) {
-                return notFailed;
-            }
             uint64_t bound = 0;
             while (bound < notFailed) {
                 setSolverTimeout(timeout * 1000);
@@ -518,7 +516,7 @@ namespace storm {
                     case storm::solver::SmtSolver::CheckResult::Sat:
                         return bound;
                     case storm::solver::SmtSolver::CheckResult::Unknown:
-                        STORM_LOG_DEBUG("Solver returned 'Unknown'");
+                        STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'");
                         return bound;
                     default:
                         ++bound;
@@ -530,6 +528,7 @@ namespace storm {
         }
 
         uint64_t DFTASFChecker::getAlwaysFailedBound(uint_fast64_t timeout) {
+            STORM_LOG_TRACE("Compute bound for number of BE failures such that the DFT always fails");
             STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
             if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) {
                 return notFailed;
@@ -543,7 +542,7 @@ namespace storm {
                     case storm::solver::SmtSolver::CheckResult::Sat:
                         return bound;
                     case storm::solver::SmtSolver::CheckResult::Unknown:
-                        STORM_LOG_DEBUG("Solver returned 'Unknown'");
+                        STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'");
                         return bound;
                     default:
                         --bound;

src/test/storm-dft/api/DftSmtTest.cpp

@@ -23,4 +23,26 @@ namespace {
         smtChecker.toSolver();
         EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Sat);
     }
+
+    TEST(DftSmtTest, SpareTest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spareTwoModules.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+        EXPECT_EQ(smtChecker.checkTleFailsWithLeq(2), storm::solver::SmtSolver::CheckResult::Unsat);
+        EXPECT_EQ(smtChecker.checkTleFailsWithEq(3), storm::solver::SmtSolver::CheckResult::Sat);
+    }
+
+    TEST(DftSmtTest, BoundTest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+        EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(2));
+        EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(4));
+    }
 }