From 4413259325832371b3598f448a1498c9063c091b Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 31 Aug 2012 09:26:37 +0000
Subject: [PATCH] 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 | 22 ++++++++++++++++++++-
 prism/src/explicit/MDPModelChecker.java  | 25 ++++++++++++++++++++++--
 prism/src/explicit/STPGModelChecker.java | 25 ++++++++++++++++++++++--
 3 files changed, 67 insertions(+), 5 deletions(-)

diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 9afa981e..c439f02d 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/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()) {
diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index 19814a83..d1534c05 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/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 {
diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java
index 579bf4fa..24937942 100644
--- a/prism/src/explicit/STPGModelChecker.java
+++ b/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 {