Implicit preconditions for states

[treiher]

The disjunction of all incoming transitions should be considered as implicit precondition for states. The state transitions and the corresponding conditions must be represented in the generated state machine, so that the preconditions can be shown by SPARK. It probably makes sense to add the determination of these implicit preconditions to the model, so that this information can also be used for the verification of the session model (#633).