diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index befc25505..ed8cc4a57 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -543,6 +543,12 @@ namespace storm { storm::utility::Stopwatch latticeWatch(true); storm::analysis::LatticeExtender *extender = new storm::analysis::LatticeExtender(sparseModel); std::tuple criticalPair = extender->toLattice(formulas); + // TODO check not mdp + auto dtmcModel = model->as>(); + // TODO check formula type + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmcModel, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates()); + std::map>> result = assumptionMaker.startMakingAssumptions(std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair)); diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp new file mode 100644 index 000000000..6727793c0 --- /dev/null +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -0,0 +1,72 @@ +// +// Created by Jip Spel on 12.09.18. +// + +#include +#include +#include +#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" + + + + +namespace storm { + namespace analysis { + template + AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { + this->formula = formula; + + 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) { + auto val = std::pair((*itr), storm::utility::convertNumber(boost::lexical_cast((i+1)/(double (numberOfSamples + 1))))); + valuation.insert(val); + } + storm::models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; + if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); + checkResult = checker.computeUntilProbabilities(Environment(), checkTask); + } else if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { + const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); + checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "Expecting until or eventually formula"); + } + auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); + std::vector values = quantitativeResult.getValueVector(); + results.push_back(values); + } + this->numberOfStates = model->getNumberOfStates(); + this->initialStates = model->getInitialStates(); + } + + template + bool AssumptionChecker::checkOnSamples(uint_fast64_t val1, uint_fast64_t val2) { + bool result = true; + for (auto itr = results.begin(); result && itr != results.end(); ++itr) { + // TODO: als expressie + auto values = (*itr); + result &= (values[val1] >= values[val2]); + } + 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 new file mode 100644 index 000000000..7bd8cc916 --- /dev/null +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -0,0 +1,35 @@ +// +// Created by Jip Spel on 12.09.18. +// + +#ifndef STORM_ASSUMPTIONCHECKER_H +#define STORM_ASSUMPTIONCHECKER_H + +#include +#include +#include "storm/environment/Environment.h" + +namespace storm { + namespace analysis { + template + class AssumptionChecker { + public: + AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); + + bool checkOnSamples(uint_fast64_t val1, uint_fast64_t val2); + private: + std::shared_ptr formula; + + std::vector> sampleModels; + + std::vector> results; + + uint_fast64_t numberOfStates; + + storm::storage::BitVector initialStates; + }; + } +} + + +#endif //STORM_ASSUMPTIONCHECKER_H diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 134e52097..d61b5ef28 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -7,9 +7,10 @@ namespace storm { namespace analysis { template - AssumptionMaker::AssumptionMaker(storm::analysis::LatticeExtender* latticeExtender, uint_fast64_t numberOfStates) { + AssumptionMaker::AssumptionMaker(storm::analysis::LatticeExtender* latticeExtender, storm::analysis::AssumptionChecker* assumptionChecker, uint_fast64_t numberOfStates) { this->latticeExtender = latticeExtender; this->numberOfStates = numberOfStates; + 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)); @@ -27,15 +28,20 @@ namespace storm { } else { storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2)); - std::set> assumptions; - 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()); + 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; + } } return result; } @@ -43,22 +49,30 @@ namespace storm { template std::map>> AssumptionMaker::runRecursive(storm::analysis::Lattice* lattice, std::set> assumptions) { std::map>> result; - std::tuple criticalPair = this->latticeExtender->extendLattice(lattice, assumptions); + std::tuple criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions); - if (std::get<1>(criticalPair) == numberOfStates) { + if (std::get<1>(criticalTriple) == numberOfStates) { result.insert(std::pair>>(lattice, assumptions)); } else { - storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(std::get<1>(criticalPair))); - storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(std::get<2>(criticalPair))); + auto val1 = std::get<1>(criticalTriple); + auto val2 = std::get<2>(criticalTriple); + storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); + storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(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()); - myMap = createAssumptions(var2, var1, lattice, assumptions); - result.insert(myMap.begin(), myMap.end()); - } + 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; + } + } return result; } @@ -67,11 +81,13 @@ namespace storm { std::shared_ptr assumption1 = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(), var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::Greater)); + storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); assumptions.insert(assumption1); return (runRecursive(lattice, assumptions)); } + + template class AssumptionMaker; } } diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 2fa0a890c..49b50d3ea 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -6,8 +6,11 @@ #define STORM_ASSUMPTIONMAKER_H #include "Lattice.h" +#include "AssumptionChecker.h" #include "storm/storage/expressions/BinaryRelationExpression.h" #include "LatticeExtender.h" +#include "storm-pars/utility/ModelInstantiator.h" + namespace storm { namespace analysis { @@ -15,7 +18,7 @@ namespace storm { template class AssumptionMaker { public: - AssumptionMaker(storm::analysis::LatticeExtender* latticeExtender, uint_fast64_t numberOfStates); + AssumptionMaker(storm::analysis::LatticeExtender* latticeExtender, storm::analysis::AssumptionChecker* checker, uint_fast64_t numberOfStates); std::map>> startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2); @@ -29,6 +32,8 @@ namespace storm { std::shared_ptr expressionManager; uint_fast64_t numberOfStates; + + storm::analysis::AssumptionChecker* assumptionChecker; }; } } diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 24d5c4039..d62a0a696 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -34,7 +34,7 @@ namespace storm { STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() - || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula"); + || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until or eventually formula"); uint_fast64_t numberOfStates = this->model->getNumberOfStates(); @@ -86,7 +86,7 @@ namespace storm { // 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::Greater, storm::exceptions::NotImplementedException, "Only greater assumptions allowed"); + STORM_LOG_THROW(expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, storm::exceptions::NotImplementedException, "Only greater 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(); diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 8d2537598..62be096db 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -156,6 +156,4 @@ namespace storm { }; template class MonotonicityChecker; } - } -