From cca2ad474e2adc2b5881f2bdb2a6861caf0f0ad9 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Mon, 8 Oct 2018 11:12:15 +0200 Subject: [PATCH] First check on samples for monotonicity --- src/storm-pars-cli/storm-pars.cpp | 40 +----- .../analysis/MonotonicityChecker.cpp | 120 +++++++++++++++++- src/storm-pars/analysis/MonotonicityChecker.h | 28 +++- .../analysis/MonotonicityCheckerTest.cpp | 64 +++++++++- 4 files changed, 210 insertions(+), 42 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index a32a92f3d..0e4a61bf6 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -1,9 +1,5 @@ - -#include "storm-pars/analysis/AssumptionMaker.h" -#include "storm-pars/analysis/Lattice.h" -#include "storm-pars/analysis/LatticeExtender.h" #include "storm-pars/analysis/MonotonicityChecker.h" #include "storm-cli-utilities/cli.h" @@ -529,40 +525,12 @@ namespace storm { std::cout << "Hello, Jip2" << std::endl; std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); - std::shared_ptr> sparseModel = model->as>(); - - // Transform to Lattices - storm::utility::Stopwatch latticeWatch(true); - storm::analysis::LatticeExtender *extender = new storm::analysis::LatticeExtender(sparseModel); - std::tuple criticalTuple = extender->toLattice(formulas); - std::map>> result; - if (model->isOfType(storm::models::ModelType::Dtmc)) { - auto dtmcModel = model->as>(); - auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmcModel, 3); - auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates(), parSettings.isValidateAssumptionsSet()); - result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple)); - } else if (model->isOfType(storm::models::ModelType::Dtmc)) { - auto mdpModel = model->as>(); - auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], mdpModel, 3); - auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates(), parSettings.isValidateAssumptionsSet()); - result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple)); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type."); - } - - - latticeWatch.stop(); - STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); - // Monotonicity? + // Monotonicity storm::utility::Stopwatch monotonicityWatch(true); - if (result.size() > 0) { - auto monotonicityChecker = storm::analysis::MonotonicityChecker(); - monotonicityChecker.checkMonotonicity(result, sparseModel->getTransitionMatrix()); - monotonicityWatch.stop(); - } else { - STORM_PRINT(std::endl << "Could not find monotonicity, no lattices created" << std::endl); - } + auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet()); + monotonicityChecker.checkMonotonicity(); + monotonicityWatch.stop(); STORM_PRINT(std::endl << "Time for monotonicity: " << monotonicityWatch << "." << std::endl << std::endl); diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 3a97e200b..eb8d74bf2 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -3,11 +3,50 @@ // #include "MonotonicityChecker.h" +#include "storm-pars/analysis/AssumptionMaker.h" +#include "storm-pars/analysis/AssumptionChecker.h" +#include "storm-pars/analysis/Lattice.h" +#include "storm-pars/analysis/LatticeExtender.h" + #include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/InvalidOperationException.h" + +#include "storm/utility/Stopwatch.h" +#include "storm/models/ModelType.h" + +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" + namespace storm { namespace analysis { + template + MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate) { + this->model = model; + this->formulas = formulas; + this->validate = validate; + } + + template + std::map>> MonotonicityChecker::checkMonotonicity() { + bool maybeMonotone = true; + if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto dtmcModel = model->as>(); + maybeMonotone = checkOnSamples(dtmcModel,3); + } //TODO mdp + if (maybeMonotone) { + auto map = createLattice(); + std::shared_ptr> sparseModel = model->as>(); + auto matrix = sparseModel->getTransitionMatrix(); + return checkMonotonicity(map, matrix); + } else { + std::map>> result; + std::cout << "Not monotone" << std::endl; + return result; + } + } + template std::map>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { auto i = 0; @@ -65,6 +104,33 @@ namespace storm { return result; } + template + std::map>> MonotonicityChecker::createLattice() { + // Transform to Lattices + storm::utility::Stopwatch latticeWatch(true); + std::shared_ptr> sparseModel = model->as>(); + storm::analysis::LatticeExtender *extender = new storm::analysis::LatticeExtender(sparseModel); + std::tuple criticalTuple = extender->toLattice(formulas); + std::map>> result; + if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto dtmcModel = model->as>(); + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmcModel, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates(), validate); + result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple)); + } else if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto mdpModel = model->as>(); + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], mdpModel, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates(), validate); + result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type."); + } + + latticeWatch.stop(); + STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); + return result; + } + template std::map> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { std::map> varsMonotone; @@ -163,6 +229,58 @@ namespace storm { return varsMonotone; } + template + bool MonotonicityChecker::checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples) { + bool monDecr = true; + bool monIncr = true; + + auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>(*model); + auto matrix = model->getTransitionMatrix(); + std::set variables = storm::models::sparse::getProbabilityParameters(*model); + double previous = -1; + 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); + } + storm::models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; + auto formula = formulas[0]; + 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(); + auto initialStates = model->getInitialStates(); + double initial = 0; + for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) { + initial += values[i]; + } + if (previous != -1) { + monDecr &= previous >= initial; + monIncr &= previous <= initial; + } + previous = initial; + } + + bool result = monDecr || monIncr; + return result; + } + template class MonotonicityChecker; } } diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 9fe48067e..81300897c 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -8,8 +8,13 @@ #include #include "Lattice.h" #include "storm/storage/expressions/BinaryRelationExpression.h" -#include "storm/storage/SparseMatrix.h" + #include "carl/core/Variable.h" +#include "storm/models/ModelBase.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/logic/Formula.h" +#include "storm/storage/SparseMatrix.h" namespace storm { namespace analysis { @@ -18,17 +23,38 @@ namespace storm { class MonotonicityChecker { public: + MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate); /*! * Checks for all lattices in the map if they are monotone increasing or monotone decreasing. * * @param map The map with lattices and the assumptions made to create the lattices. * @param matrix The transition matrix. + * @return TODO */ std::map>> checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + /*! + * TODO + * @param model + * @param formulas + * @param validate + * @return + */ + std::map>> checkMonotonicity(); + private: + //TODO: variabele type std::map> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) ; + std::map>> createLattice(); + + bool checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); + + std::shared_ptr model; + + std::vector> formulas; + + bool validate; }; } } diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index b7d40675a..7912bf7b0 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -10,8 +10,27 @@ #include "storm/storage/SparseMatrix.h" #include "storm/adapters/RationalFunctionAdapter.h" -TEST(MonotonicityCheckerTest, Monotone) { - auto checker = storm::analysis::MonotonicityChecker(); +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm-pars/api/storm-pars.h" +#include "storm/api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" + +TEST(MonotonicityCheckerTest, Monotone_no_model) { + std::shared_ptr model; + std::vector> formulas; + auto checker = storm::analysis::MonotonicityChecker(model, formulas, false); // Build lattice auto numberOfStates = 4; auto above = storm::storage::BitVector(numberOfStates); @@ -53,8 +72,10 @@ TEST(MonotonicityCheckerTest, Monotone) { EXPECT_TRUE(entry2->second.second); } -TEST(MonotonicityCheckerTest, NotMonotone) { - auto checker = storm::analysis::MonotonicityChecker(); +TEST(MonotonicityCheckerTest, Not_monotone_no_model) { + std::shared_ptr model; + std::vector> formulas; + auto checker = storm::analysis::MonotonicityChecker(model, formulas, false); // Build lattice auto numberOfStates = 4; auto above = storm::storage::BitVector(numberOfStates); @@ -89,4 +110,39 @@ TEST(MonotonicityCheckerTest, NotMonotone) { ASSERT_EQ("p", entry1->first.name()); EXPECT_FALSE(entry1->second.first); EXPECT_FALSE(entry1->second.second); +} + +TEST(MonotonicityCheckerTest, Brp_with_bisimulation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + + // Apply bisimulation + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (storm::settings::getModule().isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; + } + + dtmc = storm::api::performBisimulationMinimization(model, formulas, bisimType)->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); + + storm::analysis::MonotonicityChecker monotonicityChecker = storm::analysis::MonotonicityChecker(dtmc, formulas, true); + auto result = monotonicityChecker.checkMonotonicity(); + EXPECT_EQ(result.size(), 1); + EXPECT_EQ(result.begin()->second.size(), 2); + auto monotone = result.begin()->second.begin(); + EXPECT_EQ(monotone->second.first, true); + EXPECT_EQ(monotone->second.second, false); } \ No newline at end of file