Description
Currently we create labels from expressions if these expressions are part of a given formula. For example, a formula P=? [F s=7 & d=2] adds a label ((s = 7) & (d = 2)) to the model. This means that a sparse model can have a label which might not be considered a "valid" label because it contains special characters.
Interestingly, a symbolic model never has such labels because the model checker keeps track of the expression and does not add a corresponding label.
If we do not export the labels stemming from formula expressions in the DRN format, this solves #705 but this is only one aspect of the problem. Stormpy for instance would still allow to access such labels and might lead to similar issues at some point.
My suggestion is to add a method which creates a "valid" label for an AtomicExpressionFormula and then add checks in addLabel() that labels have to be of the form [a-Z_][a-Z0-9_]*. This would align with the usual assumptions on label identifiers.
How to translate expressions to valid labels? We could for example use the hash of an AtomicExpressionFormula.