Better error message for unsupported property in simplification of parametric model

[volkm]

When trying to analyze a parametric model with an unsupported formula the simplification throws an UnexpectedException here. It would be better to clearly indicate that the given formula is not supported. As I see it, we could either

1. convert the debug messages in the Simplifier to warnings,
2. throw an exception instead and capture it, or
3. try to continue with the original model if the simplification was not possible.

What would be the best way?

[sjunges]

@linusheck could you look into this please?

[linusheck]

"Who is responsible" for simplifying the model is inconsistent: for feasibility and monotonicity, this is done by storm-pars.cpp and cannot be disabled by the user:

// TODO: why only simplify in these modes
if (parametricSettings.getOperationMode() == storm::pars::utility::ParametricMode::Monotonicity ||
    parametricSettings.getOperationMode() == storm::pars::utility::ParametricMode::Feasibility) {
    STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidSettingsException, "Simplification requires property to be specified");
    result.model = storm::pars::simplifyModel<ValueType>(result.model, input);
    result.changed = true;
}

For partitioning, it is done by the parameter lifting model checkers and is configurable:

if (skipModelSimplification) {
    this->parametricModel = parametricModel;
    this->specifyFormula(env, checkTask);
} else {
    auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<SparseModelType>(*parametricModel);
    if (!simplifier.simplify(checkTask.getFormula())) {
        STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
    }
    this->parametricModel = simplifier.getSimplifiedModel();
    this->specifyFormula(env, checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
}

I think we should only have one place where simplification happens, either in storm-pars.cpp (I kind of prefer this) or in the methods themselves. Once it's configurable whether to simplify, I think Storm should throw an error if it is not supported instead of trying to continue with the original model. Returning false is fine but throwing an exception would also work.

[volkm]

In my view, simplifying the model should be optional as a pre-processing step and not be part of the method. I would also be in favor of simplifying the model in storm-pars. Maybe an even better idea would be to move the simplification to the api.

[sjunges]

I tend to agree with Matthias here, although I think that part of the simplification is actually bringing the model into a normal form -- which is not necessarily a general simplification and it may be rather method-specific. The general question may be: who is responsible for bringing the model into the right form such that it can be supported by an algorithm?

[linusheck]

The simplification is definitely method-specific and it can also be intransparent to the user when simplification is happening and when it isn't. For instance, when monotonicity tells me that the model is monotone at state 25, it's by default referring to the state of the simplified model, which might not be the same when I invoke a different method with default arguments.

[volkm]

Given your last example, I would be in favor of making the simplification a bit more transparent such that at least some traceability is given. Ideally we decouple a general simplification (which can usually be applied) from the method-specific simplifications (which are needed to obtain a normal form). I am not sure whether this is possible though and how much effort it would be.