Use reachability reward computation for complex state formulas

E.g., R=?[ F (a & A[F b])] was previously handled via co-safety, as
the operand of the F operator is not a proposition.

prism/src/explicit/ProbModelChecker.java

@@ -1123,7 +1123,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardPathFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
-		if (Expression.isReach(expr)) {
+		if (Expression.isReachWithStateFormula(expr)) {
 			return checkRewardReach(model, modelRewards, (ExpressionTemporal) expr, minMax, statesOfInterest);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr, true)) {

prism/src/param/ParamModelChecker.java

@@ -1081,7 +1081,7 @@ final public class ParamModelChecker extends PrismComponent
 	 */
 	private RegionValues checkRewardPathFormula(ParamModel model, ParamRewardStruct rew, Expression expr, boolean min, BitSet needStates) throws PrismException
 	{
-		if (Expression.isReach(expr)) {
+		if (Expression.isReachWithStateFormula(expr)) {
 			return checkRewardReach(model, rew, (ExpressionTemporal) expr, min, needStates);
 		} else if (Expression.isCoSafeLTLSyntactic(expr, true)) {
 			throw new PrismNotSupportedException(mode.Engine() + " does not yet support co-safe reward computation");

prism/src/prism/NondetModelChecker.java

@@ -1415,7 +1415,7 @@ public class NondetModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
-		if (Expression.isReach(expr)) {
+		if (Expression.isReachWithStateFormula(expr)) {
 			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min, statesOfInterest);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr, true)) {

prism/src/prism/ProbModelChecker.java

@@ -906,7 +906,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
-		if (Expression.isReach(expr)) {
+		if (Expression.isReachWithStateFormula(expr)) {
 			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, statesOfInterest);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr, true)) {