Started with SMT encoding for DFTs

Former-commit-id: a2a68cee6a

src/builder/DftSmtBuilder.cpp

@@ -0,0 +1,120 @@
+#include "src/builder/DFTSMTBuilder.h"
+#include "src/exceptions/NotImplementedException.h"
+
+namespace storm {
+    namespace builder {
+
+        template <typename ValueType>
+        DFTSMTBuilder<ValueType>::DFTSMTBuilder() : manager(std::make_shared<storm::expressions::ExpressionManager>()) {
+            solver = storm::utility::solver::SmtSolverFactory().create(*manager);
+        }
+
+        template <typename ValueType>
+        void DFTSMTBuilder<ValueType>::convertToSMT(storm::storage::DFT<ValueType> const& dft) {
+            std::cout << "Convert DFT to SMT" << std::endl;
+            timeMax = manager->integer(dft.nrBasicElements());
+            timeFailSafe = manager->integer(dft.nrBasicElements() + 1);
+            timeZero = manager->integer(0);
+            
+            // Convert all elements
+            for (size_t i = 0; i < dft.nrElements(); ++i) {
+                std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
+                std::cout << "Consider " << element->toString() << std::endl;
+                if (element->isBasicElement()) {
+                    storm::expressions::Variable varBE = convert(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(element));
+                    varsBE.push_back(varBE);
+                } else if (element->isGate()) {
+                    storm::expressions::Variable varGate = convert(std::static_pointer_cast<storm::storage::DFTGate<ValueType> const>(element));
+                    if (dft.getTopLevelIndex() == i) {
+                        topLevel = varGate;
+                    }
+                } else if (element->isDependency()) {
+                    convert(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(element));
+                } else if (element->isRestriction()) {
+                    convert(std::static_pointer_cast<storm::storage::DFTRestriction<ValueType> const>(element));
+                }
+            }
+            
+            // No simultaneous fails can occur
+            for (size_t i = 0; i < varsBE.size() - 1; ++i) {
+                storm::expressions::Expression be = varsBE[i];
+                for (size_t j = i + 1; j < varsBE.size(); ++j) {
+                    storm::expressions::Expression assertion = be != varsBE[j];
+                    solver->add(assertion);
+                }
+            }
+            
+            // For every time-point one BE must fail
+            for (size_t time = 1; time <= dft.nrBasicElements(); ++time) {
+                storm::expressions::Expression exprTime = manager->integer(time);
+                storm::expressions::Expression assertion = varsBE[0] == exprTime;
+                for (size_t i = 1; i < varsBE.size(); ++i) {
+                    assertion = assertion || varsBE[i] == exprTime;
+                }
+                assertion = assertion || topLevel <= exprTime;
+                solver->add(assertion);
+            }
+            
+        }
+        
+        template <typename ValueType>
+        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTBE<ValueType> const> const& be) {
+            storm::expressions::Variable var = manager->declareIntegerVariable(be->name());
+            storm::expressions::Expression assertion = timeZero < var && var < timeFailSafe;
+            solver->add(assertion);
+            return var;
+        }
+        
+        template <typename ValueType>
+        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTGate<ValueType> const> const& gate) {
+            storm::expressions::Variable var = manager->declareIntegerVariable(gate->name());
+            storm::expressions::Expression assertion = timeZero < var && var <= timeFailSafe;
+            solver->add(assertion);
+            return var;
+        }
+        
+        template <typename ValueType>
+        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> const& dependency) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The dependency cannot be converted into SMT.");
+        }
+        
+        template <typename ValueType>
+        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTRestriction<ValueType> const> const& restriction) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The restriction cannot be converted into SMT.");
+        }
+
+        template <typename ValueType>
+        bool DFTSMTBuilder<ValueType>::check() const {
+            std::cout << "Check" << std::endl;
+            storm::solver::SmtSolver::CheckResult result = solver->check();
+            switch (result) {
+                case solver::SmtSolver::CheckResult::Sat:
+                {
+                    std::cout << "SAT with model:" << std::endl;
+                    std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel();
+                    for (auto const& pair : *manager) {
+                        std::cout << pair.first.getName() << "->" << model->getIntegerValue(pair.first) << std::endl;
+                    }
+                    return true;
+                }
+                case solver::SmtSolver::CheckResult::Unsat:
+                    return false;
+                case solver::SmtSolver::CheckResult::Unknown:
+                default:
+                    STORM_LOG_ASSERT(false, "Result is unknown.");
+                    return false;
+            }
+        }
+        
+
+        // Explicitly instantiate the class.
+        template class DFTSMTBuilder<double>;
+
+#ifdef STORM_HAVE_CARL
+        template class DFTSMTBuilder<storm::RationalFunction>;
+#endif
+
+    } // namespace builder
+} // namespace storm
+
+

src/builder/DftSmtBuilder.h

@@ -0,0 +1,49 @@
+#ifndef DFTSMTBUILDER_H
+#define	DFTSMTBUILDER_H
+
+#include "src/solver/SmtSolver.h"
+#include "src/utility/solver.h"
+#include "src/storage/dft/DFT.h"
+
+namespace storm {
+    namespace builder {
+
+        template<typename ValueType>
+        class DFTSMTBuilder {
+
+        public:
+            DFTSMTBuilder();
+            
+            void convertToSMT(storm::storage::DFT<ValueType> const& dft);
+            
+            bool check() const;
+
+        private:
+            
+            std::shared_ptr<storm::solver::SmtSolver> solver;
+            
+            std::shared_ptr<storm::expressions::ExpressionManager> manager;
+            
+            storm::expressions::Expression timeMax;
+            
+            storm::expressions::Expression timeFailSafe;
+            
+            storm::expressions::Expression timeZero;
+            
+            storm::expressions::Expression topLevel;
+            
+            std::vector<storm::expressions::Variable> varsBE;
+
+            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTBE<ValueType> const> const& be);
+
+            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTGate<ValueType> const> const& gate);
+            
+            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> const& dependency);
+            
+            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTRestriction<ValueType> const> const& restriction);
+
+        };
+    }
+}
+
+#endif	/* DFTSMTBUILDER_H */

src/settings/modules/DFTSettings.cpp

@@ -27,7 +27,10 @@ namespace storm {
             const std::string DFTSettings::propTimeBoundOptionName = "timebound";
             const std::string DFTSettings::minValueOptionName = "min";
             const std::string DFTSettings::maxValueOptionName = "max";
-
+#ifdef STORM_HAVE_Z3
+            const std::string DFTSettings::solveWithSmtOptionName = "smt";
+#endif
+            
             DFTSettings::DFTSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
@@ -39,6 +42,9 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
+#ifdef STORM_HAVE_Z3
+                this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
+#endif
             }
             
             bool DFTSettings::isDftFileSet() const {
@@ -85,6 +91,12 @@ namespace storm {
                 return this->getOption(maxValueOptionName).getHasOptionBeenSet();
             }
             
+#ifdef STORM_HAVE_Z3
+            bool DFTSettings::solveWithSMT() const {
+                return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
+            }
+#endif
+            
             void DFTSettings::finalize() {
                 
             }

src/settings/modules/DFTSettings.h

@@ -99,6 +99,15 @@ namespace storm {
                  */
                 double getPropTimebound() const;
                 
+#ifdef STORM_HAVE_Z3
+                /*!
+                 * Retrieves whether the DFT should be checked via SMT.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool solveWithSMT() const;
+#endif
+                
                 bool check() const override;
                 void finalize() override;
 
@@ -119,6 +128,9 @@ namespace storm {
                 static const std::string propTimeBoundOptionName;
                 static const std::string minValueOptionName;
                 static const std::string maxValueOptionName;
+#ifdef STORM_HAVE_Z3
+                static const std::string solveWithSmtOptionName;
+#endif
                 
             };