From 77a70179d3e69c5c915cda02425bd672e21d4d35 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 14 May 2019 15:05:47 +0200 Subject: [PATCH] Update MonotonicityChecker --- .../analysis/MonotonicityChecker.cpp | 618 +++++------------- src/storm-pars/analysis/MonotonicityChecker.h | 18 +- .../analysis/MonotonicityCheckerTest.cpp | 89 +-- 3 files changed, 185 insertions(+), 540 deletions(-) diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 64543de48..a2f3693c0 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -27,112 +27,35 @@ namespace storm { namespace analysis { template - MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate) { + MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, uint_fast64_t numberOfSamples) { outfile.open(filename, std::ios_base::app); + assert (model != nullptr); this->model = model; this->formulas = formulas; this->validate = validate; - this->resultCheckOnSamples = std::map>(); - // TODO initialiseren van sample check - if (model != nullptr) { - std::shared_ptr> sparseModel = model->as>(); - this->extender = new storm::analysis::LatticeExtender(sparseModel); - outfile << model->getNumberOfStates() << ", " << model->getNumberOfTransitions() << ", "; + + // sampling + if ( model->isOfType(storm::models::ModelType::Dtmc)) { + this->resultCheckOnSamples = std::map>(checkOnSamples(model->as>(), numberOfSamples)); + } else if (model->isOfType(storm::models::ModelType::Mdp)){ + this->resultCheckOnSamples = std::map>(checkOnSamples(model->as>(), numberOfSamples)); + } + + std::shared_ptr> sparseModel = model->as>(); + this->extender = new storm::analysis::LatticeExtender(sparseModel); + outfile << model->getNumberOfStates() << ", " << model->getNumberOfTransitions() << ", "; outfile.close(); - totalWatch = storm::utility::Stopwatch(true); } template std::map>> MonotonicityChecker::checkMonotonicity() { - // TODO: check on samples or not? - totalWatch = storm::utility::Stopwatch(true); - auto latticeWatch = storm::utility::Stopwatch(true); auto map = createLattice(); - // STORM_PRINT(std::endl << "Time for creating lattice: " << latticeWatch << "." << std::endl << std::endl); std::shared_ptr> sparseModel = model->as>(); auto matrix = sparseModel->getTransitionMatrix(); return checkMonotonicity(map, matrix); } - template - std::vector> MonotonicityChecker::checkAssumptionsOnRegion(std::vector> assumptions) { - assert (formulas[0]->isProbabilityOperatorFormula()); - assert (formulas[0]->asProbabilityOperatorFormula().getSubformula().isUntilFormula() || formulas[0]->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); - Environment env = Environment(); - std::shared_ptr> sparseModel = model->as>(); - bool generateSplitEstimates = false; - bool allowModelSimplification = false; - auto task = storm::api::createTask(formulas[0], true); - // TODO: storm::RationalNumber or double? - - // TODO: Also allow different models - STORM_LOG_THROW (sparseModel->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotImplementedException, - "Checking assumptions on a region not implemented for this type of model"); - auto modelChecker = storm::api::initializeParameterLiftingDtmcModelChecker(env, sparseModel, task, generateSplitEstimates, allowModelSimplification); - - std::stack, int>> regions; - std::vector> satRegions; - std::string regionText = ""; - auto parameters = storm::models::sparse::getProbabilityParameters(*sparseModel); - for (auto itr = parameters.begin(); itr != parameters.end(); ++itr) { - if (regionText != "") { - regionText += ","; - } - // TODO: region bounds - regionText += "0.1 <= " + itr->name() + " <= 0.9"; - } - - auto initialRegion = storm::api::parseRegion(regionText, parameters); - regions.push(std::pair, int>(initialRegion,0)); - while (!regions.empty()) { - auto lastElement = regions.top(); - regions.pop(); - storm::storage::ParameterRegion currentRegion = lastElement.first; - - // TODO: depth - if (lastElement.second < 5) { - auto upperBound = modelChecker->getBound(env, currentRegion, storm::solver::OptimizationDirection::Maximize); - auto lowerBound = modelChecker->getBound(env, currentRegion, storm::solver::OptimizationDirection::Minimize); - std::vector valuesUpper = upperBound->template asExplicitQuantitativeCheckResult().getValueVector(); - std::vector valuesLower = lowerBound->template asExplicitQuantitativeCheckResult().getValueVector(); - bool assumptionsHold = true; - for (auto itr = assumptions.begin(); assumptionsHold && itr != assumptions.end(); ++itr) { - auto assumption = *itr; - if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { - auto state1 = std::stoi( - assumption->getFirstOperand()->asVariableExpression().getVariableName()); - auto state2 = std::stoi( - assumption->getSecondOperand()->asVariableExpression().getVariableName()); - assumptionsHold &= valuesLower[state1] >= valuesUpper[state2]; - } else if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { - auto state1 = std::stoi( - assumption->getFirstOperand()->asVariableExpression().getVariableName()); - auto state2 = std::stoi( - assumption->getSecondOperand()->asVariableExpression().getVariableName()); - assumptionsHold &= valuesLower[state1] == valuesUpper[state2]; - } else { - assert(false); - } - } - if (!assumptionsHold) { - std::vector> newRegions; - currentRegion.split(currentRegion.getCenterPoint(), newRegions); - for (auto itr = newRegions.begin(); itr != newRegions.end(); ++itr) { - regions.push(std::pair, int>(*itr, - lastElement.second + - 1)); - } - } else { - satRegions.push_back(currentRegion); - } - } - } - return satRegions; - } - - - template std::map>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { storm::utility::Stopwatch monotonicityCheckWatch(true); @@ -142,8 +65,26 @@ namespace storm { if (map.size() == 0) { // Nothing is known - outfile << " No assumptions; ?"; - // STORM_PRINT(std::endl << "Do not know about monotonicity" << std::endl); + outfile << " No assumptions -"; + STORM_PRINT("No valid assumptions, couldn't build a sufficient lattice"); + if (resultCheckOnSamples.size() != 0) { + STORM_PRINT("\n" << "Based results on samples"); + } else { + outfile << " ?"; + } + + for (auto entry : resultCheckOnSamples) { + if (!entry.second.first && ! entry.second.second) { + outfile << " SX " << entry.first << " "; + } else if (entry.second.first && ! entry.second.second) { + outfile << " SI " << entry.first << " "; + } else if (entry.second.first && entry.second.second) { + outfile << " SC " << entry.first << " "; + } else { + outfile << " SD " << entry.first << " "; + } + } + } else { auto i = 0; for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { @@ -160,43 +101,21 @@ namespace storm { validSomewhere = itr2->second.first || itr2->second.second; } if (assumptions.size() > 0) { -// auto regions = checkAssumptionsOnRegion(assumptions); -// if (regions.size() > 0) { -// // STORM_PRINT("For regions: " << std::endl); -// bool first = true; -// for (auto itr2 = regions.begin(); itr2 != regions.end(); ++itr2) { -// if (first) { -// // STORM_PRINT(" "); -// first = false; -// } -// // STORM_PRINT(*itr2); -// outfile << (*itr2); -// } -// // STORM_PRINT(std::endl); -// outfile << ", "; -// } else { - // STORM_PRINT("Assumption(s): "); - bool first = true; - for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) { - if (!first) { - // STORM_PRINT(" ^ "); - outfile << (" ^ "); - } else { - first = false; - } - // STORM_PRINT(*(*itr2)); - outfile << (*(*itr2)); + bool first = true; + for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) { + if (!first) { + outfile << (" ^ "); + } else { + first = false; } - // STORM_PRINT(std::endl); - outfile << " - "; -// } + outfile << (*(*itr2)); + } + outfile << " - "; } else if (assumptions.size() == 0) { outfile << "No assumptions - "; } - if (validSomewhere && varsMonotone.size() == 0) { - // STORM_PRINT("Result is constant" << std::endl); outfile << "No params"; } else if (validSomewhere) { auto itr2 = varsMonotone.begin(); @@ -204,21 +123,15 @@ namespace storm { if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() && (!resultCheckOnSamples[itr2->first].first && !resultCheckOnSamples[itr2->first].second)) { - // STORM_PRINT(" - Not monotone in: " << itr2->first << std::endl); outfile << "X " << itr2->first; } else { if (itr2->second.first && itr2->second.second) { - // 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); outfile << "I " << itr2->first; } else if (itr2->second.second) { - // STORM_PRINT(" - Monotone decreasing in: " << itr2->first << std::endl); outfile << "D " << itr2->first; } else { - - // STORM_PRINT(" - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl); outfile << "? " << itr2->first; } } @@ -244,7 +157,6 @@ namespace storm { monotonicityCheckWatch.stop(); outfile << monotonicityCheckWatch << ", "; - // STORM_PRINT(std::endl << "Time for monotonicity check on lattice: " << monotonicityCheckWatch << "." << std::endl << std::endl); outfile.close(); return result; } @@ -283,7 +195,6 @@ namespace storm { assert(false); } latticeWatch.stop(); - // STORM_PRINT(std::endl << "Total time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); outfile.open(filename, std::ios_base::app); outfile << latticeWatch << ", "; outfile.close(); @@ -300,7 +211,7 @@ namespace storm { assert (lattice->getAddedStates()->size() == lattice->getAddedStates()->getNumberOfSetBits()); result.insert(std::pair>>(lattice, assumptions)); } else { - + // Make the three assumptions auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, lattice); assert (assumptionTriple.size() == 3); auto itr = assumptionTriple.begin(); @@ -310,152 +221,55 @@ namespace storm { ++itr; auto assumption3 = *itr; - auto assumptionsCopy = std::vector>( - assumptions); - auto assumptionsCopy2 = std::vector>( - assumptions); + if (assumption1.second != AssumptionStatus::INVALID) { + auto latticeCopy = new Lattice(lattice); + auto assumptionsCopy = std::vector>(assumptions); - auto latticeCopy = new storm::analysis::Lattice(lattice); - auto latticeCopy2 = new storm::analysis::Lattice(lattice); - - assumptions.push_back(assumption1.first); - assumptionsCopy.push_back(assumption2.first); - assumptionsCopy2.push_back(assumption3.first); + if (assumption1.second == AssumptionStatus::UNKNOWN) { + // only add assumption to the set of assumptions if it is unknown if it is valid + assumptionsCopy.push_back(assumption1.first); + } - auto criticalTuple = extender->extendLattice(lattice, assumption1.first); - if (assumption1.second != AssumptionStatus::INVALID && somewhereMonotonicity(std::get<0>(criticalTuple))) { - auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, - std::get<1>(criticalTuple), std::get<2>(criticalTuple), - assumptions); - result.insert(map.begin(), map.end()); + auto criticalTuple = extender->extendLattice(latticeCopy, assumption1.first); + if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + std::get<1>(criticalTuple), std::get<2>(criticalTuple), + assumptionsCopy); + result.insert(map.begin(), map.end()); + } } - // TODO: checkend at ie niet invalid is - criticalTuple = extender->extendLattice(latticeCopy, assumption2.first); - if (assumption2.second != AssumptionStatus::INVALID && somewhereMonotonicity(std::get<0>(criticalTuple))) { - auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, - std::get<1>(criticalTuple), std::get<2>(criticalTuple), - assumptionsCopy); - result.insert(map.begin(), map.end()); - } - criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first); - if (assumption3.second != AssumptionStatus::INVALID && somewhereMonotonicity(std::get<0>(criticalTuple))) { - auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, - std::get<1>(criticalTuple), std::get<2>(criticalTuple), - assumptionsCopy2); - result.insert(map.begin(), map.end()); + if (assumption2.second != AssumptionStatus::INVALID) { + auto latticeCopy = new Lattice(lattice); + auto assumptionsCopy = std::vector>(assumptions); + + if (assumption2.second == AssumptionStatus::UNKNOWN) { + assumptionsCopy.push_back(assumption2.first); + } + + auto criticalTuple = extender->extendLattice(latticeCopy, assumption2.first); + if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + std::get<1>(criticalTuple), std::get<2>(criticalTuple), + assumptionsCopy); + result.insert(map.begin(), map.end()); + } } + if (assumption3.second != AssumptionStatus::INVALID) { + // Here we can use the original lattice and assumptions set + if (assumption3.second == AssumptionStatus::UNKNOWN) { + assumptions.push_back(assumption3.first); + } -// if (!assumption1.second && !assumption2.second && !assumption3.second) { -// // Both assumption cannot be validated, so we need to keep them both -// // TODO: hier niet verder gaan als je iets gevonden hebt? -// auto assumptionsCopy = std::vector>( -// assumptions); -// auto assumptionsCopy2 = std::vector>( -// assumptions); -// auto latticeCopy = new storm::analysis::Lattice(lattice); -// auto latticeCopy2 = new storm::analysis::Lattice(lattice); -// assumptions.push_back(assumption1.first); -// assumptionsCopy.push_back(assumption2.first); -// assumptionsCopy2.push_back(assumption3.first); -// -// auto criticalTuple = extender->extendLattice(lattice, assumption1.first); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, -// std::get<1>(criticalTuple), std::get<2>(criticalTuple), -// assumptions); -// result.insert(map.begin(), map.end()); -// } -// -// criticalTuple = extender->extendLattice(latticeCopy, assumption2.first); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, -// std::get<1>(criticalTuple), std::get<2>(criticalTuple), -// assumptionsCopy); -// result.insert(map.begin(), map.end()); -// } -// criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, -// std::get<1>(criticalTuple), std::get<2>(criticalTuple), -// assumptionsCopy2); -// result.insert(map.begin(), map.end()); -// } -//// } -// } else if (!assumption3.second && assumption1.second && assumption2.second) { -//// assert (false); -// //TODO Both assumptions hold --> should not happen if we change it to < instead of <= -// auto assumption = assumptionMaker->createEqualAssumption(val1, val2); -// if (!validate) { -// assumptions.push_back(assumption); -// } -// // if validate is true and both hold, then they must be valid, so no need to add to assumptions -// auto criticalTuple = extender->extendLattice(lattice, assumption); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions); -// } -// } else if (!assumption3.second && !assumption2.second && assumption1.second) { -// if (!validate) { -//// assert(false); -// assumptions.push_back(assumption1.first); -// } -// // if validate is true and both hold, then they must be valid, so no need to add to assumptions -// -// auto criticalTuple = extender->extendLattice(lattice, assumption1.first); -// -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions); -// } -// -// } else if (!assumption3.second && !assumption1.second && assumption2.second){ -//// assert (assumption2.second); -// if (!validate) { -// assumptions.push_back(assumption2.first); -// } -// // if validate is true and both hold, then they must be valid, so no need to add to assumptions -// auto criticalTuple = extender->extendLattice(lattice, assumption2.first); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions); -// } -// } else { -// // TODO: should not happen -// STORM_LOG_WARN("All assumptions are true");// {" << *(assumption1.first) <<", " << *(assumption2.first) << ", " << *(assumption3.first) << "}" << std::endl); -// // Both assumption cannot be validated, so we need to keep them both -// // TODO: hier niet verder gaan als je iets gevonden hebt? -// auto assumptionsCopy = std::vector>( -// assumptions); -// auto assumptionsCopy2 = std::vector>( -// assumptions); -// auto latticeCopy = new storm::analysis::Lattice(lattice); -// auto latticeCopy2 = new storm::analysis::Lattice(lattice); -// assumptions.push_back(assumption1.first); -// assumptionsCopy.push_back(assumption2.first); -// assumptionsCopy2.push_back(assumption2.first); -// -// auto criticalTuple = extender->extendLattice(lattice, assumption1.first); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, -// std::get<1>(criticalTuple), std::get<2>(criticalTuple), -// assumptions); -// result.insert(map.begin(), map.end()); -// } -// -// criticalTuple = extender->extendLattice(latticeCopy, assumption2.first); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, -// std::get<1>(criticalTuple), std::get<2>(criticalTuple), -// assumptionsCopy); -// result.insert(map.begin(), map.end()); -// } -// criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first); -// if (somewhereMonotonicity(std::get<0>(criticalTuple))) { -// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, -// std::get<1>(criticalTuple), std::get<2>(criticalTuple), -// assumptionsCopy2); -// result.insert(map.begin(), map.end()); -// } -// } + auto criticalTuple = extender->extendLattice(lattice, assumption3.first); + if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + std::get<1>(criticalTuple), std::get<2>(criticalTuple), + assumptions); + result.insert(map.begin(), map.end()); + } + } } return result; } @@ -474,17 +288,17 @@ namespace storm { template std::map> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { -// storm::utility::Stopwatch analyseWatch(true); std::map> varsMonotone; + // go over all rows, check for each row local monotonicity for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { - // go over all rows auto row = matrix.getRow(i); // only enter if you are in a state with at least two successors (so there must be successors, - // and first prob shouldnt be 1) + // and first prob shouldn't be 1) if (row.begin() != row.end() && !row.begin()->getValue().isOne()) { std::map transitions; + // Gather all states which are reached with a non constant probability auto states = new storm::storage::BitVector(matrix.getColumnCount()); std::set vars; for (auto const& entry : row) { @@ -498,94 +312,79 @@ namespace storm { } } - auto sortedStates = lattice->sortStates(states); - - if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) {\ - // states are not properly sorted - for (auto itr = vars.begin(); itr != vars.end(); ++itr) { -// if (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end() && -// (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second)) { -// if (varsMonotone.find(*itr) == varsMonotone.end()) { -// varsMonotone[*itr].first = false; -// varsMonotone[*itr].second = false; -// } -// } else { - if (varsMonotone.find(*itr) == varsMonotone.end()) { - varsMonotone[*itr].first = true; - varsMonotone[*itr].second = true; - } - std::pair *value = &varsMonotone.find(*itr)->second; - std::pair old = *value; - + // Copy info from checkOnSamples + for (auto itr = vars.begin(); itr != vars.end(); ++itr) { + assert (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end()); + if (varsMonotone.find(*itr) == varsMonotone.end()) { + varsMonotone[*itr].first = resultCheckOnSamples[*itr].first; + varsMonotone[*itr].second = resultCheckOnSamples[*itr].second; + } else { + varsMonotone[*itr].first &= resultCheckOnSamples[*itr].first; + varsMonotone[*itr].second &= resultCheckOnSamples[*itr].second; + } + } + // Sort the states based on the lattice + auto sortedStates = lattice->sortStates(states); + if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) { + // If the states are not all sorted, we still might obtain some monotonicity + for (auto var: vars) { + // current value of monotonicity + std::pair *value = &varsMonotone.find(var)->second; - for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) { - for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) { + // Go over all transitions to successor states, compare all of them + for (auto itr2 = transitions.begin(); (value->first || value->second) + && itr2 != transitions.end(); ++itr2) { + for (auto itr3 = transitions.begin(); (value->first || value->second) + && itr3 != transitions.end(); ++itr3) { if (itr2->first < itr3->first) { - auto derivative2 = getDerivative(itr2->second, *itr); - auto derivative3 = getDerivative(itr3->second, *itr); + auto derivative2 = getDerivative(itr2->second, var); + auto derivative3 = getDerivative(itr3->second, var); 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. + if (compare == Lattice::ABOVE) { + // As the first state (itr2) is above the second state (itr3) it + // is sufficient to look at the derivative of itr2. std::pair mon2; - if (derivative2.isConstant()) { - mon2 = std::pair(derivative2.constantPart() >= 0, - derivative2.constantPart() <= 0); - } else { - mon2 = checkDerivative(derivative2); - } + 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. + } else if (compare == Lattice::BELOW) { + // As the second state (itr3) is above the first state (itr2) it + // is sufficient to look at the derivative of itr3. std::pair mon3; - if (derivative2.isConstant()) { - mon3 = std::pair(derivative3.constantPart() >= 0, - derivative3.constantPart() <= 0); - } else { - mon3 = checkDerivative(derivative3); - } + + mon3 = checkDerivative(derivative3); value->first &= mon3.first; value->second &= mon3.second; - } else if (compare == storm::analysis::Lattice::SAME) { - assert (false); - // TODO: klopt dit + } else if (compare == Lattice::SAME) { // Behaviour doesn't matter, as the states are at the same level. } else { - // As the relation between the states is unknown, we can't claim anything about the monotonicity. - value->first = false; - value->second = false; + // only if derivatives are the same we can continue + if (derivative2 != derivative3) { + // As the relation between the states is unknown, we can't claim + // anything about the monotonicity. + value->first = false; + value->second = false; + } + } } -// } } } } } else { - + // The states are all sorted for (auto var : vars) { -// if (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end() && -// (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second)) { -// if (varsMonotone.find(*itr) == varsMonotone.end()) { -// varsMonotone[*itr].first = false; -// varsMonotone[*itr].second = false; -// } -// } else { - if (varsMonotone.find(var) == varsMonotone.end()) { - varsMonotone[var].first = true; - varsMonotone[var].second = true; - } std::pair *value = &varsMonotone.find(var)->second; bool change = false; for (auto const &i : sortedStates) { -// auto res = checkDerivative(transitions[i].derivative(var)); auto res = checkDerivative(getDerivative(transitions[i], var)); change = change || (!(value->first && value->second) // they do not hold both - && ((value->first && !res.first) - || (value->second && !res.second))); + && ((value->first && !res.first) + || (value->second && !res.second))); if (change) { value->first &= res.second; @@ -598,84 +397,19 @@ namespace storm { break; } } + } } } } - -// analyseWatch.stop(); - // STORM_PRINT(std::endl << "Time to check monotonicity based on the lattice: " << analyseWatch << "." << std::endl << std::endl); -// outfile << analyseWatch << "; "; return varsMonotone; } -// template -// std::pair MonotonicityChecker::checkDerivative(ValueType derivative) { -// bool monIncr = false; -// bool monDecr = false; -// -// if (derivative.isZero()) { -// monIncr = true; -// monDecr = true; -// } else if (derivative.isConstant()) { -// monIncr = derivative.constantPart() >= 0; -// monDecr = derivative.constantPart() <= 0; -// } else { -// -// 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 && var < manager->rational(1); -// } -// -// 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; -// if (monIncr && monDecr) { -// monIncr = false; -// monDecr = false; -// } -// } -// assert (!(monIncr && monDecr) || derivative.isZero()); -// -// return std::pair(monIncr, monDecr); -// } - - template - bool MonotonicityChecker::somewhereMonotonicity(storm::analysis::Lattice* lattice) { + bool MonotonicityChecker::somewhereMonotonicity(Lattice* lattice) { std::shared_ptr> sparseModel = model->as>(); auto matrix = sparseModel->getTransitionMatrix(); - // TODO: tussenresultaten hergebruiken std::map> varsMonotone; for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { @@ -691,46 +425,54 @@ namespace storm { auto val = first.getValue(); auto vars = val.gatherVariables(); + // Copy info from checkOnSamples for (auto itr = vars.begin(); itr != vars.end(); ++itr) { + assert (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end()); if (varsMonotone.find(*itr) == varsMonotone.end()) { - varsMonotone[*itr].first = true; - varsMonotone[*itr].second = true; + varsMonotone[*itr].first = resultCheckOnSamples[*itr].first; + varsMonotone[*itr].second = resultCheckOnSamples[*itr].second; + } else { + varsMonotone[*itr].first &= resultCheckOnSamples[*itr].first; + varsMonotone[*itr].second &= resultCheckOnSamples[*itr].second; } - 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); - - 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. - std::pair mon2; - if (derivative2.isConstant()) { - mon2 = std::pair(derivative2.constantPart() >= 0, derivative2.constantPart() <=0); - } else { + } + + for (auto var: vars) { + // current value of monotonicity + std::pair *value = &varsMonotone.find(var)->second; + + // Go over all transitions to successor states, compare all of them + for (auto itr2 = transitions.begin(); (value->first || value->second) + && itr2 != transitions.end(); ++itr2) { + for (auto itr3 = transitions.begin(); (value->first || value->second) + && itr3 != transitions.end(); ++itr3) { + if (itr2->first < itr3->first) { + + auto derivative2 = getDerivative(itr2->second, var); + auto derivative3 = getDerivative(itr3->second, var); + + auto compare = lattice->compare(itr2->first, itr3->first); + + if (compare == Lattice::ABOVE) { + // As the first state (itr2) is above the second state (itr3) it + // is sufficient to look at the derivative of itr2. + std::pair mon2; 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. - std::pair mon3; - if (derivative2.isConstant()) { - mon3 = std::pair(derivative3.constantPart() >= 0, derivative3.constantPart() <=0); - } else { + value->first &= mon2.first; + value->second &= mon2.second; + } else if (compare == Lattice::BELOW) { + // As the second state (itr3) is above the first state (itr2) it + // is sufficient to look at the derivative of itr3. + std::pair mon3; + mon3 = checkDerivative(derivative3); + value->first &= mon3.first; + value->second &= mon3.second; + } else if (compare == Lattice::SAME) { + // 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 } - 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 } } } @@ -804,7 +546,7 @@ namespace storm { initial += values[i]; } float diff = previous - initial; - // TODO: define precission + // TODO: define precision if (previous != -1 && diff > 0.000005 && diff < -0.000005) { monDecr &= previous >= initial; monIncr &= previous <= initial; @@ -815,7 +557,6 @@ namespace storm { } samplesWatch.stop(); - // STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); resultCheckOnSamples = result; return result; } @@ -886,7 +627,6 @@ namespace storm { } samplesWatch.stop(); - // STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); resultCheckOnSamples = result; return result; } diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index a183edf14..47e189ad4 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -31,7 +31,7 @@ namespace storm { class MonotonicityChecker { public: - MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate); + MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, uint_fast64_t numberOfSamples = 100); /*! * Checks for all lattices in the map if they are monotone increasing or monotone decreasing. * @@ -111,10 +111,6 @@ namespace storm { assert (s.check() == storm::solver::SmtSolver::CheckResult::Sat); s.add(exprToCheck); monDecr = s.check() == storm::solver::SmtSolver::CheckResult::Unsat; -// if (monIncr && monDecr) { -// monIncr = false; -// monDecr = false; -// } } assert (!(monIncr && monDecr) || derivative.isZero()); @@ -123,9 +119,9 @@ namespace storm { private: //TODO: variabele type - std::map> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) ; + std::map> analyseMonotonicity(uint_fast64_t i, Lattice* lattice, storm::storage::SparseMatrix matrix) ; - std::map>> createLattice(); + std::map>> createLattice(); std::map> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); @@ -135,9 +131,7 @@ namespace storm { ValueType getDerivative(ValueType function, carl::Variable var); - std::vector> checkAssumptionsOnRegion(std::vector> assumptions); - - std::map>> extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions); + std::map>> extendLatticeWithAssumptions(Lattice* lattice, AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions); std::shared_ptr model; @@ -147,13 +141,11 @@ namespace storm { std::map> resultCheckOnSamples; - storm::analysis::LatticeExtender *extender; + LatticeExtender *extender; std::ofstream outfile; std::string filename = "results.txt"; - - storm::utility::Stopwatch totalWatch; }; } } diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index bb2d7008e..5b9a4ebfb 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -80,93 +80,6 @@ TEST(MonotonicityCheckerTest, Derivative_checker) { EXPECT_FALSE(functionRes.second); } -TEST(MonotonicityCheckerTest, Monotone_no_model) { - std::shared_ptr model; - std::vector> formulas; - auto checker = storm::analysis::MonotonicityChecker(model, formulas, false); - // Build lattice - auto numberOfStates = 4; - auto above = storm::storage::BitVector(numberOfStates); - above.set(1); - auto below = storm::storage::BitVector(numberOfStates); - below.set(0); - auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); - lattice.add(2); - lattice.add(3); - // Build map - std::vector> assumptions; - std::map>> map; - map.insert(std::pair>>(&lattice, assumptions)); - - // Build matrix - auto builder = storm::storage::SparseMatrixBuilder(numberOfStates, numberOfStates, 4); - std::shared_ptr cache = std::make_shared(); - carl::StringParser parser; - parser.setVariables({"p", "q"}); - auto func = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("p"), cache)); - auto funcMin = storm::RationalFunction(storm::RationalFunction(1)-func); - builder.addNextValue(2, 1, func); - builder.addNextValue(2, 0, funcMin); - func = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("q"), cache)); - funcMin = storm::RationalFunction(storm::RationalFunction(1)-func); - builder.addNextValue(3, 1, funcMin); - builder.addNextValue(3, 0, func); - storm::storage::SparseMatrix matrix = builder.build(); - - std::map>> result = checker.checkMonotonicity(map, matrix); - ASSERT_EQ(1, result.size()); - ASSERT_EQ(2, result.begin()->second.size()); - auto entry1 = result.begin()->second.begin(); - auto entry2 = ++ (result.begin()->second.begin()); - ASSERT_EQ("p", entry1->first.name()); - EXPECT_TRUE(entry1->second.first); - EXPECT_FALSE(entry1->second.second); - EXPECT_FALSE(entry2->second.first); - EXPECT_TRUE(entry2->second.second); -} - -TEST(MonotonicityCheckerTest, Not_monotone_no_model) { - std::shared_ptr model; - std::vector> formulas; - auto checker = storm::analysis::MonotonicityChecker(model, formulas, false); - // Build lattice - auto numberOfStates = 4; - auto above = storm::storage::BitVector(numberOfStates); - above.set(1); - auto below = storm::storage::BitVector(numberOfStates); - below.set(0); - auto initialMiddle = storm::storage::BitVector(numberOfStates); - auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates); - lattice.add(2); - lattice.add(3); - // Build map - std::vector> assumptions; - std::map>> map; - map.insert(std::pair>>(&lattice, assumptions)); - - // Build matrix - auto builder = storm::storage::SparseMatrixBuilder(numberOfStates, numberOfStates, 4); - std::shared_ptr cache = std::make_shared(); - carl::StringParser parser; - parser.setVariables({"p", "q"}); - auto func = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("p"), cache)); - auto funcMin = storm::RationalFunction(storm::RationalFunction(1)-func); - builder.addNextValue(2, 1, func); - builder.addNextValue(2, 0, funcMin); - builder.addNextValue(3, 1, funcMin); - builder.addNextValue(3, 0, func); - auto matrix = builder.build(); - - auto result = checker.checkMonotonicity(map, matrix); - ASSERT_EQ(1, result.size()); - ASSERT_EQ(1, result.begin()->second.size()); - auto entry1 = result.begin()->second.begin(); - ASSERT_EQ("p", entry1->first.name()); - EXPECT_FALSE(entry1->second.first); - EXPECT_FALSE(entry1->second.second); -} - TEST(MonotonicityCheckerTest, Brp_with_bisimulation) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; std::string formulaAsString = "P=? [F s=4 & i=N ]"; @@ -200,4 +113,4 @@ TEST(MonotonicityCheckerTest, Brp_with_bisimulation) { auto monotone = result.begin()->second.begin(); EXPECT_EQ(monotone->second.first, true); EXPECT_EQ(monotone->second.second, false); -} \ No newline at end of file +}