From 99566fce6486c373a71c2d332bca75042601fc06 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 21 Jun 2011 20:06:47 +0000
Subject: [PATCH] Explicit model checker handles "and" directly, not via
 evaluate().

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3130 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/StateModelChecker.java | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 45a3f6ca..2a89595d 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -478,14 +478,20 @@ public class StateModelChecker
 	{
 		Object res;
 
+		// Binary ops
+		// (just "and" for now - more to come later)
+		if (expr instanceof ExpressionBinaryOp && Expression.isAnd(expr)) {
+			res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr);
+		}
 		// Literals
-		if (expr instanceof ExpressionLiteral) {
+		else if (expr instanceof ExpressionLiteral) {
 			res = checkExpressionLiteral(model, (ExpressionLiteral) expr);
 		}
 		// Labels
 		else if (expr instanceof ExpressionLabel) {
 			res = checkExpressionLabel(model, (ExpressionLabel) expr);
 		}
+		
 		// Anything else - just evaluate expression repeatedly
 		else if (expr.getType() instanceof TypeBool) {
 			int numStates = model.getNumStates();
@@ -520,6 +526,18 @@ public class StateModelChecker
 		return res;
 	}
 
+	/**
+	 * Model check a binary operator.
+	 */
+	protected Object checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr) throws PrismException
+	{
+		// (just "and" for now - more to come later)
+		BitSet res1bs = (BitSet) checkExpression(model, expr.getOperand1()); 
+		BitSet res2bs = (BitSet) checkExpression(model, expr.getOperand2());
+		res1bs.and(res2bs);
+		return res2bs;
+	}
+
 	/**
 	 * Model check a literal.
 	 */