From b82ab5f9c29350794bf68ca3d832ddd96eb2e61b Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Mon, 24 Sep 2018 13:39:51 +0200 Subject: [PATCH] Validate assumption with SMT solving --- src/storm-pars/analysis/AssumptionChecker.cpp | 90 +++++++++++++++---- src/storm-pars/analysis/AssumptionChecker.h | 4 +- .../expressions/ValueTypeToExpression.cpp | 74 +++++++++++++++ .../expressions/ValueTypeToExpression.h | 46 ++++++++++ 4 files changed, 198 insertions(+), 16 deletions(-) create mode 100644 src/storm/storage/expressions/ValueTypeToExpression.cpp create mode 100644 src/storm/storage/expressions/ValueTypeToExpression.h diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index 0e18d0a7e..fdac5ed62 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -1,6 +1,7 @@ // // Created by Jip Spel on 12.09.18. // +#include #include "AssumptionChecker.h" #include "storm-pars/utility/ModelInstantiator.h" @@ -15,6 +16,8 @@ #include "storm/storage/expressions/SimpleValuation.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/VariableExpression.h" +#include "storm/utility/constants.h" +#include "storm/storage/expressions/ValueTypeToExpression.h" namespace storm { namespace analysis { @@ -133,9 +136,13 @@ namespace storm { // Only implemented for two successors if (row1.getNumberOfEntries() == 2 && row2.getNumberOfEntries() == 2) { - result = validateAssumptionOnFunction(lattice, row1, row2); + result = validateAssumptionFunction(lattice, row1, row2); + if (!result) { + result = validateAssumptionSMTSolver(lattice, row1, row2); + } } } + if (result) { validatedAssumptions.insert(assumption); } else { @@ -145,28 +152,28 @@ namespace storm { } template - bool AssumptionChecker::validateAssumptionOnFunction(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::rows row1, typename storm::storage::SparseMatrix::rows row2) { + bool AssumptionChecker::validateAssumptionFunction(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::rows row1, typename storm::storage::SparseMatrix::rows row2) { bool result = false; - auto succ1State1 = row1.begin(); - auto succ2State1 = (++row1.begin()); - auto succ1State2 = row2.begin(); - auto succ2State2 = (++row2.begin()); + auto state1succ1 = row1.begin(); + auto state1succ2 = (++row1.begin()); + auto state2succ1 = row2.begin(); + auto state2succ2 = (++row2.begin()); - if (succ1State1->getColumn() == succ2State2->getColumn() - && succ1State2->getColumn() == succ2State1->getColumn()) { + if (state1succ1->getColumn() == state2succ2->getColumn() + && state2succ1->getColumn() == state1succ2->getColumn()) { // swap them - auto temp = succ2State1; - succ2State1 = succ1State1; - succ1State1 = temp; + auto temp = state1succ2; + state1succ2 = state1succ1; + state1succ1 = temp; } - if (succ1State1->getColumn() == succ1State2->getColumn() && succ2State1->getColumn() == succ2State2->getColumn()) { + if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { ValueType prob; - auto comp = lattice->compare(succ1State1->getColumn(), succ2State1->getColumn()); + auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()); if (comp == storm::analysis::Lattice::ABOVE) { - prob = succ1State1->getValue() - succ1State2->getValue(); + prob = state1succ1->getValue() - state2succ1->getValue(); } else if (comp == storm::analysis::Lattice::BELOW) { - prob = succ2State1->getValue() - succ2State2->getValue(); + prob = state1succ2->getValue() - state2succ2->getValue(); } auto vars = prob.gatherVariables(); // TODO: Type @@ -185,6 +192,59 @@ namespace storm { return result; } + template + bool AssumptionChecker::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::rows row1, typename storm::storage::SparseMatrix::rows row2) { + bool result = false; + auto state1succ1 = row1.begin(); + auto state1succ2 = (++row1.begin()); + auto state2succ1 = row2.begin(); + auto state2succ2 = (++row2.begin()); + + if (state1succ1->getColumn() == state2succ2->getColumn() + && state2succ1->getColumn() == state1succ2->getColumn()) { + std::swap(state1succ1, state1succ2); + } + + if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { + std::shared_ptr smtSolverFactory = std::make_shared(); + std::shared_ptr manager( + new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown; + storm::expressions::Variable succ1 = manager->declareRationalVariable(std::to_string(state1succ1->getColumn())); + storm::expressions::Variable succ2 = manager->declareRationalVariable(std::to_string(state1succ2->getColumn())); + auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()); + if (comp == storm::analysis::Lattice::ABOVE || comp == storm::analysis::Lattice::BELOW) { + if (comp == storm::analysis::Lattice::BELOW) { + std::swap(succ1, succ2); + } + storm::expressions::Expression exprGiven = succ1 >= succ2; + + auto valueTypeToExpression = storm::expressions::ValueTypeToExpression(manager); + storm::expressions::Expression exprToCheck = + (valueTypeToExpression.toExpression(state1succ1->getValue())*succ1 + + valueTypeToExpression.toExpression(state2succ1->getValue())*succ2 + >= valueTypeToExpression.toExpression(state1succ2->getValue())*succ1 + + valueTypeToExpression.toExpression(state1succ1->getValue())*succ2); + + storm::expressions::Expression exprBounds = manager->boolean(true); + auto variables = manager->getVariables(); + for (auto var : variables) { + exprBounds = exprBounds && var >= 0 && var <= 1; + } + + s.add(exprGiven); + s.add(exprToCheck); + s.add(exprBounds); + smtResult = s.check(); + } + + result = smtResult == storm::solver::SmtSolver::CheckResult::Sat; + } + return result; + } + template bool AssumptionChecker::validated(std::shared_ptr assumption) { return find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end(); diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index bec43dd11..098e6433d 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -69,7 +69,9 @@ namespace storm { std::set> validatedAssumptions; - bool validateAssumptionOnFunction(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::rows row1, typename storm::storage::SparseMatrix::rows row2); + bool validateAssumptionFunction(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::rows row1, typename storm::storage::SparseMatrix::rows row2); + + bool validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::rows row1, typename storm::storage::SparseMatrix::rows row2); }; } } diff --git a/src/storm/storage/expressions/ValueTypeToExpression.cpp b/src/storm/storage/expressions/ValueTypeToExpression.cpp new file mode 100644 index 000000000..e1fa5c871 --- /dev/null +++ b/src/storm/storage/expressions/ValueTypeToExpression.cpp @@ -0,0 +1,74 @@ +// +// Created by Jip Spel on 24.09.18. +// + +#include "ValueTypeToExpression.h" +#include "storm/utility/constants.h" + +namespace storm { + namespace expressions { + template + ValueTypeToExpression::ValueTypeToExpression(std::shared_ptr manager) : manager(manager) { + // Intentionally left empty. + } + + template + std::shared_ptr ValueTypeToExpression::getManager() { + return manager; + } + + template + Expression ValueTypeToExpression::toExpression(ValueType function) { + auto varsFunction = function.gatherVariables(); + for (auto var : varsFunction) { + auto varsManager = manager->getVariables(); + bool found = find_if(varsManager.begin(), varsManager.end(), + [&](auto val) -> bool { + return val.getName() == var.name(); + }) != varsManager.end(); +// bool found = false; + // TODO kan dit niet anders + for (auto itr = varsManager.begin(); !found && itr != varsManager.end(); ++itr) { + found = (*itr).getName().compare(var.name()) == 0; + } + + if (!found) { + manager->declareIntegerVariable(var.name()); + } + } + + auto denominator = function.denominator(); + if (!denominator.isConstant()) { + STORM_LOG_DEBUG("Expecting the denominator to be constant"); + } + + storm::expressions::Expression denominatorVal = manager->integer(std::stoi(storm::utility::to_string(denominator.constantPart()))); + storm::expressions::Expression result; + if (function.isConstant()) { + result = manager->integer(std::stoi(storm::utility::to_string(function.constantPart()))); + } else { + auto nominator = function.nominatorAsPolynomial().polynomialWithCoefficient(); + result = manager->integer(std::stoi(storm::utility::to_string(nominator.constantPart()))); + for (auto itr = nominator.begin(); itr != nominator.end(); ++itr) { + varsFunction.clear(); + (*itr).gatherVariables(varsFunction); + // TODO: beter maken + storm::expressions::Expression nominatorPartExpr = manager->integer( + std::stoi(storm::utility::to_string((*itr).coeff()))); + for (auto var : varsFunction) { + if (!(*itr).derivative(var).isConstant()) { + STORM_LOG_DEBUG("Expecting partial derivatives of nominator parts to be constant"); + } + nominatorPartExpr = nominatorPartExpr * manager->getVariable(var.name()); + } + if (varsFunction.size() >= 1) { + result = result + nominatorPartExpr; + } + } + result = result / denominatorVal; + } + return result; + } + template class ValueTypeToExpression; + } +} \ No newline at end of file diff --git a/src/storm/storage/expressions/ValueTypeToExpression.h b/src/storm/storage/expressions/ValueTypeToExpression.h new file mode 100644 index 000000000..d0748483d --- /dev/null +++ b/src/storm/storage/expressions/ValueTypeToExpression.h @@ -0,0 +1,46 @@ +// +// Created by Jip Spel on 24.09.18. +// + +#ifndef STORM_VALUETYPETOEXPRESSION_H +#define STORM_VALUETYPETOEXPRESSION_H + +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace expressions { + template + class ValueTypeToExpression { + public: + /*! + * + * + * @param manager The manager of the variables. + */ + ValueTypeToExpression(std::shared_ptr manager); + + /*! + * Retrieves the manager responsible for the variables of this valuation. + * + * @return The pointer to the manager. + */ + std::shared_ptr getManager(); + + /*! + * + * @param function + * @param manager + * @return + */ + Expression toExpression(ValueType function); + + private: + // The manager responsible for the variables of this valuation. + std::shared_ptr manager; + }; + } +} + + +#endif //STORM_VALUETYPETOEXPRESSION_H