From 70a48835ad0fdab892926231bb9ab5145f26426b Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 27 Aug 2015 12:51:39 +0000
Subject: [PATCH] Bug fix in CNF conversion (from Yuyang).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10596 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/BooleanUtils.java | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/prism/src/parser/BooleanUtils.java b/prism/src/parser/BooleanUtils.java
index 31e2ea27..3d92d182 100644
--- a/prism/src/parser/BooleanUtils.java
+++ b/prism/src/parser/BooleanUtils.java
@@ -32,8 +32,10 @@ import java.util.List;
 
 import parser.ast.Expression;
 import parser.ast.ExpressionBinaryOp;
+import parser.ast.ExpressionLiteral;
 import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
+import parser.type.TypeBool;
 import parser.visitor.ASTTraverseModify;
 import prism.PrismException;
 import prism.PrismLangException;
@@ -158,7 +160,13 @@ public class BooleanUtils
 		if (Expression.isNot(expr)) {
 			Expression neg = ((ExpressionUnaryOp) expr).getOperand();
 			// Boolean operators
-			if (Expression.isNot(neg)) {
+			if (Expression.isTrue(neg)) {
+				// ! true  ==  false
+				return new ExpressionLiteral(TypeBool.getInstance(), false);
+			} else if (Expression.isFalse(neg)) {
+				// ! false  ==  true
+				return new ExpressionLiteral(TypeBool.getInstance(), true);
+			} else if (Expression.isNot(neg)) {
 				Expression a = ((ExpressionUnaryOp) neg).getOperand();
 				// !(!a)  ==  a 
 				return doConversionToPositiveNormalForm(a, ltl);