From 06255ef08ee2a350fb0835060e43804e875cad27 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 14 Sep 2018 11:06:28 +0200 Subject: [PATCH] Use BinaryRelationExpression to check on samples --- src/storm-pars/analysis/AssumptionChecker.cpp | 34 ++++++++--- src/storm-pars/analysis/AssumptionChecker.h | 15 +++-- src/storm-pars/analysis/AssumptionMaker.cpp | 60 +++++++++---------- 3 files changed, 64 insertions(+), 45 deletions(-) diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index 6727793c0..bba77fb37 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -2,15 +2,16 @@ // Created by Jip Spel on 12.09.18. // -#include -#include -#include +#include "storm-pars/utility/ModelInstantiator.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/exceptions/NotSupportedException.h" #include "AssumptionChecker.h" #include "storm/modelchecker/CheckTask.h" #include "storm/environment/Environment.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" - +#include "storm/storage/expressions/SimpleValuation.h" +#include "storm/storage/expressions/ExpressionManager.h" @@ -23,8 +24,6 @@ namespace storm { auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>(*model.get()); 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) { @@ -52,8 +51,8 @@ namespace storm { std::vector values = quantitativeResult.getValueVector(); results.push_back(values); } - this->numberOfStates = model->getNumberOfStates(); - this->initialStates = model->getInitialStates(); +// this->numberOfStates = model->getNumberOfStates(); +// this->initialStates = model->getInitialStates(); } template @@ -67,6 +66,25 @@ namespace storm { return result; } + template + bool AssumptionChecker::checkOnSamples(std::shared_ptr assumption) { + bool result = true; + std::set vars = std::set({}); + assumption->gatherVariables(vars); + for (auto itr = results.begin(); result && itr != results.end(); ++itr) { + std::shared_ptr manager = assumption->getManager().getSharedPointer(); + auto valuation = storm::expressions::SimpleValuation(manager); + auto values = (*itr); + for (auto var = vars.begin(); result && var != vars.end(); ++var) { + storm::expressions::Variable par = *var; + auto index = std::stoi(par.getName()); + valuation.setRationalValue(par, values[index]); + } + result &= assumption->evaluateAsBool(&valuation); + } + return result; + } + template class AssumptionChecker; } } \ No newline at end of file diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index 7bd8cc916..78e209ab2 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -5,9 +5,11 @@ #ifndef STORM_ASSUMPTIONCHECKER_H #define STORM_ASSUMPTIONCHECKER_H -#include -#include +#include "storm/logic/Formula.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/environment/Environment.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" + namespace storm { namespace analysis { @@ -17,16 +19,17 @@ namespace storm { AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); bool checkOnSamples(uint_fast64_t val1, uint_fast64_t val2); + bool checkOnSamples(std::shared_ptr assumption); private: std::shared_ptr formula; - std::vector> sampleModels; +// std::vector> sampleModels; std::vector> results; - uint_fast64_t numberOfStates; - - storm::storage::BitVector initialStates; +// uint_fast64_t numberOfStates; +// +// storm::storage::BitVector initialStates; }; } } diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index d61b5ef28..db98a3498 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -13,7 +13,7 @@ namespace storm { this->assumptionChecker = assumptionChecker; this->expressionManager = std::make_shared(storm::expressions::ExpressionManager()); for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) { - expressionManager->declareIntegerVariable(std::to_string(i)); + expressionManager->declareRationalVariable(std::to_string(i)); } } @@ -29,19 +29,14 @@ namespace storm { storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2)); - if (assumptionChecker->checkOnSamples(critical1, critical2)) { - auto latticeCopy = new Lattice(lattice); - std::set> assumptions; - auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions); - result.insert(myMap.begin(), myMap.end()); - } - if (assumptionChecker->checkOnSamples(critical2, critical1)) { - std::set> assumptions; - auto myMap = createAssumptions(var2, var1, lattice, assumptions); - result.insert(myMap.begin(), myMap.end()); - } else { - delete lattice; - } + auto latticeCopy = new Lattice(lattice); + std::set> assumptions; + auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions); + result.insert(myMap.begin(), myMap.end()); + + std::set> assumptions2; + myMap = createAssumptions(var2, var1, lattice, assumptions2); + result.insert(myMap.begin(), myMap.end()); } return result; } @@ -59,31 +54,34 @@ namespace storm { storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); - if (assumptionChecker->checkOnSamples(val1, val2)) { - auto latticeCopy = new Lattice(lattice); - std::set> assumptionsCopy = std::set>(assumptions); - auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy); - result.insert(myMap.begin(), myMap.end()); - } - - if (assumptionChecker->checkOnSamples(val2, val1)) { - auto myMap = createAssumptions(var2, var1, lattice, assumptions); - result.insert(myMap.begin(), myMap.end()); - } else { - delete lattice; - } + auto latticeCopy = new Lattice(lattice); + std::set> assumptionsCopy = std::set>( + assumptions); + auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy); + result.insert(myMap.begin(), myMap.end()); + + myMap = createAssumptions(var2, var1, lattice, assumptions); + result.insert(myMap.begin(), myMap.end()); } return result; } template std::map>> AssumptionMaker::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::set> assumptions) { - std::shared_ptr assumption1 - = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(), + 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)); - assumptions.insert(assumption1); - return (runRecursive(lattice, assumptions)); + if (assumptionChecker->checkOnSamples(assumption)) { + assumptions.insert(assumption); + result = (runRecursive(lattice, assumptions)); + } else { + delete lattice; + } + + return result; }