Handle reward bounded formulae without specified reward model

[AlexBork]

This PR extends Storm to handle reward bounded until formulae without an explicitly specified reward model, i.e. a formula of the form P=? [ "safe" Urew<3 "goal"]. In case the reward model is not unique, an error is thrown. This mirrors the behavior of the reward operator if no reward model is specified and simplifies property specification for models with unique reward models. In addition, the relevant parser test case is extended.