reworked checking whether parameter lifting is applicable

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, ConstantType>(FunctionValuation(std::move(simplifiedFunction), std::move(simplifiedValuation)), storm::utility::one<ConstantType>()));
-            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, ConstantType>(FunctionValuation(std::move(simplifiedFunction), std::move(simplifiedValuation)), storm::utility::one<ConstantType>()));
             return insertionRes.first->second;
         }
     

src/storm/utility/parameterlifting.h

@@ -1,11 +1,15 @@
 #ifndef STORM_UTILITY_PARAMETERLIFTING_H
 #define STORM_UTILITY_PARAMETERLIFTING_H
 
+#include <vector>
+
 #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<typename ValueType>
-            static bool validateParameterLiftingSound(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula) {
-                switch (model.getType()) {
-                    default:
+            static bool validateParameterLiftingSound(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<storm::logic::Formula const> 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<storm::models::sparse::MarkovAutomaton<ValueType>>()->isClosed()) {
+                        STORM_LOG_ERROR("parameter lifting requires a closed Markov automaton.");
                         return false;
+                    }
+                    auto const& rateVector = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates();
+                    auto const& markovianStates = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->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<ValueType> 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<typename storm::utility::parametric::VariableType<ValueType>::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<typename storm::utility::parametric::VariableType<ValueType>::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;
             }
             
         }

src/storm/utility/storm.h

@@ -326,7 +326,7 @@ namespace storm {
         storm::utility::Stopwatch parameterLiftingStopWatch(true);
         std::shared_ptr<storm::logic::Formula const> 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...");