From 0d1ddb623270cc2c52d3fc78ae0a95e83edb448c Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 14 May 2019 16:25:21 +0200 Subject: [PATCH] Make sampling in monotonicity-analysis optional --- src/storm-pars-cli/storm-pars.cpp | 3 +- .../analysis/MonotonicityChecker.cpp | 92 +++++++++++-------- src/storm-pars/analysis/MonotonicityChecker.h | 28 +++--- .../settings/modules/ParametricSettings.cpp | 14 ++- .../settings/modules/ParametricSettings.h | 19 +++- .../analysis/MonotonicityCheckerTest.cpp | 41 ++++++++- 6 files changed, 134 insertions(+), 63 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 01fa208e2..0105e55ef 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -727,7 +727,8 @@ namespace storm { std::ofstream outfile; outfile.open("results.txt", std::ios_base::app); storm::utility::Stopwatch monotonicityWatch(true); - auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet()); + auto numberOfSamples = parSettings.getNumberOfSamples(); + auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet(), numberOfSamples); monotonicityChecker.checkMonotonicity(); monotonicityWatch.stop(); STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index a2f3693c0..092a3ffbf 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -28,24 +28,28 @@ namespace storm { namespace analysis { template MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, uint_fast64_t numberOfSamples) { - outfile.open(filename, std::ios_base::app); assert (model != nullptr); this->model = model; this->formulas = formulas; this->validate = validate; - // sampling - if ( model->isOfType(storm::models::ModelType::Dtmc)) { - this->resultCheckOnSamples = std::map>(checkOnSamples(model->as>(), numberOfSamples)); - } else if (model->isOfType(storm::models::ModelType::Mdp)){ - this->resultCheckOnSamples = std::map>(checkOnSamples(model->as>(), numberOfSamples)); + if (numberOfSamples > 0) { + // sampling + if (model->isOfType(storm::models::ModelType::Dtmc)) { + this->resultCheckOnSamples = std::map>( + checkOnSamples(model->as>(), numberOfSamples)); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + this->resultCheckOnSamples = std::map>( + checkOnSamples(model->as>(), numberOfSamples)); + } + checkSamples= true; + } else { + checkSamples= false; } std::shared_ptr> sparseModel = model->as>(); this->extender = new storm::analysis::LatticeExtender(sparseModel); - outfile << model->getNumberOfStates() << ", " << model->getNumberOfTransitions() << ", "; - outfile.close(); } template @@ -96,10 +100,6 @@ namespace storm { matrix); auto assumptions = itr->second; - bool validSomewhere = false; - for (auto itr2 = varsMonotone.begin(); !validSomewhere && itr2 != varsMonotone.end(); ++itr2) { - validSomewhere = itr2->second.first || itr2->second.second; - } if (assumptions.size() > 0) { bool first = true; for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) { @@ -115,12 +115,13 @@ namespace storm { outfile << "No assumptions - "; } - if (validSomewhere && varsMonotone.size() == 0) { + if (varsMonotone.size() == 0) { outfile << "No params"; - } else if (validSomewhere) { + } else { auto itr2 = varsMonotone.begin(); while (itr2 != varsMonotone.end()) { - if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() && + if (checkSamples && + resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() && (!resultCheckOnSamples[itr2->first].first && !resultCheckOnSamples[itr2->first].second)) { outfile << "X " << itr2->first; @@ -143,11 +144,6 @@ namespace storm { result.insert( std::pair>>( lattice, varsMonotone)); - } else { - result.insert( - std::pair>>( - lattice, varsMonotone)); - outfile << "no monotonicity found"; } ++i; outfile << ";"; @@ -156,7 +152,6 @@ namespace storm { outfile << ", "; monotonicityCheckWatch.stop(); - outfile << monotonicityCheckWatch << ", "; outfile.close(); return result; } @@ -195,9 +190,6 @@ namespace storm { assert(false); } latticeWatch.stop(); - outfile.open(filename, std::ios_base::app); - outfile << latticeWatch << ", "; - outfile.close(); return result; } @@ -313,17 +305,28 @@ namespace storm { } // Copy info from checkOnSamples - for (auto itr = vars.begin(); itr != vars.end(); ++itr) { - assert (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end()); - if (varsMonotone.find(*itr) == varsMonotone.end()) { - varsMonotone[*itr].first = resultCheckOnSamples[*itr].first; - varsMonotone[*itr].second = resultCheckOnSamples[*itr].second; - } else { - varsMonotone[*itr].first &= resultCheckOnSamples[*itr].first; - varsMonotone[*itr].second &= resultCheckOnSamples[*itr].second; + if (checkSamples) { + for (auto var : vars) { + assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end()); + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = resultCheckOnSamples[var].first; + varsMonotone[var].second = resultCheckOnSamples[var].second; + } else { + varsMonotone[var].first &= resultCheckOnSamples[var].first; + varsMonotone[var].second &= resultCheckOnSamples[var].second; + } + } + } else { + for (auto var : vars) { + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = true; + varsMonotone[var].second = true; + } } } + + // Sort the states based on the lattice auto sortedStates = lattice->sortStates(states); if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) { @@ -426,14 +429,23 @@ namespace storm { auto val = first.getValue(); auto vars = val.gatherVariables(); // Copy info from checkOnSamples - for (auto itr = vars.begin(); itr != vars.end(); ++itr) { - assert (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end()); - if (varsMonotone.find(*itr) == varsMonotone.end()) { - varsMonotone[*itr].first = resultCheckOnSamples[*itr].first; - varsMonotone[*itr].second = resultCheckOnSamples[*itr].second; - } else { - varsMonotone[*itr].first &= resultCheckOnSamples[*itr].first; - varsMonotone[*itr].second &= resultCheckOnSamples[*itr].second; + if (checkSamples) { + for (auto var : vars) { + assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end()); + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = resultCheckOnSamples[var].first; + varsMonotone[var].second = resultCheckOnSamples[var].second; + } else { + varsMonotone[var].first &= resultCheckOnSamples[var].first; + varsMonotone[var].second &= resultCheckOnSamples[var].second; + } + } + } else { + for (auto var : vars) { + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = true; + varsMonotone[var].second = true; + } } } diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 47e189ad4..81bd6801a 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -31,27 +31,23 @@ namespace storm { class MonotonicityChecker { public: - MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, uint_fast64_t numberOfSamples = 100); /*! - * 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 + * Constructor of MonotonicityChecker + * @param model the model considered + * @param formula the formula considered + * @param validate whether or not assumptions are to be validated + * @param numberOfSamples number of samples taken for monotonicity checking, default 0, + * if 0then no check on samples is executed */ - std::map>> checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, uint_fast64_t numberOfSamples=0); /*! - * TODO - * @return + * Checks for model and formula as provided in constructor for monotonicity */ std::map>> checkMonotonicity(); /*! - * TODO - * @param lattice - * @param matrix - * @return + * Checks if monotonicity can be found in this lattice. Unordered states are not checked */ bool somewhereMonotonicity(storm::analysis::Lattice* lattice) ; @@ -118,6 +114,8 @@ namespace storm { } private: + std::map>> checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + //TODO: variabele type std::map> analyseMonotonicity(uint_fast64_t i, Lattice* lattice, storm::storage::SparseMatrix matrix) ; @@ -139,13 +137,15 @@ namespace storm { bool validate; + bool checkSamples; + std::map> resultCheckOnSamples; LatticeExtender *extender; std::ofstream outfile; - std::string filename = "results.txt"; + std::string filename = "monotonicity.txt"; }; } } diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index 967d83ef8..e0c8c3bee 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -22,8 +22,9 @@ namespace storm { const std::string ParametricSettings::samplesGraphPreservingOptionName = "samples-graph-preserving"; const std::string ParametricSettings::sampleExactOptionName = "sample-exact"; const std::string ParametricSettings::monotonicityAnalysis = "monotonicity-analysis"; - const std::string ParametricSettings::sccElimination = "elim-scc"; - const std::string ParametricSettings::validateAssumptions = "validate-assumptions"; + const std::string ParametricSettings::sccElimination = "mon-elim-scc"; + const std::string ParametricSettings::validateAssumptions = "mon-validate-assumptions"; + const std::string ParametricSettings::samplesMonotonicityAnalysis = "mon-samples"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.") @@ -36,8 +37,11 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, samplesGraphPreservingOptionName, false, "Sets whether it can be assumed that the samples are graph-preserving.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, sampleExactOptionName, false, "Sets whether to sample using exact arithmetic.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").build()); this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples") + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build()); + } bool ParametricSettings::exportResultToFile() const { @@ -83,6 +87,10 @@ namespace storm { bool ParametricSettings::isValidateAssumptionsSet() const { return this->getOption(validateAssumptions).getHasOptionBeenSet(); } + + uint_fast64_t ParametricSettings::getNumberOfSamples() const { + return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger(); + } } // namespace modules } // namespace settings } // namespace storm diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 29cbb81bf..cbb740ec6 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -42,7 +42,7 @@ namespace storm { */ bool transformContinuousModel() const; - /* + /*! * Retrieves whether instead of model checking, only the wellformedness constraints should be obtained. */ bool onlyObtainConstraints() const; @@ -64,12 +64,26 @@ namespace storm { */ bool isSampleExactSet() const; + /*! + * Retrieves whether monotonicity analysis should be applied. + */ bool isMonotonicityAnalysisSet() const; - // TODO: maybe move to other place + + /*! + * Retrieves whether SCCs in the monotonicity analysis should be eliminated. + */ bool isSccEliminationSet() const; + /*! + * Retrieves whether assumptions in monotonicity analysis should be validated + */ bool isValidateAssumptionsSet() const; + /*! + * Retrieves the number of samples used for sampling in the monotonicity analysis + */ + uint_fast64_t getNumberOfSamples() const; + const static std::string moduleName; private: @@ -84,6 +98,7 @@ namespace storm { const static std::string monotonicityAnalysis; const static std::string sccElimination; const static std::string validateAssumptions; + const static std::string samplesMonotonicityAnalysis; }; } // namespace modules diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp index 5b9a4ebfb..27ba61483 100644 --- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -80,7 +80,7 @@ TEST(MonotonicityCheckerTest, Derivative_checker) { EXPECT_FALSE(functionRes.second); } -TEST(MonotonicityCheckerTest, Brp_with_bisimulation) { +TEST(MonotonicityCheckerTest, Brp_with_bisimulation_no_samples) { 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 @@ -111,6 +111,41 @@ TEST(MonotonicityCheckerTest, Brp_with_bisimulation) { EXPECT_EQ(1, result.size()); EXPECT_EQ(2, result.begin()->second.size()); auto monotone = result.begin()->second.begin(); - EXPECT_EQ(monotone->second.first, true); - EXPECT_EQ(monotone->second.second, false); + EXPECT_EQ(true, monotone->second.first); + EXPECT_EQ(false, monotone->second.second); +} + +TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) { + 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, 50); + auto result = monotonicityChecker.checkMonotonicity(); + EXPECT_EQ(1, result.size()); + EXPECT_EQ(2, result.begin()->second.size()); + auto monotone = result.begin()->second.begin(); + EXPECT_EQ(true, monotone->second.first); + EXPECT_EQ(false, monotone->second.second); }