diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 2d99dcc45..998a8481d 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -30,19 +30,32 @@ namespace storm { template std::map>> MonotonicityChecker::checkMonotonicity() { - bool maybeMonotone = true; + std::map> maybeMonotone; if (model->isOfType(storm::models::ModelType::Dtmc)) { - auto dtmcModel = model->as>(); - maybeMonotone = checkOnSamples(dtmcModel,3); - } //TODO mdp - if (maybeMonotone) { + auto dtmc = model->as>(); + maybeMonotone = checkOnSamples(dtmc,3); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + auto mdp = model->as>(); + maybeMonotone = checkOnSamples(mdp,3); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type."); + } + + bool allNotMonotone = true; + for (auto itr = maybeMonotone.begin(); itr != maybeMonotone.end(); ++itr) { + if (itr->second.first || itr->second.second) { + allNotMonotone = false; + } + } + + if (!allNotMonotone) { 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; + STORM_PRINT(std::endl << "Not monotone in all parameters" << std::endl); return result; } } @@ -86,15 +99,19 @@ namespace storm { STORM_PRINT("Result is constant" << std::endl); } else { for (auto itr2 = varsMonotone.begin(); itr2 != varsMonotone.end(); ++itr2) { - if (itr2->second.first) { - STORM_PRINT(" - Monotone increasing in: " << itr2->first << std::endl); + if (!resultCheckOnSamples[itr2->first].first && !resultCheckOnSamples[itr2->first].second) { + STORM_PRINT(" - Not monotone in: " << itr2->first << std::endl); } else { - STORM_PRINT(" - Do not know if monotone increasing in: " << itr2->first << std::endl); - } - if (itr2->second.second) { - STORM_PRINT(" - Monotone decreasing in: " << itr2->first << std::endl); - } else { - STORM_PRINT(" - Do not know if monotone decreasing in: " << itr2->first << std::endl); + if (itr2->second.first) { + STORM_PRINT(" - Monotone increasing in: " << itr2->first << std::endl); + } else { + STORM_PRINT(" - Do not know if monotone increasing in: " << itr2->first << std::endl); + } + if (itr2->second.second) { + STORM_PRINT(" - Monotone decreasing in: " << itr2->first << std::endl); + } else { + STORM_PRINT(" - Do not know if monotone decreasing in: " << itr2->first << std::endl); + } } } result.insert( @@ -118,13 +135,13 @@ namespace storm { 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 dtmc = model->as>(); + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, 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 mdp = model->as>(); + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], mdp, 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 { @@ -138,6 +155,8 @@ namespace storm { template std::map> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { + storm::utility::Stopwatch analyseWatch(true); + std::map> varsMonotone; std::ofstream myfile; std::string filename = "mc" + std::to_string(j) + ".dot"; @@ -165,47 +184,57 @@ namespace storm { auto val = first.getValue(); auto vars = val.gatherVariables(); for (auto itr = vars.begin(); itr != vars.end(); ++itr) { - if (varsMonotone.find(*itr) == varsMonotone.end()) { - varsMonotone[*itr].first = true; - varsMonotone[*itr].second = true; - } - std::pair* value = &varsMonotone.find(*itr)->second; - std::pair old = *value; - - for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) { - for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) { - auto derivative2 = (*itr2).second.derivative(*itr); - auto derivative3 = (*itr3).second.derivative(*itr); - STORM_LOG_THROW(derivative2.isConstant() && derivative3.isConstant(), storm::exceptions::NotSupportedException, "Expecting derivative to be constant"); - - auto compare = lattice->compare((*itr2).first, (*itr3).first); - - if (compare == storm::analysis::Lattice::ABOVE) { - // As the first state (itr2) is above the second state (itr3) it is sufficient to look at the derivative of itr2. - value->first &=derivative2.constantPart() >= 0; - value->second &=derivative2.constantPart() <= 0; - } else if (compare == storm::analysis::Lattice::BELOW) { - // As the second state (itr3) is above the first state (itr2) it is sufficient to look at the derivative of itr3. - value->first &=derivative3.constantPart() >= 0; - value->second &=derivative3.constantPart() <= 0; - } else if (compare == storm::analysis::Lattice::SAME) { - // Behaviour doesn't matter, as the states are at the same level. - } else { - // As the relation between the states is unknown, we can't claim anything about the monotonicity. - value->first = false; - value->second = false; + if (!resultCheckOnSamples[*itr].first && !resultCheckOnSamples[*itr].second) { + if (varsMonotone.find(*itr) == varsMonotone.end()) { + varsMonotone[*itr].first = false; + varsMonotone[*itr].second = false; + } + color = "color = red, "; + } else { + if (varsMonotone.find(*itr) == varsMonotone.end()) { + varsMonotone[*itr].first = true; + varsMonotone[*itr].second = true; + } + std::pair *value = &varsMonotone.find(*itr)->second; + std::pair old = *value; + + for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) { + for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) { + auto derivative2 = (*itr2).second.derivative(*itr); + auto derivative3 = (*itr3).second.derivative(*itr); + STORM_LOG_THROW(derivative2.isConstant() && derivative3.isConstant(), + storm::exceptions::NotSupportedException, + "Expecting derivative to be constant"); + + auto compare = lattice->compare((*itr2).first, (*itr3).first); + + if (compare == storm::analysis::Lattice::ABOVE) { + // As the first state (itr2) is above the second state (itr3) it is sufficient to look at the derivative of itr2. + value->first &= derivative2.constantPart() >= 0; + value->second &= derivative2.constantPart() <= 0; + } else if (compare == storm::analysis::Lattice::BELOW) { + // As the second state (itr3) is above the first state (itr2) it is sufficient to look at the derivative of itr3. + value->first &= derivative3.constantPart() >= 0; + value->second &= derivative3.constantPart() <= 0; + } else if (compare == storm::analysis::Lattice::SAME) { + // Behaviour doesn't matter, as the states are at the same level. + } else { + // As the relation between the states is unknown, we can't claim anything about the monotonicity. + value->first = false; + value->second = false; + } } } - } - if ((value->first != old.first) && (value->second != old.second)) { - color = "color = red, "; - } else if ((value->first != old.first)) { - myfile << "\t edge[style=dashed];" << std::endl; - color = "color = blue, "; - } else if ((value->second != old.second)) { - myfile << "\t edge[style=dotted];" << std::endl; - color = "color = blue, "; + if ((value->first != old.first) && (value->second != old.second)) { + color = "color = red, "; + } else if ((value->first != old.first)) { + myfile << "\t edge[style=dashed];" << std::endl; + color = "color = blue, "; + } else if ((value->second != old.second)) { + myfile << "\t edge[style=dotted];" << std::endl; + color = "color = blue, "; + } } } @@ -231,58 +260,151 @@ namespace storm { myfile << "\t}" << std::endl; myfile << "}" << std::endl; myfile.close(); + + analyseWatch.stop(); + STORM_PRINT(std::endl << "Time to check monotonicity based on the lattice: " << analyseWatch << "." << std::endl << std::endl); return varsMonotone; } template - bool MonotonicityChecker::checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples) { - bool monDecr = true; - bool monIncr = true; + std::map> MonotonicityChecker::checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples) { + storm::utility::Stopwatch samplesWatch(true); + + std::map> result; 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]; + std::set variables = storm::models::sparse::getProbabilityParameters(*model); + + for (auto itr = variables.begin(); itr != variables.end(); ++itr) { + double previous = -1; + bool monDecr = true; + bool monIncr = true; + + for (auto i = 0; i < numberOfSamples; ++i) { + auto valuation = storm::utility::parametric::Valuation(); + for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { + // Only change value for current variable + if ((*itr) == (*itr2)) { + auto val = std::pair( + (*itr2), storm::utility::convertNumber( + boost::lexical_cast((i + 1) / (double(numberOfSamples + 1))))); + valuation.insert(val); + } else { + auto val = std::pair( + (*itr2), storm::utility::convertNumber( + boost::lexical_cast((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; } - if (previous != -1) { - monDecr &= previous >= initial; - monIncr &= previous <= initial; + result.insert(std::pair>(*itr, std::pair(monIncr, monDecr))); + } + + samplesWatch.stop(); + STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); + resultCheckOnSamples = result; + return result; + } + + template + std::map> MonotonicityChecker::checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples) { + storm::utility::Stopwatch samplesWatch(true); + + std::map> result; + + auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Mdp>(*model); + auto matrix = model->getTransitionMatrix(); + std::set variables = storm::models::sparse::getProbabilityParameters(*model); + + for (auto itr = variables.begin(); itr != variables.end(); ++itr) { + double previous = -1; + bool monDecr = true; + bool monIncr = true; + + for (auto i = 0; i < numberOfSamples; ++i) { + auto valuation = storm::utility::parametric::Valuation(); + for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { + // Only change value for current variable + if ((*itr) == (*itr2)) { + auto val = std::pair( + (*itr2), storm::utility::convertNumber( + boost::lexical_cast((i + 1) / (double(numberOfSamples + 1))))); + valuation.insert(val); + } else { + auto val = std::pair( + (*itr2), storm::utility::convertNumber( + boost::lexical_cast((1) / (double(numberOfSamples + 1))))); + valuation.insert(val); + } + } + storm::models::sparse::Mdp sampleModel = instantiator.instantiate(valuation); + auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(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; } - previous = initial; + result.insert(std::pair>(*itr, std::pair(monIncr, monDecr))); } - bool result = monDecr || monIncr; + samplesWatch.stop(); + STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl); + resultCheckOnSamples = result; return result; } diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 81300897c..44676aa2c 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -48,13 +48,17 @@ namespace storm { std::map>> createLattice(); - bool checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); + std::map> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); + + std::map> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); std::shared_ptr model; std::vector> formulas; bool validate; + + std::map> resultCheckOnSamples; }; } }