Add support for negation of simple path formulae to parametric engine.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10211 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/param/ParamModelChecker.java

@@ -892,12 +892,27 @@ final public class ParamModelChecker extends PrismComponent
 	
 	private RegionValues checkProbPathFormulaSimple(ParamModel model, Expression expr, boolean min, BitSet needStates) throws PrismException
 	{
+		boolean negated = false;
 		RegionValues probs = null;
+		
+		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
+		
+		// Negation
+		if (expr instanceof ExpressionUnaryOp &&
+		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
+			negated = true;
+			expr = ((ExpressionUnaryOp)expr).getOperand();
+		}
+			
 		if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			
+			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
 				throw new PrismNotSupportedException("Next operator not supported by parametric engine");
-			} else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
+			}
+			// Until
+			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
 				BitSet needStatesInner = new BitSet(model.getNumStates());
 				needStatesInner.set(0, model.getNumStates());
 				RegionValues b1 = checkExpression(model, exprTemp.getOperand1(), needStatesInner);
@@ -908,10 +923,14 @@ final public class ParamModelChecker extends PrismComponent
 					probs = checkProbUntil(model, b1, b2, min, needStates);
 				}
 			}
-			// Anything else - convert to until and recurse
-			else {
-				probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), min, needStates);
-			}
+		}
+		
+		if (probs == null)
+			throw new PrismException("Unrecognised path operator in P operator");
+
+		if (negated) {
+			// Subtract from 1 for negation
+			probs = probs.binaryOp(new BigRational(1, 1), parserBinaryOpToRegionOp(ExpressionBinaryOp.MINUS));
 		}
 		
 		return probs;

prism/src/param/RegionValues.java

@@ -270,7 +270,18 @@ public final class RegionValues implements Iterable<Entry<Region, StateValues>>
 			RegionValues vals = region.binaryOp(op, values.get(region), pValue);
 			result.addAll(vals);
 		}
+		return result;
+	}
 
+	public RegionValues binaryOp(BigRational p, int op)
+	{
+		RegionValues result = new RegionValues(factory);
+		Function pFn = factory.getFunctionFactory().fromBigRational(p);
+		StateValues pValue = new StateValues(values.get(regions.get(0)).getNumStates(), factory.getInitialState(), pFn);
+		for (Region region : regions) {
+			RegionValues vals = region.binaryOp(op, pValue, values.get(region));
+			result.addAll(vals);
+		}
 		return result;
 	}