Added upper bound correction

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

@@ -35,12 +35,21 @@ namespace storm {
                     case storm::storage::DFTElementType::BE:
                         beVariables.push_back(varNames.size() - 1);
                         break;
-                    case storm::storage::DFTElementType::SPARE:
-                    {
+                    case storm::storage::DFTElementType::SPARE: {
                         auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
                         for (auto const &spareChild : spare->children()) {
                             varNames.push_back("c_" + element->name() + "_" + spareChild->name());
-                            claimVariables.emplace(SpareAndChildPair(element->id(), spareChild->id()), varNames.size() - 1);
+                            claimVariables.emplace(SpareAndChildPair(element->id(), spareChild->id()),
+                                                   varNames.size() - 1);
+                        }
+                        break;
+                    }
+                    case storm::storage::DFTElementType::PDEP: {
+                        auto dep = std::static_pointer_cast<storm::storage::DFTDependency<double> const>(element);
+                        for (auto const &depEvent : dep->dependentEvents()) {
+                            varNames.push_back("d_" + element->name() + "_" + depEvent->name());
+                            dependencyVariables.emplace(DependencyPair(element->id(), depEvent->id()),
+                                                        varNames.size() - 1);
                         }
                         break;
                     }
@@ -114,7 +123,8 @@ namespace storm {
                         // FDEPs are considered later in the Markovian constraints
                         break;
                     default:
-                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "SMT encoding for type '" << element->type() << "' is not supported.");
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
+                                        "SMT encoding for type '" << element->type() << "' is not supported.");
                         break;
                 }
             }
@@ -323,6 +333,11 @@ namespace storm {
             }
         }
 
+        void DFTASFChecker::generatePdepConstraint(size_t i, std::vector<uint64_t> childVarIndices,
+                                                   std::shared_ptr<storm::storage::DFTElement<ValueType> const> element) {
+            // TODO
+        }
+
         void DFTASFChecker::addMarkovianConstraints() {
             uint64_t nrMarkovian = dft.nrBasicElements();
             std::set<size_t> depElements;
@@ -341,16 +356,22 @@ namespace storm {
                         std::vector<std::shared_ptr<SmtConstraint>> depFailed;
                         for (auto const &dependency : element->outgoingDependencies()) {
                             for (auto const &depElement : dependency->dependentEvents()) {
-                                depFailed.push_back(std::make_shared<IsLessEqualConstant>(timePointVariables.at(depElement->id()), i));
+                                depFailed.push_back(
+                                        std::make_shared<IsLessEqualConstant>(timePointVariables.at(depElement->id()),
+                                                                              i));
                             }
                         }
-                        markovianC[i].push_back(std::make_shared<Implies>(triggerFailed, std::make_shared<And>(depFailed)));
+                        markovianC[i].push_back(
+                                std::make_shared<Implies>(triggerFailed, std::make_shared<And>(depFailed)));
                     }
                 }
             }
             for (uint64_t i = 0; i < nrMarkovian; ++i) {
-                constraints.push_back(std::make_shared<Iff>(std::make_shared<IsBoolValue>(markovianVariables.at(i), true), std::make_shared<And>(markovianC[i])));
-                constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed.");
+                constraints.push_back(
+                        std::make_shared<Iff>(std::make_shared<IsBoolValue>(markovianVariables.at(i), true),
+                                              std::make_shared<And>(markovianC[i])));
+                constraints.back()->setDescription("Markovian (" + std::to_string(i) +
+                                                   ") iff all dependent events which trigger failed also failed.");
             }
 
             // In non-Markovian steps the next failed element is a dependent BE (constraint 10) + additions to specification in paper
@@ -366,9 +387,11 @@ namespace storm {
                                     timePointVariables.at(j), i + 1);
                             std::vector<std::shared_ptr<SmtConstraint>> triggerFailed;
                             for (auto const &dependency : be->ingoingDependencies()) {
-                                triggerFailed.push_back(std::make_shared<IsLessEqualConstant>(timePointVariables.at(dependency->triggerEvent()->id()), i));
+                                triggerFailed.push_back(std::make_shared<IsLessEqualConstant>(
+                                        timePointVariables.at(dependency->triggerEvent()->id()), i));
                             }
-                            nonMarkovianC[i].push_back(std::make_shared<Implies>(nextFailure, std::make_shared<Or>(triggerFailed)));
+                            nonMarkovianC[i].push_back(
+                                    std::make_shared<Implies>(nextFailure, std::make_shared<Or>(triggerFailed)));
                         }
                     }
                 }
@@ -382,8 +405,11 @@ namespace storm {
                 }
                 // Add Constraint that any DEPENDENT event has to fail next
                 nonMarkovianC[i].push_back(std::make_shared<Or>(dependentConstr));
-                constraints.push_back(std::make_shared<Implies>(std::make_shared<IsBoolValue>(markovianVariables.at(i), false), std::make_shared<And>(nonMarkovianC[i])));
-                constraints.back()->setDescription("Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE.");
+                constraints.push_back(
+                        std::make_shared<Implies>(std::make_shared<IsBoolValue>(markovianVariables.at(i), false),
+                                                  std::make_shared<And>(nonMarkovianC[i])));
+                constraints.back()->setDescription(
+                        "Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE.");
             }
 
             // In Markovian steps the failure rate is positive (constraint 11)
@@ -402,7 +428,9 @@ namespace storm {
                 }
             }
             for (uint64_t i = 0; i < nrMarkovian; ++i) {
-                constraints.push_back(std::make_shared<Implies>(std::make_shared<IsBoolValue>(markovianVariables.at(i), true), std::make_shared<And>(notColdC[i])));
+                constraints.push_back(
+                        std::make_shared<Implies>(std::make_shared<IsBoolValue>(markovianVariables.at(i), true),
+                                                  std::make_shared<And>(notColdC[i])));
                 constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") -> positive failure rate.");
             }
 
@@ -424,6 +452,12 @@ namespace storm {
             for (auto const &markovianVarEntry : markovianVariables) {
                 stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl;
             }
+            if (!dependencyVariables.empty()) {
+                stream << "; Dependency variables" << std::endl;
+                for (auto const &depVar : dependencyVariables) {
+                    stream << "(declare-fun " << varNames[depVar.second] << "() Int)" << std::endl;
+                }
+            }
             if (!tmpTimePointVariables.empty()) {
                 stream << "; Temporary variables" << std::endl;
                 for (auto const &tmpVar : tmpTimePointVariables) {
@@ -462,6 +496,11 @@ namespace storm {
                     manager->declareIntegerVariable(varNames[tmpVar]);
                 }
             }
+            if (!dependencyVariables.empty()) {
+                for (auto const &depVar : dependencyVariables) {
+                    manager->declareIntegerVariable(varNames[depVar]);
+                }
+            }
             // Add constraints to solver
             for (auto const &constraint : constraints) {
                 solver->add(constraint->toExpression(varNames, manager));
@@ -475,10 +514,10 @@ namespace storm {
             // Set backtracking marker to check several properties without reconstructing DFT encoding
             solver->push();
             // Constraint that toplevel element can fail with less or equal 'bound' failures
-            std::shared_ptr<SmtConstraint> tleNeverFailedConstr = std::make_shared<IsConstantValue>(
+            std::shared_ptr<SmtConstraint> tleFailedConstr = std::make_shared<IsConstantValue>(
                     timePointVariables.at(dft.getTopLevelIndex()), bound);
             std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
-            solver->add(tleNeverFailedConstr->toExpression(varNames, manager));
+            solver->add(tleFailedConstr->toExpression(varNames, manager));
             storm::solver::SmtSolver::CheckResult res = solver->check();
             solver->pop();
             return res;
@@ -525,7 +564,7 @@ namespace storm {
             }
             // Set backtracking marker to check several properties without reconstructing DFT encoding
             solver->push();
-            // Constraint that toplevel element can fail with less or equal 'bound' failures
+            // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited
             std::shared_ptr<SmtConstraint> countConstr = std::make_shared<BoolCountIsLessConstant>(
                     markovianIndices, checkNumber);
             std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
@@ -535,6 +574,30 @@ namespace storm {
             return res;
         }
 
+        storm::solver::SmtSolver::CheckResult
+        DFTASFChecker::checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint) {
+            STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
+            std::vector<uint64_t> markovianIndices;
+            // Get Markovian variable indices
+            for (uint64_t i = 0; i < timepoint; ++i) {
+                markovianIndices.push_back(markovianVariables.at(i));
+            }
+            // Set backtracking marker to check several properties without reconstructing DFT encoding
+            solver->push();
+            // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited
+            std::shared_ptr<SmtConstraint> countConstr = std::make_shared<BoolCountIsConstantValue>(
+                    markovianIndices, timepoint);
+            // Constraint that TLE fails at timepoint
+            std::shared_ptr<SmtConstraint> timepointConstr = std::make_shared<IsConstantValue>(
+                    timePointVariables.at(dft.getTopLevelIndex()), timepoint);
+            std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
+            solver->add(countConstr->toExpression(varNames, manager));
+            solver->add(timepointConstr->toExpression(varNames, manager));
+            storm::solver::SmtSolver::CheckResult res = solver->check();
+            solver->pop();
+            return res;
+        }
+
         uint64_t DFTASFChecker::correctLowerBound(uint64_t bound, uint_fast64_t timeout) {
             STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
             STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound));
@@ -547,13 +610,40 @@ namespace storm {
                         STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(bound));
                         return bound;
                     case storm::solver::SmtSolver::CheckResult::Unknown:
-                        STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to ");
+                        STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to "
+                                                << std::to_string(bound));
+                        return bound;
+                    default:
+                        --bound;
+                        break;
+                }
+            }
+            return bound;
+        }
+
+        uint64_t DFTASFChecker::correctUpperBound(uint64_t bound, uint_fast64_t timeout) {
+            STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
+            STORM_LOG_DEBUG("Upper bound correction - try to correct bound " << std::to_string(bound));
+
+            while (bound > 1) {
+                setSolverTimeout(timeout * 1000);
+                storm::solver::SmtSolver::CheckResult tmp_res =
+                        checkFailsAtTimepointWithOnlyMarkovianState(bound);
+                unsetSolverTimeout();
+                switch (tmp_res) {
+                    case storm::solver::SmtSolver::CheckResult::Sat:
+                        STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(bound));
+                        return bound;
+                    case storm::solver::SmtSolver::CheckResult::Unknown:
+                        STORM_LOG_DEBUG("Upper bound correction - Solver returned 'Unknown', corrected to ");
                         return bound;
                     default:
                         --bound;
                         break;
+
                 }
             }
+            STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(bound));
             return bound;
         }
 
@@ -567,7 +657,7 @@ namespace storm {
                 unsetSolverTimeout();
                 switch (tmp_res) {
                     case storm::solver::SmtSolver::CheckResult::Sat:
-                        if (dft.getDependencies().size() > 0) {
+                        if (!dft.getDependencies().empty()) {
                             return correctLowerBound(bound, timeout);
                         } else {
                             return bound;
@@ -597,7 +687,11 @@ namespace storm {
                 unsetSolverTimeout();
                 switch (tmp_res) {
                     case storm::solver::SmtSolver::CheckResult::Sat:
+                        if (!dft.getDependencies().empty()) {
+                            return correctUpperBound(bound, timeout);
+                        } else {
                             return bound;
+                        }
                     case storm::solver::SmtSolver::CheckResult::Unknown:
                         STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'");
                         return bound;

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

@@ -25,6 +25,20 @@ namespace storm {
             uint64_t childIndex;
         };
 
+        class DependencyPair {
+        public:
+            DependencyPair(uint64_t depIndex, uint64_t childIndex) : depIndex(depIndex), childIndex(childIndex) {
+            }
+
+            friend bool operator<(DependencyPair const &p1, DependencyPair const &p2) {
+                return p1.depIndex < p2.depIndex || (p1.depIndex == p2.depIndex && p1.childIndex < p2.childIndex);
+            }
+
+        private:
+            uint64_t depIndex;
+            uint64_t childIndex;
+        };
+
 
         class DFTASFChecker {
             using ValueType = double;
@@ -104,15 +118,33 @@ namespace storm {
              */
             storm::solver::SmtSolver::CheckResult checkFailsWithLessThanMarkovianState(uint64_t checkNumber);
 
+            /**
+             * Helper function that checks if the DFT can fail at a timepoint while visiting less than a given number of Markovian states
+             *
+             * @param timepoint point in time to check
+             * @return "Sat" if a sequence of BE failures exists such that less than checkNumber Markovian states are visited,
+             * "Unsat" if it does not, otherwise "Unknown"
+             */
+            storm::solver::SmtSolver::CheckResult checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint);
+
             /**
              * Helper function for correction of least failure bound when dependencies are present
              *
              * @param bound known lower bound to be corrected
              * @param timeout timeout timeout for each query in seconds
-             * @return the corrected bound, 1 if correction cannot be completed
+             * @return the corrected bound
              */
             uint64_t correctLowerBound(uint64_t bound, uint_fast64_t timeout);
 
+            /**
+             * Helper function for correction of bound for number of BEs such that the DFT always fails when dependencies are present
+             *
+             * @param bound known bound to be corrected
+             * @param timeout timeout timeout for each query in seconds
+             * @return the corrected bound
+             */
+            uint64_t correctUpperBound(uint64_t bound, uint_fast64_t timeout);
+
             uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
 
             /**
@@ -176,6 +208,13 @@ namespace storm {
             void generateSpareConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                                          std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
 
+            /**
+             * Add constraints encoding PDEP gates.
+             * This corresponds to constraint (4)
+             */
+            void generatePdepConstraint(std::vector<uint64_t> childVarIndices,
+                                        std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
+
             /**
             * Add constraints encoding claiming rules.
             * This corresponds to constraint (8) and addition
@@ -194,6 +233,7 @@ namespace storm {
             std::unordered_map<uint64_t, uint64_t> timePointVariables;
             std::vector<std::shared_ptr<SmtConstraint>> constraints;
             std::map<SpareAndChildPair, uint64_t> claimVariables;
+            std::map<DependencyPair, uint64_t> dependencyVariables;
             std::unordered_map<uint64_t, uint64_t> markovianVariables;
             std::vector<uint64_t> tmpTimePointVariables;
             uint64_t notFailed;

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

@@ -630,6 +630,39 @@ namespace storm {
             std::vector<uint64_t> varIndices;
             uint64_t value;
         };
+
+        class BoolCountIsConstantValue : public SmtConstraint {
+        public:
+            BoolCountIsConstantValue(std::vector<uint64_t> varIndices, uint64_t val) : varIndices(varIndices),
+                                                                                       value(val) {
+            }
+
+            std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
+                std::stringstream sstr;
+                sstr << "(= (+ ";
+                for (uint64_t i = 0; i < varIndices.size(); ++i) {
+                    sstr << "(ite " << varNames.at(varIndices.at(i)) << " 1 0 )";
+                }
+                sstr << ") " << value << " )";
+                return sstr.str();
+            }
+
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                std::vector<storm::expressions::Expression> boolToInt;
+                for (uint64_t i = 0; i < varIndices.size(); ++i) {
+                    boolToInt.push_back(
+                            ite(manager->getVariableExpression(varNames.at(varIndices.at(i))), // If variable is true
+                                manager->integer(1), // set 1
+                                manager->integer(0))); // else 0
+                }
+                return sum(boolToInt) == manager->integer(value);
+            }
+
+        private:
+            std::vector<uint64_t> varIndices;
+            uint64_t value;
+        };
     }
 }