Explicit model checker can handle negated path operators like G.

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

prism/src/explicit/DTMCModelChecker.java

@@ -63,9 +63,29 @@ public class DTMCModelChecker extends ProbModelChecker
 	{
 		StateValues probs = null;
 
+		// Negation/parentheses
+		if (expr instanceof ExpressionUnaryOp) {
+			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
+			// Parentheses
+			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
+				// Recurse
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand());
+			}
+			// Negation
+			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
+				// Compute, then subtract from 1 
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand());
+				probs.timesConstant(-1.0);
+				probs.plusConstant(1.0);
+			}
+		}
 		// Temporal operators
-		if (expr instanceof ExpressionTemporal) {
+		else if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			// Next
+			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
+				throw new PrismException("The explicit engine does not yet handle the next operator");
+			}
 			// Until
 			if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
 				if (exprTemp.hasBounds()) {

prism/src/explicit/MDPModelChecker.java

@@ -33,6 +33,7 @@ import java.util.Map;
 
 import parser.ast.Expression;
 import parser.ast.ExpressionTemporal;
+import parser.ast.ExpressionUnaryOp;
 import prism.PrismDevNullLog;
 import prism.PrismException;
 import prism.PrismFileLog;
@@ -68,11 +69,31 @@ public class MDPModelChecker extends ProbModelChecker
 	{
 		StateValues probs = null;
 
+		// Negation/parentheses
+		if (expr instanceof ExpressionUnaryOp) {
+			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
+			// Parentheses
+			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
+				// Recurse
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), min);
+			}
+			// Negation
+			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
+				// Compute, then subtract from 1 
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), !min);
+				probs.timesConstant(-1.0);
+				probs.plusConstant(1.0);
+			}
+		}
 		// Temporal operators
-		if (expr instanceof ExpressionTemporal) {
+		else if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			// Next
+			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
+				throw new PrismException("The explicit engine does not yet handle the next operator");
+			}
 			// Until
-			if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
+			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
 				if (exprTemp.hasBounds()) {
 					probs = checkProbBoundedUntil(model, exprTemp, min);
 				} else {

prism/src/explicit/STPGModelChecker.java

@@ -31,6 +31,7 @@ import java.util.*;
 
 import parser.ast.Expression;
 import parser.ast.ExpressionTemporal;
+import parser.ast.ExpressionUnaryOp;
 import prism.*;
 import explicit.rewards.STPGRewards;
 
@@ -62,11 +63,31 @@ public class STPGModelChecker extends ProbModelChecker
 	{
 		StateValues probs = null;
 
+		// Negation/parentheses
+		if (expr instanceof ExpressionUnaryOp) {
+			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
+			// Parentheses
+			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
+				// Recurse
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), min1, min2);
+			}
+			// Negation
+			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
+				// Compute, then subtract from 1 
+				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), !min1, !min2);
+				probs.timesConstant(-1.0);
+				probs.plusConstant(1.0);
+			}
+		}
 		// Temporal operators
-		if (expr instanceof ExpressionTemporal) {
+		else if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			// Next
+			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
+				throw new PrismException("The explicit engine does not yet handle the next operator");
+			}
 			// Until
-			if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
+			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
 				if (exprTemp.hasBounds()) {
 					probs = checkProbBoundedUntil(model, exprTemp, min1, min2);
 				} else {