From a72c7a244af2d4e56915ab456835b0eebe4b3f93 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Wed, 30 Jan 2019 14:45:06 +0100 Subject: [PATCH] Fix bug with acyclic pmcs and more than one assumption --- src/storm-pars/analysis/LatticeExtender.cpp | 22 +- src/storm-pars/analysis/LatticeExtender.h | 2 +- .../analysis/MonotonicityChecker.cpp | 217 ++++++++++-------- 3 files changed, 136 insertions(+), 105 deletions(-) diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 4917da795..4161f8345 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -75,7 +75,7 @@ namespace storm { acyclic &= decomposition.getBlock(i).size() <= 1; } if (acyclic) { - states = storm::utility::graph::getTopologicalSort(matrix); + statesSorted = storm::utility::graph::getTopologicalSort(matrix); } else { for (uint_fast64_t i = 0; i < numberOfStates; ++i) { stateMap[i] = storm::storage::BitVector(numberOfStates, false); @@ -221,7 +221,11 @@ namespace storm { lowest = i; } } - lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); + if (lowest == highest) { + lattice->addToNode(stateNumber, lattice->getNode(highest)); + } else { + lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); + } } return std::make_tuple(lattice, numberOfStates, numberOfStates); } @@ -239,16 +243,17 @@ namespace storm { auto oldNumberSet = numberOfStates; while (oldNumberSet != lattice->getAddedStates().getNumberOfSetBits()) { oldNumberSet = lattice->getAddedStates().getNumberOfSetBits(); + auto states = statesSorted; if (acyclic && states.size() > 0) { auto nextState = *(states.begin()); - while (lattice->getAddedStates().get(nextState) && states.size() > 0) { + while (lattice->getAddedStates()[nextState] && states.size() > 1) { + // states.size()>1 such that there is at least one state left after erase states.erase(states.begin()); - nextState = *(states.begin()); } - if (! lattice->getAddedStates().get(nextState)) { + if (! lattice->getAddedStates()[nextState]) { auto row = this->model->getTransitionMatrix().getRow(nextState); auto successors = storm::storage::BitVector(lattice->getAddedStates().size()); for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { @@ -258,16 +263,20 @@ namespace storm { } } auto seenStates = (lattice->getAddedStates()); + assert ((seenStates & successors) == successors); auto result = extendAllSuccAdded(lattice, nextState, successors); - if (std::get<1>(result) != successors.size()) { + if (std::get<1>(result) != numberOfStates) { return result; } else { + assert (lattice->getNode(nextState) != nullptr); states.erase(states.begin()); } } + auto added = lattice->getAddedStates().getNumberOfSetBits(); assert (lattice->getNode(nextState) != nullptr); + assert (lattice->getAddedStates()[nextState]); } else if (!acyclic) { // TODO: kan dit niet efficienter @@ -324,6 +333,7 @@ namespace storm { } } } + assert (lattice->getAddedStates().getNumberOfSetBits() == numberOfStates); return std::make_tuple(lattice, numberOfStates, numberOfStates); } template class LatticeExtender; diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 7ff23ba05..c087d6422 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -54,7 +54,7 @@ namespace storm { std::map stateMap; - std::vector states; + std::vector statesSorted; bool acyclic; diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 9c2a90b1f..8f1a4efa0 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -150,14 +150,17 @@ namespace storm { auto i = 0; for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { auto lattice = itr->first; - if (itr != map.begin()) { - outfile << ";"; - } + + auto addedStates = lattice->getAddedStates().getNumberOfSetBits(); + assert (addedStates == lattice->getAddedStates().size()); std::map> varsMonotone = analyseMonotonicity(i, lattice, matrix); auto assumptions = itr->second; - bool validSomewhere = true; + bool validSomewhere = false; + for (auto itr2 = varsMonotone.begin(); !validSomewhere && itr2 != varsMonotone.end(); ++itr2) { + validSomewhere = itr2->second.first || itr2->second.second; + } if (assumptions.size() > 0) { // auto regions = checkAssumptionsOnRegion(assumptions); // if (regions.size() > 0) { @@ -189,9 +192,7 @@ namespace storm { // STORM_PRINT(std::endl); outfile << " - "; // } - } - - if (validSomewhere && assumptions.size() == 0) { + } else if (assumptions.size() == 0) { outfile << "No assumptions - "; } @@ -202,12 +203,12 @@ namespace storm { } else if (validSomewhere) { auto itr2 = varsMonotone.begin(); while (itr2 != varsMonotone.end()) { - 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 (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; @@ -222,7 +223,7 @@ namespace storm { // STORM_PRINT(" - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl); outfile << "? " << itr2->first; } - } +// } ++itr2; if (itr2 != varsMonotone.end()) { outfile << " "; @@ -231,8 +232,14 @@ namespace storm { result.insert( std::pair>>( lattice, varsMonotone)); + } else { + result.insert( + std::pair>>( + lattice, varsMonotone)); + outfile << "no monotonicity found"; } ++i; + outfile << ";"; } } outfile << ", "; @@ -292,10 +299,10 @@ namespace storm { auto numberOfStates = model->getNumberOfStates(); if (val1 == numberOfStates || val2 == numberOfStates) { assert (val1 == val2); + assert (lattice->getAddedStates().size() == lattice->getAddedStates().getNumberOfSetBits()); result.insert(std::pair>>(lattice, assumptions)); } else { - // TODO: should be triple auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, lattice); assert (assumptionTriple.size() == 3); auto itr = assumptionTriple.begin(); @@ -305,11 +312,13 @@ namespace storm { ++itr; auto assumption3 = *itr; - if (!assumption1.second && !assumption2.second) { + 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 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); @@ -318,60 +327,63 @@ namespace storm { 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); + 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); + std::get<1>(criticalTuple), std::get<2>(criticalTuple), + assumptionsCopy); result.insert(map.begin(), map.end()); } - // TODO verbeteren -// 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 (assumption1.second && assumption2.second) { - //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 (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); - + criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first); if (somewhereMonotonicity(std::get<0>(criticalTuple))) { - result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions); - } - - } else { - 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); + 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 (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 (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 { +// 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); +// } +// } } return result; } @@ -396,13 +408,13 @@ namespace storm { auto val = first.getValue(); auto vars = val.gatherVariables(); 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 (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; @@ -445,7 +457,7 @@ namespace storm { value->first = false; value->second = false; } - } +// } } } } @@ -463,41 +475,50 @@ namespace storm { bool monIncr = false; bool monDecr = false; - std::shared_ptr smtSolverFactory = std::make_shared(); - std::shared_ptr manager( - new storm::expressions::ExpressionManager()); + if (derivative.isZero()) { + monIncr = true; + monDecr = true; + } else { - storm::solver::Z3SmtSolver s(*manager); - storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown; + std::shared_ptr smtSolverFactory = std::make_shared(); + std::shared_ptr manager( + new storm::expressions::ExpressionManager()); - std::set variables = derivative.gatherVariables(); + 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; - } + 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; + 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; + } + assert (!(monIncr && monDecr) || derivative.isZero()); return std::pair(monIncr, monDecr); }