From e23a2226056d97f295adce42daf2790aacf20cd2 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 18 Sep 2018 10:30:59 +0200 Subject: [PATCH] Add simple validation for assumptions --- src/storm-pars-cli/storm-pars.cpp | 3 +- src/storm-pars/analysis/AssumptionChecker.cpp | 60 ++++++++++++++++++- src/storm-pars/analysis/AssumptionChecker.h | 12 ++++ src/storm-pars/analysis/AssumptionMaker.cpp | 33 +++++----- src/storm-pars/analysis/AssumptionMaker.h | 6 +- src/storm-pars/analysis/Lattice.cpp | 2 +- src/storm-pars/analysis/LatticeExtender.cpp | 31 +++++----- src/storm-pars/analysis/LatticeExtender.h | 9 +-- .../analysis/MonotonicityChecker.cpp | 11 ++-- src/storm-pars/analysis/MonotonicityChecker.h | 2 +- 10 files changed, 121 insertions(+), 48 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index e2fec0e19..a5a06cc34 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -549,10 +549,9 @@ namespace storm { auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmcModel, 3); auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates()); - std::map>> result = assumptionMaker.makeAssumptions( + std::map, bool>>> result = assumptionMaker.makeAssumptions( std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair)); - latticeWatch.stop(); STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index 5cc5e6ea9..1d175a01c 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -13,20 +13,23 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/storage/expressions/SimpleValuation.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/VariableExpression.h" namespace storm { namespace analysis { template AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { this->formula = formula; + this->matrix = model->getTransitionMatrix(); // Create sample points - auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>(*model.get()); + auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>(*model); auto matrix = model->getTransitionMatrix(); std::set variables = storm::models::sparse::getProbabilityParameters(*model); for (auto i = 0; i < numberOfSamples; ++i) { auto valuation = storm::utility::parametric::Valuation(); for (auto itr = variables.begin(); itr != variables.end(); ++itr) { + // TODO: Type auto val = std::pair((*itr), storm::utility::convertNumber(boost::lexical_cast((i+1)/(double (numberOfSamples + 1))))); valuation.insert(val); } @@ -73,6 +76,61 @@ namespace storm { return result; } + template + bool AssumptionChecker::validateAssumption(std::shared_ptr assumption, storm::analysis::Lattice* lattice) { + bool result = false; + std::set vars = std::set({}); + assumption->gatherVariables(vars); + + STORM_LOG_THROW(assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, storm::exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported"); + + auto val1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()); + auto val2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()); + auto row1 = matrix.getRow(val1); + auto row2 = matrix.getRow(val2); + if (row1.getNumberOfEntries() != 2 && row2.getNumberOfEntries() != 2) { + assert (false); + } + + auto succ11 = row1.begin(); + auto succ12 = (++row1.begin()); + auto succ21 = row2.begin(); + auto succ22 = (++row2.begin()); + + if (succ12->getColumn() == succ21->getColumn() && succ11->getColumn() == succ22->getColumn()) { + auto temp = succ12; + succ12 = succ11; + succ11 = temp; + } + + if (succ11->getColumn() == succ21->getColumn() && succ12->getColumn() == succ22->getColumn()) { + ValueType prob; + auto comp = lattice->compare(succ11->getColumn(), succ12->getColumn()); + if (comp == storm::analysis::Lattice::ABOVE) { + prob = succ11->getValue() - succ21->getValue(); + } else if (comp == storm::analysis::Lattice::BELOW) { + prob = succ12->getValue() - succ22->getValue(); + } + auto vars = prob.gatherVariables(); + // TODO: Type + std::map substitutions; + for (auto var:vars) { + auto derivative = prob.derivative(var); + assert(derivative.isConstant()); + if (derivative.constantPart() >=0) { + substitutions[var] = 0; + } else if(derivative.constantPart() <= 0) { + substitutions[var] = 1; + } + } + result = prob.evaluate(substitutions) >= 0; + } + if (!result) { + STORM_PRINT("Could not validate: " << *assumption << std::endl); + } + return result; + } + template class AssumptionChecker; } } diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index 2f0f8313a..45b2b237e 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -9,6 +9,7 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/environment/Environment.h" #include "storm/storage/expressions/BinaryRelationExpression.h" +#include "Lattice.h" namespace storm { namespace analysis { @@ -32,9 +33,20 @@ namespace storm { */ bool checkOnSamples(std::shared_ptr assumption); + /*! + * Checks if an assumption can be validated based on the lattice and underlying transition matrix. + * + * @param assumption The assumption to validate. + * @param lattice The lattice. + * @return true if the assumption is validated and holds, false otherwise + */ + bool validateAssumption(std::shared_ptr assumption, storm::analysis::Lattice* lattice); + private: std::shared_ptr formula; + storm::storage::SparseMatrix matrix; + std::vector> results; }; diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 711a069cd..3382e3b2e 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -18,24 +18,24 @@ namespace storm { } template - std::map>> + std::map, bool>>> AssumptionMaker::makeAssumptions(storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2) { - std::map>> result; + std::map, bool>>> result; - std::set> emptySet; + std::vector, bool>> emptySet; if (critical1 == numberOfStates || critical2 == numberOfStates) { - result.insert(std::pair>>(lattice, emptySet)); + result.insert(std::pair, bool>>>(lattice, emptySet)); } else { storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2)); auto latticeCopy = new Lattice(lattice); - std::set> assumptions; + std::vector, bool>> assumptions; auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions); result.insert(myMap.begin(), myMap.end()); - std::set> assumptions2; + std::vector, bool>> assumptions2; myMap = createAssumptions(var2, var1, lattice, assumptions2); result.insert(myMap.begin(), myMap.end()); } @@ -43,12 +43,17 @@ namespace storm { } template - std::map>> AssumptionMaker::runRecursive(storm::analysis::Lattice* lattice, std::set> assumptions) { - std::map>> result; - std::tuple criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions); + std::map, bool>>> AssumptionMaker::runRecursive(storm::analysis::Lattice* lattice, std::vector,bool>> assumptions) { + std::map,bool>>> result; + // only the last assumption is new + std::tuple criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions.back().first); + + if (assumptions.back().second) { + assumptions.pop_back(); + } if (std::get<1>(criticalTriple) == numberOfStates) { - result.insert(std::pair>>(lattice, assumptions)); + result.insert(std::pair,bool>>>(lattice, assumptions)); } else { auto val1 = std::get<1>(criticalTriple); auto val2 = std::get<2>(criticalTriple); @@ -56,7 +61,7 @@ namespace storm { storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); auto latticeCopy = new Lattice(lattice); - std::set> assumptionsCopy = std::set>( + std::vector, bool>> assumptionsCopy = std::vector, bool>>( assumptions); auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy); result.insert(myMap.begin(), myMap.end()); @@ -68,15 +73,15 @@ namespace storm { } template - std::map>> AssumptionMaker::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::set> assumptions) { - std::map>> result; + std::map, bool>>> AssumptionMaker::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::vector, bool>> assumptions) { + std::map, bool>>> result; std::shared_ptr assumption = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); if (assumptionChecker->checkOnSamples(assumption)) { - assumptions.insert(assumption); + assumptions.push_back(std::pair, bool>(assumption, assumptionChecker->validateAssumption(assumption, lattice))); result = (runRecursive(lattice, assumptions)); } else { delete lattice; diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index a4d1a3478..55adbe0f5 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -35,13 +35,13 @@ namespace storm { * @param critical2 State number * @return A mapping from pointers to different lattices and assumptions made to create the specific lattice. */ - std::map>> makeAssumptions( + std::map, bool>>> makeAssumptions( storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2); private: - std::map>> runRecursive(storm::analysis::Lattice* lattice, std::set> assumptions); + std::map, bool>>> runRecursive(storm::analysis::Lattice* lattice, std::vector, bool>> assumptions); - std::map>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::set> assumptions); + std::map, bool>>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::vector, bool>> assumptions); storm::analysis::LatticeExtender* latticeExtender; diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 001873698..bea6439d2 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -121,7 +121,7 @@ namespace storm { if (node1 == node2) { return SAME; } - + // TODO: Uberhaupt niet mogelijk? bool isAbove = above(node1, node2, new std::set({})); bool isBelow = above(node2, node1, new std::set({})); if (isAbove && isBelow) { diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index a0448ce42..b4be618ed 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -75,24 +75,24 @@ namespace storm { } template - std::tuple LatticeExtender::extendLattice(storm::analysis::Lattice* lattice) { - std::set> assumptions; - return this->extendLattice(lattice, assumptions); - } - - template - std::tuple LatticeExtender::extendLattice(storm::analysis::Lattice* lattice, std::set> assumptions) { + std::tuple LatticeExtender::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr assumption) { auto numberOfStates = this->model->getNumberOfStates(); - // First handle assumptions - for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) { - storm::expressions::BinaryRelationExpression expr = *(*itr); - STORM_LOG_THROW(expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, storm::exceptions::NotImplementedException, "Only greater assumptions allowed"); + // First handle assumption + if (assumption != nullptr) { + storm::expressions::BinaryRelationExpression expr = *assumption; + STORM_LOG_THROW(expr.getRelationType() == + storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, + storm::exceptions::NotImplementedException, "Only GreaterOrEqual assumptions allowed"); if (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()) { storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); - if (lattice->compare(std::stoul(largest.getName(), nullptr, 0), std::stoul(smallest.getName(), nullptr, 0)) != storm::analysis::Lattice::ABOVE) { - storm::analysis::Lattice::Node* n1 = lattice->getNode(std::stoul(largest.getName(), nullptr, 0)); - storm::analysis::Lattice::Node* n2 = lattice->getNode(std::stoul(smallest.getName(), nullptr, 0)); + if (lattice->compare(std::stoul(largest.getName(), nullptr, 0), + std::stoul(smallest.getName(), nullptr, 0)) != + storm::analysis::Lattice::ABOVE) { + storm::analysis::Lattice::Node *n1 = lattice->getNode( + std::stoul(largest.getName(), nullptr, 0)); + storm::analysis::Lattice::Node *n2 = lattice->getNode( + std::stoul(smallest.getName(), nullptr, 0)); if (n1 != nullptr && n2 != nullptr) { lattice->addRelationNodes(n1, n2); @@ -102,7 +102,8 @@ namespace storm { lattice->addBetween(std::stoul(largest.getName(), nullptr, 0), lattice->getTop(), n2); } else { lattice->add(std::stoul(largest.getName(), nullptr, 0)); - lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), lattice->getNode(std::stoul(largest.getName(), nullptr, 0)), + lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), + lattice->getNode(std::stoul(largest.getName(), nullptr, 0)), lattice->getBottom()); } } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 38cc5429b..48bb7123a 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -39,23 +39,20 @@ namespace storm { std::tuple toLattice(std::vector> formulas); /*! - * Extends the lattice based on the given assumptions. + * Extends the lattice based on the given assumption. * * @param lattice The lattice. - * @param assumptions The assumptions on states. + * @param assumption The assumption on states. * @return A triple with a pointer to the lattice and two states of which the current place in the lattice * is unknown but needed. When the states have as number the number of states, no states are * unplaced but needed. */ - std::tuple extendLattice(storm::analysis::Lattice* lattice, std::set> assumptions); + std::tuple extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr assumption = nullptr); private: std::shared_ptr> model; std::map stateMap; - - std::tuple extendLattice(storm::analysis::Lattice* lattice); - }; } } diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 36d185acb..4750d21ff 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -9,7 +9,7 @@ namespace storm { namespace analysis { template - void MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { + void MonotonicityChecker::checkMonotonicity(std::map, bool>>> map, storm::storage::SparseMatrix matrix) { auto i = 0; for (auto itr = map.begin(); itr != map.end(); ++itr) { auto lattice = itr->first; @@ -23,17 +23,18 @@ namespace storm { if (assumptions.size() > 0) { STORM_PRINT("Given assumptions: " << std::endl); bool first = true; - for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) { + for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) { if (!first) { STORM_PRINT(" ^ "); } else { STORM_PRINT(" "); + first = false; } - first = false; - std::shared_ptr expression = *itr; + + std::shared_ptr expression = itr2->first; auto var1 = expression->getFirstOperand(); auto var2 = expression->getSecondOperand(); - STORM_PRINT("(" << var1->getIdentifier() << " > " << var2->getIdentifier() << ")"); + STORM_PRINT(*expression); } STORM_PRINT(std::endl); } diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 9d90e8b5d..6147b765b 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -24,7 +24,7 @@ namespace storm { * @param map The map with lattices and the assumptions made to create the lattices. * @param matrix The transition matrix. */ - void checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + void checkMonotonicity(std::map, bool>>> map, storm::storage::SparseMatrix matrix); private: std::map> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) ;