Add 'runtime errors free' check to the CIF controller properties checker

Currently, all checks of the controller properties checker (whether MDD or BDD-based) suffer from wrong results if the model has runtime errors (such as x := x + 1 making x go out of bounds). This is documented in the tool's documentation, but still it would be better to address it properly.

With BDDs, we can easily check for runtime errors:

• Take into account runtime errors and variable ranges in the initialization predicate and transition relations (CIF/BDD edges).
  • Initialization: take initial, combine with and for each edge with its not error, combine with and for each variable of its range predicate.
  • Edges: update guard to guard and not error (this is currently done already in the CIF to BDD conversion, since #878 (closed))
  • Edges: update guard to guard and range_ok, computing range_ok for each edge, from the conjunction of the range predicates of the assigned variables, apply the edge backwards to that predicate to get the states from which you get to states in that range, and you have range_ok.
• Compute the reachable states (from initial states) from that initialization predicate, using those adapted edges, to get only the reachable states, without taking edges that would result in runtime errors.
• Check for runtime errors that can occur from the reachable states:
  • Compute for each edge: x = guard and (error or not range_ok), the condition under which a guard is enabled and would lead to a runtime error.
  • Check for each edge: reachable and x = false. If it doesn't hold, we've found states where transitions with runtime errors are possible.

This could be added as a new check. The other checks still produce wrong results then for models with runtime errors. This could also be prevented:

• Bounded response: do the same tricks for updated the edge guards, to not take any transitions with runtime errors. It would thus only consider what is reachable (in forward reachability and in bounded steps) by non-error-transitions. That is fine, since the 'runtime error free' check separately checks for runtime errors.
• Non-blocking under control: similarly could probably be adapted.
• Finite response: no longer relevant as bounded response replaces it (see also #893).
• Confluence: probably could be adapted as well, but maybe it becomes easier if we migrate it to being BDD-based as discussed in #695 (closed).

Addresses #892