diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 10d61e6a0..2340e57be 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -17,6 +17,10 @@ #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/solver/Z3SmtSolver.h" +#include "storm/storage/expressions/ExpressionManager.h" + +#include "storm/storage/expressions/RationalFunctionToExpression.h" namespace storm { @@ -108,7 +112,7 @@ namespace storm { outfile << "X " << itr2->first; } else { if (itr2->second.first && itr2->second.second) { - STORM_PRINT(" - Constant in" << itr2->first); + STORM_PRINT(" - Constant in" << itr2->first << std::endl); outfile << "C " << itr2->first; } else if (itr2->second.first) { STORM_PRINT(" - Monotone increasing in: " << itr2->first << std::endl); @@ -294,22 +298,31 @@ namespace storm { for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) { for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) { - auto derivative2 = (*itr2).second.derivative(*itr); - auto derivative3 = (*itr3).second.derivative(*itr); - STORM_LOG_THROW(derivative2.isConstant() && derivative3.isConstant(), - storm::exceptions::NotSupportedException, - "Expecting derivative to be constant"); + auto derivative2 = itr2->second.derivative(*itr); + auto derivative3 = itr3->second.derivative(*itr); - auto compare = lattice->compare((*itr2).first, (*itr3).first); + auto compare = lattice->compare(itr2->first, itr3->first); if (compare == storm::analysis::Lattice::ABOVE) { // As the first state (itr2) is above the second state (itr3) it is sufficient to look at the derivative of itr2. - value->first &= derivative2.constantPart() >= 0; - value->second &= derivative2.constantPart() <= 0; + std::pair mon2; + if (derivative2.isConstant()) { + mon2 = std::pair(derivative2.constantPart() >= 0, derivative2.constantPart() <=0); + } else { + mon2 = checkDerivative(derivative2); + } + value->first &= mon2.first; + value->second &= mon2.second; } else if (compare == storm::analysis::Lattice::BELOW) { // As the second state (itr3) is above the first state (itr2) it is sufficient to look at the derivative of itr3. - value->first &= derivative3.constantPart() >= 0; - value->second &= derivative3.constantPart() <= 0; + std::pair mon3; + if (derivative2.isConstant()) { + mon3 = std::pair(derivative3.constantPart() >= 0, derivative3.constantPart() <=0); + } else { + mon3 = checkDerivative(derivative3); + } + value->first &= mon3.first; + value->second &= mon3.second; } else if (compare == storm::analysis::Lattice::SAME) { // TODO: klopt dit // Behaviour doesn't matter, as the states are at the same level. @@ -331,6 +344,51 @@ namespace storm { return varsMonotone; } + template + std::pair MonotonicityChecker::checkDerivative(ValueType derivative) { + bool monIncr = false; + bool monDecr = false; + + 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; + + std::set variables = derivative.gatherVariables(); + + + for (auto variable : variables) { + manager->declareRationalVariable(variable.name()); + + } + storm::expressions::Expression exprBounds = manager->boolean(true); + auto managervars = manager->getVariables(); + for (auto var : managervars) { + exprBounds = exprBounds && manager->rational(0) <= var && manager->rational(1) >= var; + } + + auto converter = storm::expressions::RationalFunctionToExpression(manager); + + storm::expressions::Expression exprToCheck1 = converter.toExpression(derivative) >= manager->rational(0); + s.add(exprBounds); + s.add(exprToCheck1); + smtResult = s.check(); + monIncr = smtResult == storm::solver::SmtSolver::CheckResult::Sat; + + storm::expressions::Expression exprToCheck2 = converter.toExpression(derivative) <= manager->rational(0); + s.reset(); + smtResult = storm::solver::SmtSolver::CheckResult::Unknown; + s.add(exprBounds); + s.add(exprToCheck2); + smtResult = s.check(); + monDecr = smtResult == storm::solver::SmtSolver::CheckResult::Sat; + + return std::pair(monIncr, monDecr); + } + + template bool MonotonicityChecker::somewhereMonotonicity(storm::analysis::Lattice* lattice) { std::shared_ptr> sparseModel = model->as>(); @@ -359,26 +417,36 @@ namespace storm { } std::pair *value = &varsMonotone.find(*itr)->second; std::pair old = *value; - +// TODO deze ook aanpassen aan deel met smt solver for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) { for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) { - auto derivative2 = (*itr2).second.derivative(*itr); - auto derivative3 = (*itr3).second.derivative(*itr); - STORM_LOG_THROW(derivative2.isConstant() && derivative3.isConstant(), - storm::exceptions::NotSupportedException, - "Expecting derivative to be constant"); + auto derivative2 = itr2->second.derivative(*itr); + auto derivative3 = itr3->second.derivative(*itr); - auto compare = lattice->compare((*itr2).first, (*itr3).first); + auto compare = lattice->compare(itr2->first, itr3->first); if (compare == storm::analysis::Lattice::ABOVE) { // As the first state (itr2) is above the second state (itr3) it is sufficient to look at the derivative of itr2. - value->first &= derivative2.constantPart() >= 0; - value->second &= derivative2.constantPart() <= 0; + std::pair mon2; + if (derivative2.isConstant()) { + mon2 = std::pair(derivative2.constantPart() >= 0, derivative2.constantPart() <=0); + } else { + mon2 = checkDerivative(derivative2); + } + value->first &= mon2.first; + value->second &= mon2.second; } else if (compare == storm::analysis::Lattice::BELOW) { // As the second state (itr3) is above the first state (itr2) it is sufficient to look at the derivative of itr3. - value->first &= derivative3.constantPart() >= 0; - value->second &= derivative3.constantPart() <= 0; + std::pair mon3; + if (derivative2.isConstant()) { + mon3 = std::pair(derivative3.constantPart() >= 0, derivative3.constantPart() <=0); + } else { + mon3 = checkDerivative(derivative3); + } + value->first &= mon3.first; + value->second &= mon3.second; } else if (compare == storm::analysis::Lattice::SAME) { + // TODO: klopt dit // Behaviour doesn't matter, as the states are at the same level. } else { // As the relation between the states is unknown, we don't do anything diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index b625b538c..8a2404d73 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -59,6 +59,8 @@ namespace storm { std::map> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); + std::pair checkDerivative(ValueType derivative); + std::map>> extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions); std::shared_ptr model;