Better treatment of Boolean literals in LTL formulas.

[tquatmann]

When checking LTL formulas like G (true U a), the true is somehow replaced by a fresh atomic proposition before feeding it into spot. This potentially yields unnecessarily large automata.

Obviously, this should be avoided.

[kleinj]

Should be quite easy, just add special casing/direct return for BooleanLiteralFormula at the start of https://github.com/moves-rwth/storm/blob/f37f477bc9995b9fa566dda20dd954e293497944/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp#L180

In PRISM, we have some additional logic that looks at the actual satisfying state sets for the maximal state subformulas and convert to true/false if the set covers all states of the model or is empty, respectively. In Storm, this info is not as easily available at that point of conversion...