smt checker v1, and better error messages

Former-commit-id: ab7391e85d

DFTASFChecker.cpp

@@ -0,0 +1,9 @@
+//
+//  DFTASFChecker.cpp
+//  storm
+//
+//  Created by Sebastian Junges on 27/10/16.
+//
+//
+
+#include "DFTASFChecker.hpp"

DFTASFChecker.hpp

@@ -0,0 +1,14 @@
+//
+//  DFTASFChecker.hpp
+//  storm
+//
+//  Created by Sebastian Junges on 27/10/16.
+//
+//
+
+#ifndef DFTASFChecker_hpp
+#define DFTASFChecker_hpp
+
+#include <stdio.h>
+
+#endif /* DFTASFChecker_hpp */

src/modelchecker/dft/DFTASFChecker.cpp

@@ -0,0 +1,413 @@
+#include "DFTASFChecker.h"
+#include <string>
+
+namespace storm {
+    
+    namespace modelchecker {
+        
+        /*
+         *  Variable[VarIndex] is the maximum of the others
+         */
+        class IsMaximum : public DFTConstraint {
+        public:
+            IsMaximum(uint64_t varIndex, std::vector<uint64_t> const& varIndices) : varIndex(varIndex), varIndices(varIndices) {
+                
+            }
+            
+            virtual ~IsMaximum() {
+                
+            }
+            
+            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                std::stringstream sstr;
+                sstr << "(and ";
+                // assert it is largereq than all values.
+                for (auto const& ovi : varIndices) {
+                    sstr << "(>= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
+                }
+                // assert it is one of the values.
+                sstr << "(or ";
+                for (auto const& ovi : varIndices) {
+                    sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
+                }
+                sstr << ")"; // end of the or
+                sstr << ")"; // end outer and.
+                return sstr.str();
+                
+            }
+                
+                
+            private:
+                uint64_t varIndex;
+                std::vector<uint64_t> varIndices;
+                };
+                /*
+                 *  First is the minimum of the others
+                 */
+                class IsMinimum : public DFTConstraint {
+                public:
+                    IsMinimum(uint64_t varIndex, std::vector<uint64_t> const& varIndices) : varIndex(varIndex), varIndices(varIndices) {
+                        
+                    }
+                    
+                    
+                    virtual ~IsMinimum() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        sstr << "(and ";
+                        // assert it is smallereq than all values.
+                        for (auto const& ovi : varIndices) {
+                            sstr << "(<= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
+                        }
+                        // assert it is one of the values.
+                        sstr << "(or ";
+                        for (auto const& ovi : varIndices) {
+                            sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") ";
+                        }
+                        sstr << ")"; // end of the or
+                        sstr << ")"; // end outer and.
+                        return sstr.str();
+                        
+                    }
+                    
+                    
+                private:
+                    uint64_t varIndex;
+                    std::vector<uint64_t> varIndices;
+                };
+                
+                class BetweenValues : public DFTConstraint {
+                public:
+                    BetweenValues(uint64_t varIndex, uint64_t lower, uint64_t upper) : varIndex(varIndex), upperBound(upper) , lowerBound(lower) {
+                        
+                    }
+                    virtual ~BetweenValues() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        sstr << "(and ";
+                        sstr << "(>= " << varNames.at(varIndex) << " " << lowerBound << ")";
+                        sstr << "(<= " << varNames.at(varIndex) << " " << upperBound << ")";
+                        sstr << ")";
+                        return sstr.str();
+                    }
+                    
+                private:
+                    uint64_t varIndex;
+                    uint64_t upperBound;
+                    uint64_t lowerBound;
+                };
+                
+                class And : public DFTConstraint {
+                public:
+                    And(std::vector<std::shared_ptr<DFTConstraint>> const& constraints) : constraints(constraints) {}
+                    
+                    virtual ~And() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        sstr << "(and";
+                        for(auto const& c : constraints) {
+                            sstr << " " << c->toSmtlib2(varNames);
+                        }
+                        sstr << ")";
+                        return sstr.str();
+                    }
+                private:
+                    std::vector<std::shared_ptr<DFTConstraint>> constraints;
+                    
+                };
+                
+                class Iff : public DFTConstraint {
+                public:
+                    Iff(std::shared_ptr<DFTConstraint> l, std::shared_ptr<DFTConstraint> r) : lhs(l), rhs(r) {
+                        
+                    }
+                    
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        sstr << "(= " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")";
+                        return sstr.str();
+                    }
+                    
+                private:
+                    std::shared_ptr<DFTConstraint> lhs;
+                    std::shared_ptr<DFTConstraint> rhs;
+                };
+                
+                class IsConstantValue : public DFTConstraint {
+                public:
+                    IsConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) {
+                        
+                    }
+                    
+                    virtual ~IsConstantValue() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        assert(varIndex < varNames.size());
+                        sstr << "(= " << varNames.at(varIndex) << " " << value << ")";
+                        return sstr.str();
+                    }
+                    
+                private:
+                    uint64_t varIndex;
+                    uint64_t value;
+                };
+                
+                class IsEqual : public DFTConstraint {
+                public:
+                    IsEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) {
+                        
+                    }
+                    
+                    virtual ~IsEqual() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        return "(= " + varNames.at(var1Index) + " " +  varNames.at(var2Index) + " )";
+                    }
+                    
+                private:
+                    uint64_t var1Index;
+                    uint64_t var2Index;
+                };
+                
+                class IsLEqual : public DFTConstraint {
+                public:
+                    IsLEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) {
+                        
+                    }
+                    
+                    virtual ~IsLEqual() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        return "(<= " + varNames.at(var1Index) + " " +  varNames.at(var2Index) + " )";
+                    }
+                    
+                private:
+                    uint64_t var1Index;
+                    uint64_t var2Index;
+                };
+                
+                class PairwiseDifferent : public DFTConstraint {
+                public:
+                    PairwiseDifferent(std::vector<uint64_t> const& indices) : varIndices(indices) {
+                        
+                    }
+                    virtual ~PairwiseDifferent() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        sstr << "(distinct";
+                        //                for(uint64_t i = 0; i < varIndices.size(); ++i) {
+                        //                    for(uint64_t j = i + 1; j < varIndices.size(); ++j) {
+                        //                        sstr << "()";
+                        //                    }
+                        //                }
+                        for (auto const& varIndex : varIndices) {
+                            sstr << " " << varNames.at(varIndex);
+                        }
+                        sstr << ")";
+                        return sstr.str();
+                    }
+                    
+                private:
+                    std::vector<uint64_t> varIndices;
+                };
+                
+                class Sorted : public DFTConstraint {
+                public:
+                    Sorted(std::vector<uint64_t> varIndices) : varIndices(varIndices) {
+                        
+                    }
+                    
+                    virtual ~Sorted() {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        sstr << "(and ";
+                        for(uint64_t i = 1; i < varIndices.size(); ++i) {
+                            sstr << "(<= " << varNames.at(varIndices.at(i-1)) << " " << varNames.at(varIndices.at(i)) << ")";
+                        }
+                        sstr << ") ";
+                        return sstr.str();
+                    }
+                    
+                    
+                private:
+                    std::vector<uint64_t> varIndices;
+                };
+                
+                class IfThenElse : public DFTConstraint {
+                public:
+                    IfThenElse(std::shared_ptr<DFTConstraint> ifC, std::shared_ptr<DFTConstraint> thenC, std::shared_ptr<DFTConstraint> elseC) : ifConstraint(ifC), thenConstraint(thenC), elseConstraint(elseC) {
+                        
+                    }
+                    
+                    std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                        std::stringstream sstr;
+                        sstr << "(ite " << ifConstraint->toSmtlib2(varNames) << " " << thenConstraint->toSmtlib2(varNames) << " " << elseConstraint->toSmtlib2(varNames) << ")";
+                        return sstr.str();
+                    }
+                    
+                private:
+                    std::shared_ptr<DFTConstraint> ifConstraint;
+                    std::shared_ptr<DFTConstraint> thenConstraint;
+                    std::shared_ptr<DFTConstraint> elseConstraint;
+                };
+                
+                
+                DFTASFChecker::DFTASFChecker(storm::storage::DFT<double> const& dft) : dft(dft) {
+                    // Intentionally left empty.
+                }
+                
+                uint64_t DFTASFChecker::getClaimVariableIndex(uint64_t spare, uint64_t child) const {
+                    return claimVariables.at(SpareAndChildPair(spare, child));
+                }
+                
+                void DFTASFChecker::convert() {
+                    
+                    std::vector<uint64_t> beVariables;
+                    // Convert all elements
+                    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());
+                        timePointVariables.emplace(i, varNames.size() - 1);
+                        switch (element->type()) {
+                            case storm::storage::DFTElementType::BE:
+                                beVariables.push_back(varNames.size() - 1);
+                                break;
+                            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);
+                                }
+                                break;
+                            }
+                            default:
+                                break;
+                        }
+                    }
+                    
+                    // BE
+                    constraints.push_back(std::make_shared<PairwiseDifferent>(beVariables));
+                    constraints.back()->setDescription("No two BEs fail at the same time");
+                    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));
+                    }
+                    
+                    for (size_t i = 0; i < dft.nrElements(); ++i) {
+                        std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
+                        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));
+                            constraints.back()->setDescription("Spare " + spare->name() + " claims first child");
+                            
+                        }
+                    }
+                    
+                    
+                    for (size_t i = 0; i < dft.nrElements(); ++i) {
+                        std::vector<uint64_t> childVarIndices;
+                        if (dft.isGate(i)) {
+                            std::shared_ptr<storm::storage::DFTGate<ValueType> const> gate = dft.getGate(i);
+                            for (auto const& child : gate->children()) {
+                                childVarIndices.push_back(timePointVariables.at(child->id()));
+                            }
+                        }
+                        
+                        std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
+                        switch (element->type()) {
+                            case storm::storage::DFTElementType::AND:
+                                constraints.push_back(std::make_shared<IsMaximum>(timePointVariables.at(i), childVarIndices));
+                                constraints.back()->setDescription("And gate");
+                                break;
+                            case storm::storage::DFTElementType::OR:
+                                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)));
+                                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())));
+                                constraints.back()->setDescription("Last child & claimed -> spare fails");
+                                std::vector<std::shared_ptr<DFTConstraint>> ifcs;
+                                uint64_t xv = childVarIndices.at(childVarIndices.size()-2); // if v is the child, xv is the time x fails.
+                                uint64_t csn = getClaimVariableIndex(spare->id(), children.back()->id()); // csn is the moment the spare claims the next child
+                                uint64_t xn = childVarIndices.back(); // xn is the moment the next child fails
+                                ifcs.push_back(std::make_shared<IsLEqual>(xv, xn));
+                                for(auto const& otherSpare : children.back()->parents()) {
+                                    if(otherSpare->id() == i) { continue; }// not a OTHER spare.
+                                    ifcs.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(otherSpare->id(), children.back()->id()), dft.nrBasicElements()+1));
+                                }
+                                std::shared_ptr<DFTConstraint> ite = std::make_shared<IfThenElse>(std::make_shared<And>(ifcs), std::make_shared<IsEqual>(csn, xv), std::make_shared<IsEqual>(timePointVariables.at(i),  xv));
+                                constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLEqual>(getClaimVariableIndex(spare->id(), children.at(children.size()-2)->id()), xv), ite));
+                                constraints.back()->setDescription("1 but last child & claimed");
+                                
+                                for( uint64_t j = 0; j < children.size() - 2; ++j) {
+                                    uint64_t currChild = children.size() - 1 - j;
+                                    
+                                }
+                                break;
+                            }
+                            default:
+                                break;
+                        }
+                    }
+                    
+                    constraints.push_back(std::make_shared<IsConstantValue>(dft.getTopLevelIndex(), dft.nrBasicElements()+1));
+                }
+                
+                void DFTASFChecker::toFile(std::string const& filename) {
+                    std::ofstream ofs;
+                    std::cout << "Writing to " << filename << std::endl;
+                    ofs.open(filename);
+                    ofs << "; time point variables" << std::endl;
+                    for (auto const& timeVarEntry : timePointVariables) {
+                        ofs << "(declare-fun " << varNames[timeVarEntry.second] << "()  Int)" << std::endl;
+                    }
+                    ofs << "; claim variables" << std::endl;
+                    for (auto const& claimVarEntry : claimVariables) {
+                        ofs << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl;
+                    }
+                    for (auto const& constraint : constraints) {
+                        ofs << "; " << constraint->description() << std::endl;
+                        ofs << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl;
+                    }
+                    ofs << "(check-sat)" << std::endl;
+                    ofs.close();
+                    
+                }
+    }
+}

src/modelchecker/dft/DFTASFChecker.h

@@ -0,0 +1,61 @@
+#pragma once
+
+#include <string>
+#include <vector>
+#include <unordered_map>
+#include "src/storage/dft/DFT.h"
+
+
+namespace storm {
+    namespace modelchecker {
+        class DFTConstraint {
+        public:
+            virtual ~DFTConstraint() {
+                
+            }
+            
+            virtual  std::string toSmtlib2(std::vector<std::string> const& varNames) const = 0;
+            virtual std::string description() const { return descript; }
+
+            void setDescription(std::string const& descr) {
+                descript = descr;
+            }
+            
+        private:
+            std::string descript;
+        };
+        
+        class SpareAndChildPair {
+            
+        public:
+            SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) {
+                
+            }
+            
+            uint64_t spareIndex;
+            uint64_t childIndex;
+        };
+        
+        bool operator<(SpareAndChildPair const& p1, SpareAndChildPair const& p2) {
+            return p1.spareIndex < p2.spareIndex || (p1.spareIndex == p2.spareIndex && p1.childIndex < p2.childIndex);
+        }
+        
+        class DFTASFChecker {
+            using ValueType = double;
+            
+        public:
+            DFTASFChecker(storm::storage::DFT<ValueType> const&);
+            void convert();
+            void toFile(std::string const&);
+            
+        private:
+            uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
+            
+            storm::storage::DFT<ValueType> const& dft;
+            std::vector<std::string> varNames;
+            std::unordered_map<uint64_t, uint64_t> timePointVariables;
+            std::vector<std::shared_ptr<DFTConstraint>> constraints;
+            std::map<SpareAndChildPair, uint64_t> claimVariables;
+        };
+    }
+}

src/storage/dft/DFTBuilder.cpp

@@ -32,7 +32,7 @@ namespace storm {
                         // Child not found -> find first dependent event to assure that child is dependency
                         // TODO: Not sure whether this is the intended behaviour?
                         auto itFind = mElements.find(child + "_1");
-                        STORM_LOG_ASSERT(itFind != mElements.end(), "Child not found.");
+                        STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << child << "' for gate '" << gate->name() << "' not found.");
                         STORM_LOG_ASSERT(itFind->second->isDependency(), "Child is no dependency.");
                         STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name());
                     }

src/storage/dft/DFTState.cpp

@@ -319,7 +319,7 @@ namespace storm {
                         mCurrentlyFailableBE.push_back(elem);
                         // Remove from not failable BEs
                         auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem);
-                        STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element not found.");
+                        STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << mDft.getElement(elem)->name() << " not found.");
                         mCurrentlyNotFailableBE.erase(it);
                     }
                 } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {

src/storm-dyftee.cpp

@@ -3,6 +3,8 @@
 #include "src/utility/storm.h"
 #include "src/parser/DFTGalileoParser.h"
 #include "src/modelchecker/dft/DFTModelChecker.h"
+
+#include "src/modelchecker/dft/DFTASFChecker.h"
 #include "src/cli/cli.h"
 #include "src/exceptions/BaseException.h"
 #include "src/utility/macros.h"
@@ -58,10 +60,11 @@ void analyzeWithSMT(std::string filename) {
     
     storm::parser::DFTGalileoParser<ValueType> parser;
     storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
-    storm::builder::DFTSMTBuilder<ValueType> dftSmtBuilder;
-    dftSmtBuilder.convertToSMT(dft);
-    bool sat = dftSmtBuilder.check();
-    std::cout << "SMT result: " << sat << std::endl;
+    storm::modelchecker::DFTASFChecker asfChecker(dft);
+    asfChecker.convert();
+    asfChecker.toFile("test.smt2");
+    //bool sat = dftSmtBuilder.check();
+    //std::cout << "SMT result: " << sat << std::endl;
 }
 
 /*!
@@ -120,7 +123,7 @@ int main(const int argc, const char** argv) {
         if (dftSettings.solveWithSMT()) {
             // Solve with SMT
             if (parametric) {
-                analyzeWithSMT<storm::RationalFunction>(dftSettings.getDftFilename());
+            //    analyzeWithSMT<storm::RationalFunction>(dftSettings.getDftFilename());
             } else {
                 analyzeWithSMT<double>(dftSettings.getDftFilename());
             }