Better comments for SMT generation

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

@@ -271,7 +271,8 @@ namespace storm {
 
         void DFTASFChecker::convert() {
             std::vector<uint64_t> beVariables;
-            // Convert all elements
+
+            // Initialize variables
             for (size_t i = 0; i < dft.nrElements(); ++i) {
                 std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
                 varNames.push_back("t_" + element->name());
@@ -294,21 +295,28 @@ namespace storm {
                 }
             }
 
-            // BE
+
+            // Generate constraints
+
+            // No two BEs fail at the same time (first part of constraint 12)
             constraints.push_back(std::make_shared<PairwiseDifferent>(beVariables));
             constraints.back()->setDescription("No two BEs fail at the same time");
+
+            // All BEs have to fail (second part of constraint 12)
             for (auto const& beV : beVariables) {
                 constraints.push_back(std::make_shared<BetweenValues>(beV, 1, dft.nrBasicElements()));
             }
 
-            // Claim variables
-            for (auto const& csvV : claimVariables) {
-                constraints.push_back(std::make_shared<BetweenValues>(csvV.second, 0, dft.nrBasicElements() + 1));
+
+            // Initialize claim variables in [1, |BE|+1]
+            for (auto const& claimVariable : claimVariables) {
+                constraints.push_back(std::make_shared<BetweenValues>(claimVariable.second, 0, dft.nrBasicElements() + 1));
             }
 
+            // First child of each spare is claimed in the beginning
             for (size_t i = 0; i < dft.nrElements(); ++i) {
                 std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
-                if(element->isSpareGate()) {
+                if (element->isSpareGate()) {
                     auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
                     auto const& spareChild = spare->children().front();
                     constraints.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(spare->id(), spareChild->id()), 0));
@@ -317,7 +325,9 @@ namespace storm {
                 }
             }
 
+            // Encoding for specific gates
             for (size_t i = 0; i < dft.nrElements(); ++i) {
+                // Get indices for gate children
                 std::vector<uint64_t> childVarIndices;
                 if (dft.isGate(i)) {
                     std::shared_ptr<storm::storage::DFTGate<ValueType> const> gate = dft.getGate(i);
@@ -328,25 +338,39 @@ namespace storm {
 
                 std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
                 switch (element->type()) {
+                    case storm::storage::DFTElementType::BE:
+                        // BEs were already considered before
+                        break;
                     case storm::storage::DFTElementType::AND:
+                        // Constraint for AND gate (constraint 1)
                         constraints.push_back(std::make_shared<IsMaximum>(timePointVariables.at(i), childVarIndices));
                         constraints.back()->setDescription("And gate");
                         break;
                     case storm::storage::DFTElementType::OR:
+                        // Constraint for OR gate (constraint 2)
                         constraints.push_back(std::make_shared<IsMinimum>(timePointVariables.at(i), childVarIndices));
                         constraints.back()->setDescription("Or gate");
                         break;
                     case storm::storage::DFTElementType::PAND:
-                        constraints.push_back(std::make_shared<IfThenElse>(std::make_shared<Sorted>(childVarIndices), std::make_shared<IsEqual>(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())), std::make_shared<IsConstantValue>(timePointVariables.at(i), dft.nrBasicElements()+1)));
+                    {
+
+                        // Constraint for PAND gate (constraint 3)
+                        std::shared_ptr<DFTConstraint> ifC = std::make_shared<Sorted>(childVarIndices);
+                        std::shared_ptr<DFTConstraint> thenC = std::make_shared<IsEqual>(timePointVariables.at(i), timePointVariables.at(childVarIndices.back()));
+                        std::shared_ptr<DFTConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i), dft.nrBasicElements()+1);
+                        constraints.push_back(std::make_shared<IfThenElse>(ifC, thenC, elseC));
                         constraints.back()->setDescription("Pand gate");
+                    }
                     case storm::storage::DFTElementType::SPARE:
                     {
                         auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
                         auto const& children = spare->children();
-
-                        constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLEqual>(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()), std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.back())));
+                        // If last child is claimed before failure the spare fails when the last child fails (constraint 5)
+                        std::shared_ptr<DFTConstraint> leftC = std::make_shared<IsLEqual>(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back());
+                        constraints.push_back(std::make_shared<Iff>(leftC, std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.back())));
                         constraints.back()->setDescription("Last child & claimed -> spare fails");
 
+                        // Construct constraint for claiming
                         std::shared_ptr<DFTConstraint> elseCase = nullptr;
                         for (uint64_t j = 0; j < children.size(); ++j) {
                             uint64_t currChild = children.size() - 2 - j;
@@ -354,22 +378,35 @@ namespace storm {
                             uint64_t xv = childVarIndices.at(currChild); // if v is the child, xv is the time x fails.
                             uint64_t csn = getClaimVariableIndex(spare->id(), childVarIndices.at(currChild+1)); // csn is the moment the spare claims the next child
                             uint64_t xn = childVarIndices.at(currChild+1); // xn is the moment the next child fails
+
+                            // Generate constraint for trying to claim next child
                             if (j == 0) {
+                                // Last child: spare fails at same point as xv (otherwise case in constraint 7)
                                 elseCase = std::make_shared<IsEqual>(timePointVariables.at(i), xv);
                             }
+                            // Next child is not yet failed
                             ifcs.push_back(std::make_shared<IsLEqual>(xv, xn));
+
+                            // Child is not yet claimed by a different spare (first part of case distinction for constraint 7)
                             for (auto const& otherSpare : children.at(currChild+1)->parents()) {
-                                if (otherSpare->id() == i) { continue; }// not a OTHER spare.
+                                if (otherSpare->id() == i) {
+                                    // not an OTHER spare.
+                                    continue;
+                                }
                                 ifcs.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(otherSpare->id(), children.at(currChild+1)->id()), dft.nrBasicElements()+1));
                             }
-                            std::shared_ptr<DFTConstraint> ite = std::make_shared<IfThenElse>(std::make_shared<And>(ifcs), std::make_shared<IsEqual>(csn, xv), elseCase);
-                            elseCase = ite;
-                            constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLEqual>(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), ite));
+                            // Claim next child (constraint 7)
+                            // elseCase contains the constraints for the recursive call to phi^s_{i+1}
+                            std::shared_ptr<DFTConstraint> tryClaimC = std::make_shared<IfThenElse>(std::make_shared<And>(ifcs), std::make_shared<IsEqual>(csn, xv), elseCase);
+                            elseCase = tryClaimC;
+                            // If i-th child fails after being claimed, then try to claim (i+1)-th child (constraint 6)
+                            constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLEqual>(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), tryClaimC));
                             constraints.back()->setDescription(std::to_string(j+1) + " but last child & claimed");
                         }
                         break;
                     }
                     default:
+                        STORM_LOG_WARN("DFT element of type '" << element->type() << "' is ignored for SMT encoding.");
                         break;
                 }
             }