From 24a40bba80605f9afa5d0ce3d3dd3d3d15290295 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 18 Sep 2018 12:08:53 +0200 Subject: [PATCH] Add validated assumptions to set --- src/storm-pars-cli/storm-pars.cpp | 2 +- src/storm-pars/analysis/AssumptionChecker.cpp | 97 +++++++++++-------- src/storm-pars/analysis/AssumptionChecker.h | 3 + src/storm-pars/analysis/AssumptionMaker.cpp | 32 +++--- src/storm-pars/analysis/AssumptionMaker.h | 6 +- .../analysis/MonotonicityChecker.cpp | 4 +- src/storm-pars/analysis/MonotonicityChecker.h | 2 +- 7 files changed, 82 insertions(+), 64 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index a5a06cc34..e7aedd2f7 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -549,7 +549,7 @@ namespace storm { auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmcModel, 3); auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates()); - std::map, bool>>> result = assumptionMaker.makeAssumptions( + std::map>> result = assumptionMaker.makeAssumptions( std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair)); latticeWatch.stop(); diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index 1d175a01c..c3014d3a9 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -78,59 +78,72 @@ namespace storm { 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"); + bool result = validated(assumption); + if (!result) { + std::set vars = std::set({}); + assumption->gatherVariables(vars); - 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); - } + STORM_LOG_THROW(assumption->getRelationType() == + storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, + storm::exceptions::NotSupportedException, + "Only Greater Or Equal assumptions supported"); - auto succ11 = row1.begin(); - auto succ12 = (++row1.begin()); - auto succ21 = row2.begin(); - auto succ22 = (++row2.begin()); + 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); + } - if (succ12->getColumn() == succ21->getColumn() && succ11->getColumn() == succ22->getColumn()) { - auto temp = succ12; - succ12 = succ11; - succ11 = temp; - } + auto succ11 = row1.begin(); + auto succ12 = (++row1.begin()); + auto succ21 = row2.begin(); + auto succ22 = (++row2.begin()); - 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(); + if (succ12->getColumn() == succ21->getColumn() && succ11->getColumn() == succ22->getColumn()) { + auto temp = succ12; + succ12 = succ11; + succ11 = temp; } - 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; + + 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) { + validatedAssumptions.insert(assumption); + } else { + STORM_PRINT("Could not validate: " << *assumption << std::endl); } - result = prob.evaluate(substitutions) >= 0; - } - if (!result) { - STORM_PRINT("Could not validate: " << *assumption << std::endl); } + return result; } + template + bool AssumptionChecker::validated(std::shared_ptr assumption) { + return find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end(); + } + template class AssumptionChecker; } } diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index 45b2b237e..e336f97f3 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -42,6 +42,7 @@ namespace storm { */ bool validateAssumption(std::shared_ptr assumption, storm::analysis::Lattice* lattice); + bool validated(std::shared_ptr assumption); private: std::shared_ptr formula; @@ -49,6 +50,8 @@ namespace storm { std::vector> results; + std::set> validatedAssumptions; + }; } } diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 3382e3b2e..c6804ef59 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -18,24 +18,24 @@ namespace storm { } template - std::map, bool>>> + std::map>> AssumptionMaker::makeAssumptions(storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2) { - std::map, bool>>> result; + std::map>> result; - std::vector, bool>> emptySet; + std::vector> emptySet; if (critical1 == numberOfStates || critical2 == numberOfStates) { - result.insert(std::pair, bool>>>(lattice, emptySet)); + result.insert(std::pair>>(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::vector, bool>> assumptions; + std::vector> assumptions; auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions); result.insert(myMap.begin(), myMap.end()); - std::vector, bool>> assumptions2; + std::vector> assumptions2; myMap = createAssumptions(var2, var1, lattice, assumptions2); result.insert(myMap.begin(), myMap.end()); } @@ -43,17 +43,17 @@ namespace storm { } template - std::map, bool>>> AssumptionMaker::runRecursive(storm::analysis::Lattice* lattice, std::vector,bool>> assumptions) { - std::map,bool>>> result; + std::map>> AssumptionMaker::runRecursive(storm::analysis::Lattice* lattice, std::vector> assumptions) { + std::map>> result; // only the last assumption is new - std::tuple criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions.back().first); + std::tuple criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions.back()); - if (assumptions.back().second) { + if (assumptionChecker->validated(assumptions.back())) { assumptions.pop_back(); } if (std::get<1>(criticalTriple) == numberOfStates) { - result.insert(std::pair,bool>>>(lattice, assumptions)); + result.insert(std::pair>>(lattice, assumptions)); } else { auto val1 = std::get<1>(criticalTriple); auto val2 = std::get<2>(criticalTriple); @@ -61,7 +61,7 @@ namespace storm { storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); auto latticeCopy = new Lattice(lattice); - std::vector, bool>> assumptionsCopy = std::vector, bool>>( + std::vector> assumptionsCopy = std::vector>( assumptions); auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy); result.insert(myMap.begin(), myMap.end()); @@ -73,15 +73,17 @@ namespace storm { } template - 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::map>> AssumptionMaker::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::vector> assumptions) { + std::map>> 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.push_back(std::pair, bool>(assumption, assumptionChecker->validateAssumption(assumption, lattice))); + // TODO: only if validation on + assumptionChecker->validateAssumption(assumption, lattice); + assumptions.push_back(std::shared_ptr(assumption)); result = (runRecursive(lattice, assumptions)); } else { delete lattice; diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 55adbe0f5..73e6c5bdd 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, bool>>> makeAssumptions( + std::map>> makeAssumptions( storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2); private: - std::map, bool>>> runRecursive(storm::analysis::Lattice* lattice, std::vector, bool>> assumptions); + std::map>> runRecursive(storm::analysis::Lattice* lattice, std::vector> assumptions); - std::map, bool>>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::vector, bool>> assumptions); + std::map>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::vector> assumptions); storm::analysis::LatticeExtender* latticeExtender; diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 4750d21ff..0ee7c6ad2 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, bool>>> map, storm::storage::SparseMatrix matrix) { + void MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { auto i = 0; for (auto itr = map.begin(); itr != map.end(); ++itr) { auto lattice = itr->first; @@ -31,7 +31,7 @@ namespace storm { first = false; } - std::shared_ptr expression = itr2->first; + std::shared_ptr expression = *itr2; auto var1 = expression->getFirstOperand(); auto var2 = expression->getSecondOperand(); STORM_PRINT(*expression); diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 6147b765b..222c0129a 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, bool>>> map, storm::storage::SparseMatrix matrix); + void checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); private: std::map> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) ;