From fc9befbe9e23ce437688b1c705edb3e3cd9a14d6 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 11 Apr 2019 14:22:13 +0200 Subject: [PATCH] Added toExpression functions for SMT constraints --- .../modelchecker/dft/DFTASFChecker.cpp | 23 +++-- .../modelchecker/dft/DFTASFChecker.h | 4 +- .../modelchecker/dft/SmtConstraint.cpp | 94 +++++++++++++++---- 3 files changed, 95 insertions(+), 26 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 77fd60108..7852426e8 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -4,6 +4,7 @@ #include "storm/utility/file.h" #include "storm/utility/bitoperations.h" +#include "storm-parsers/parser/ExpressionCreator.h" #include "storm/solver/SmtSolver.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/Type.h" @@ -123,12 +124,6 @@ namespace storm { // Handle dependencies addMarkovianConstraints(); - - //TODO Move this out of convert method - - // Toplevel element will not fail (part of constraint 13) - constraints.push_back(std::make_shared(timePointVariables.at(dft.getTopLevelIndex()), notFailed)); - constraints.back()->setDescription("Toplevel element should not fail"); } // Constraint Generator Functions @@ -434,10 +429,12 @@ namespace storm { storm::utility::closeFile(stream); } - void DFTASFChecker::toSolver() { + std::vector DFTASFChecker::toSolver() { + std::vector resultVector; std::shared_ptr manager(new storm::expressions::ExpressionManager()); std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create( *manager); + //Add variables to manager for (auto const &timeVarEntry : timePointVariables) { manager->declareIntegerVariable(varNames[timeVarEntry.second]); } @@ -452,11 +449,21 @@ namespace storm { manager->declareIntegerVariable(varNames[tmpVar]); } } + // Add constraints to solver for (auto const &constraint : constraints) { solver->add(constraint->toExpression(varNames, manager)); } + // Set backtracking marker to check several properties without reconstructing DFT encoding + solver->push(); + + // Constraint that toplevel element will not fail (part of constraint 13) + std::shared_ptr tleNeverFailedConstr = std::make_shared( + timePointVariables.at(dft.getTopLevelIndex()), notFailed); + solver->add(tleNeverFailedConstr->toExpression(varNames, manager)); + resultVector.push_back(solver->check()); + solver->pop(); - //TODO Add porperties to check + return resultVector; } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index f202b40e7..0f152e6fa 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -4,6 +4,7 @@ #include #include +#include "storm/solver/SmtSolver.h" #include "SmtConstraint.h" #include "storm-dft/storage/dft/DFT.h" #include "storm/utility/solver.h" @@ -35,7 +36,8 @@ namespace storm { */ void convert(); void toFile(std::string const&); - void toSolver(); + + std::vector toSolver(); private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index bfec8b438..34450d98f 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -1,4 +1,5 @@ #include "DFTASFChecker.h" +#include #include namespace storm { @@ -36,7 +37,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector outerAnd; + std::vector innerOr; + for (auto const &ovi : varIndices) { + outerAnd.push_back((manager->getVariableExpression(varNames.at(varIndex)) >= + manager->getVariableExpression(varNames.at(ovi)))); + innerOr.push_back((manager->getVariableExpression(varNames.at(varIndex)) == + manager->getVariableExpression(varNames.at(ovi)))); + } + outerAnd.push_back(disjunction(innerOr)); + return conjunction(outerAnd); } private: @@ -76,7 +86,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector outerAnd; + std::vector innerOr; + for (auto const &ovi : varIndices) { + outerAnd.push_back((manager->getVariableExpression(varNames.at(varIndex)) <= + manager->getVariableExpression(varNames.at(ovi)))); + innerOr.push_back((manager->getVariableExpression(varNames.at(varIndex)) == + manager->getVariableExpression(varNames.at(ovi)))); + } + outerAnd.push_back(disjunction(innerOr)); + return conjunction(outerAnd); } private: @@ -105,7 +124,8 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return (manager->getVariableExpression(varNames.at(varIndex)) >= lowerBound) && + (manager->getVariableExpression(varNames.at(varIndex)) <= upperBound); } private: @@ -139,7 +159,15 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + if (constraints.empty()) { + return manager->boolean(true); + } else { + std::vector conjuncts; + for (auto const &c : constraints) { + conjuncts.push_back(c->toExpression(varNames, manager)); + } + return conjunction(conjuncts); + } } private: @@ -172,7 +200,15 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + if (constraints.empty()) { + return manager->boolean(false); + } else { + std::vector disjuncts; + for (auto const &c : constraints) { + disjuncts.push_back(c->toExpression(varNames, manager)); + } + return disjunction(disjuncts); + } } private: @@ -194,7 +230,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return implies(lhs->toExpression(varNames, manager), rhs->toExpression(varNames, manager)); } private: @@ -216,7 +252,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return iff(lhs->toExpression(varNames, manager), rhs->toExpression(varNames, manager)); } private: @@ -241,7 +277,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->boolean(value); } private: @@ -270,7 +306,11 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + if (value) { + return manager->getVariableExpression(varNames.at(varIndex)); + } else { + return !(manager->getVariableExpression(varNames.at(varIndex))); + } } private: @@ -296,7 +336,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(varIndex)) == manager->integer(value); } private: @@ -322,7 +362,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(varIndex)) < value; } private: @@ -347,7 +387,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(varIndex)) <= value; } private: @@ -370,7 +410,8 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(var1Index)) == + manager->getVariableExpression(varNames.at(var2Index)); } private: @@ -393,7 +434,8 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(var1Index)) < + manager->getVariableExpression(varNames.at(var2Index)); } private: @@ -427,7 +469,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector conjuncts; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + for (uint64_t j = i + 1; j < varIndices.size(); ++j) { + // check all elements pairwise for inequality + conjuncts.push_back(manager->getVariableExpression(varNames.at(varIndices.at(i))) != + manager->getVariableExpression(varNames.at(varIndices.at(j)))); + } + } + // take the conjunction of all pairwise inequalities + return conjunction(conjuncts); } private: @@ -455,9 +506,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector conjuncts; + for (uint64_t i = 1; i < varIndices.size(); ++i) { + conjuncts.push_back(manager->getVariableExpression(varNames.at(varIndices.at(i - 1))) <= + manager->getVariableExpression(varNames.at(varIndices.at(i)))); + } + // take the conjunction of all pairwise inequalities + return conjunction(conjuncts); } + private: std::vector varIndices; }; @@ -479,7 +537,9 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return ite(ifConstraint->toExpression(varNames, manager), + thenConstraint->toExpression(varNames, manager), + elseConstraint->toExpression(varNames, manager)); } private: