From 9425d3506eb01449dadfb538ed369904ba3bf54f Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 5 Apr 2017 15:19:12 +0200 Subject: [PATCH] reworked checking whether parameter lifting is applicable --- src/storm/transformer/ParameterLifter.cpp | 5 +- src/storm/utility/parameterlifting.h | 117 +++++++++++++++++++++- src/storm/utility/storm.h | 2 +- 3 files changed, 115 insertions(+), 9 deletions(-) diff --git a/src/storm/transformer/ParameterLifter.cpp b/src/storm/transformer/ParameterLifter.cpp index ffd2d1bd5..829631cff 100644 --- a/src/storm/transformer/ParameterLifter.cpp +++ b/src/storm/transformer/ParameterLifter.cpp @@ -245,11 +245,8 @@ namespace storm { storm::utility::parametric::gatherOccurringVariables(simplifiedFunction, variablesInFunction); AbstractValuation simplifiedValuation = valuation.getSubValuation(variablesInFunction); // insert the function and the valuation - auto insertionRes = collectedFunctions.insert(std::pair(FunctionValuation(std::move(simplifiedFunction), std::move(simplifiedValuation)), storm::utility::one())); - if(insertionRes.second) { - STORM_LOG_WARN_COND(storm::utility::parametric::isMultiLinearPolynomial(insertionRes.first->first.first), "Parameter lifting for non-multilinear polynomial " << insertionRes.first->first.first << " invoked. This might not be sound..."); - } //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. + auto insertionRes = collectedFunctions.insert(std::pair(FunctionValuation(std::move(simplifiedFunction), std::move(simplifiedValuation)), storm::utility::one())); return insertionRes.first->second; } diff --git a/src/storm/utility/parameterlifting.h b/src/storm/utility/parameterlifting.h index f2cf58972..11ae11962 100644 --- a/src/storm/utility/parameterlifting.h +++ b/src/storm/utility/parameterlifting.h @@ -1,11 +1,15 @@ #ifndef STORM_UTILITY_PARAMETERLIFTING_H #define STORM_UTILITY_PARAMETERLIFTING_H +#include + #include "storm/models/sparse/Model.h" #include "storm/utility/parametric.h" #include "storm/utility/macros.h" #include "storm/logic/Formula.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" namespace storm { @@ -16,18 +20,123 @@ namespace storm { * Checks whether the parameter lifting approach is sound on the given model with respect to the provided property * * This method is taylored to an efficient but incomplete check, i.e., if false is returned, - * parameter lifting might still be applicable. Checking this, however, would be more involved. + * parameter lifting might still be applicable. + * + * More precisely, we only check if the occurring functions are multilinear polynomials. + * However, Parameter Lifting also works for fractions of multilinear polynomials where for every state s, + * every probability and reward occurring at s have the same denominator. * * @param model * @param formula * @return true iff it was successfully validated that parameter lifting is sound on the provided model. */ template - static bool validateParameterLiftingSound(storm::models::sparse::Model const& model, storm::logic::Formula const& formula) { - switch (model.getType()) { - default: + static bool validateParameterLiftingSound(std::shared_ptr> const& model, std::shared_ptr const& formula) { + + // Check whether all numbers occurring in the model are multilinear + + // Transition matrix + if (model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::Ctmc)) { + for (auto const& entry : model->getTransitionMatrix()) { + if (!storm::utility::parametric::isMultiLinearPolynomial(entry.getValue())) { + STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model."); + return false; + } + } + } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + // Markov Automata store the probability matrix and the exit rate vector. However, we need to considert the rate matrix. + if (model->template as>()->isClosed()) { + STORM_LOG_ERROR("parameter lifting requires a closed Markov automaton."); return false; + } + auto const& rateVector = model->template as>()->getExitRates(); + auto const& markovianStates = model->template as>()->getMarkovianStates(); + for (uint_fast64_t state = 0; state < model->getNumberOfStates(); ++state) { + if (markovianStates.get(state)) { + auto const& exitRate = rateVector[state]; + for (auto const& entry : model->getTransitionMatrix().getRowGroup(state)) { + if (!storm::utility::parametric::isMultiLinearPolynomial(storm::utility::simplify(entry.getValue() * exitRate))) { + STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model."); + return false; + } + } + } else { + for (auto const& entry : model->getTransitionMatrix().getRowGroup(state)) { + if (!storm::utility::parametric::isMultiLinearPolynomial(entry.getValue())) { + STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model."); + return false; + } + } + } + } + } else { + STORM_LOG_ERROR("Unsupported model type for parameter lifting."); + return false; + } + + // Rewards + if (formula->isRewardOperatorFormula()) { + storm::models::sparse::StandardRewardModel const& rewardModel = formula->asRewardOperatorFormula().hasRewardModelName() ? + model->getRewardModel(formula->asRewardOperatorFormula().getRewardModelName()) : + model->getUniqueRewardModel(); + if (rewardModel.hasStateRewards()) { + for (auto const& rew : rewardModel.getStateRewardVector()) { + if (!storm::utility::parametric::isMultiLinearPolynomial(rew)) { + STORM_LOG_WARN("The input model contains a non-linear polynomial as state reward: '" << rew << "'. Can not validate that parameter lifting is sound on this model."); + return false; + } + } + } + // Parameters in transition rewards (and for continuous time models also action rewards) have to be disjoint from the probability/rate parameters. + // Note: This check could also be done action-wise. + std::set::type> collectedRewardParameters; + if (rewardModel.hasStateActionRewards()) { + if (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + for (auto const& rew : rewardModel.getStateActionRewardVector()) { + if (!storm::utility::parametric::isMultiLinearPolynomial(rew)) { + STORM_LOG_WARN("The input model contains a non-linear polynomial as action reward: '" << rew << "'. Can not validate that parameter lifting is sound on this model."); + return false; + } + storm::utility::parametric::gatherOccurringVariables(rew, collectedRewardParameters); + } + } else { + for (auto const& rew : rewardModel.getStateActionRewardVector()) { + if (!storm::utility::parametric::isMultiLinearPolynomial(rew)) { + STORM_LOG_WARN("The input model contains a non-linear polynomial as action reward: '" << rew << "'. Can not validate that parameter lifting is sound on this model."); + return false; + } + } + } + } + + if (rewardModel.hasTransitionRewards()) { + for (auto const& rewEntry : rewardModel.getTransitionRewardMatrix()) { + if (!storm::utility::parametric::isMultiLinearPolynomial(rewEntry.getValue())) { + STORM_LOG_WARN("The input model contains a non-linear polynomial as transition reward: '" << rewEntry.getValue() << "'. Can not validate that parameter lifting is sound on this model."); + return false; + } + storm::utility::parametric::gatherOccurringVariables(rewEntry.getValue(), collectedRewardParameters); + } + } + + if (!collectedRewardParameters.empty()) { + std::set::type> transitionParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParIt = collectedRewardParameters.begin(); + auto trParIt = transitionParameters.begin(); + while (rewParIt != collectedRewardParameters.end() && trParIt != transitionParameters.end()) { + if (*rewParIt == *trParIt) { + STORM_LOG_WARN("Parameter " << *trParIt << " occurs in a transition probability/rate and in a transition/action reward. Parameter lifting might not be sound on this model."); + return false; + } + if (*rewParIt < *trParIt) { + ++rewParIt; + } else { + ++trParIt; + } + } + } } + return true; } } diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index f9830ff98..ed75cba48 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -326,7 +326,7 @@ namespace storm { storm::utility::Stopwatch parameterLiftingStopWatch(true); std::shared_ptr consideredFormula = formula; - STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*markovModel, *formula), "Could not validate whether parameter lifting is sound on the input model and the formula " << *formula); + STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(markovModel, formula), "Could not validate whether parameter lifting is sound on the input model and the formula " << *formula); if (markovModel->isOfType(storm::models::ModelType::Ctmc) || markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_PRINT_AND_LOG("Transforming continuous model to discrete model...");