Storm can almost model check weak until and release formulas. I see the following things missing for that (must not be part of this PR

[tquatmann]

Once #1055 is in place, it looks like Storm can almost model check weak until and release formulas using the LTL machinery. I see the following things missing for that

• Enable the new formulas in the pctlStar() FragmentSpecification so that the model checker's canHandle returns true for the new formulas.
• The FormulaParserGrammar should be extended, so we can also parse the formulas in PRISM-style; not sure if introducing W and R operators invalidates models that use W/R as variable or constant identifiers.
• Add proper tests

Originally posted by @tquatmann in #1055 (comment)