From 7da07f7b99e91aad9044e42012746ae43438e7db Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 21 Aug 2015 00:27:51 +0000 Subject: [PATCH] Small refactor in positive normal form conversion. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10553 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/BooleanUtils.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/prism/src/parser/BooleanUtils.java b/prism/src/parser/BooleanUtils.java index 37e8c22f..e5c3183e 100644 --- a/prism/src/parser/BooleanUtils.java +++ b/prism/src/parser/BooleanUtils.java @@ -165,17 +165,17 @@ public class BooleanUtils } else if (Expression.isOr(neg)) { Expression a = ((ExpressionBinaryOp) neg).getOperand1(); Expression b = ((ExpressionBinaryOp) neg).getOperand2(); - Expression aNeg = Expression.Not(a); - Expression bNeg = Expression.Not(b); + Expression aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl); + Expression bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); // !(a | b) == !a & !b - return doConversionToPositiveNormalForm(Expression.And(aNeg, bNeg), ltl); + return Expression.And(aNeg, bNeg); } else if (Expression.isAnd(neg)) { Expression a = ((ExpressionBinaryOp) neg).getOperand1(); Expression b = ((ExpressionBinaryOp) neg).getOperand2(); - Expression aNeg = Expression.Not(a); - Expression bNeg = Expression.Not(b); + Expression aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl); + Expression bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); // !(a & b) == !a | !b - return doConversionToPositiveNormalForm(Expression.Or(aNeg, bNeg), ltl); + return Expression.Or(aNeg, bNeg); } // Temporal operators (if required) else if (ltl) {