From f49ccb3ad92c7b911f3a565e6fafada4649cc9fe Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 22 Mar 2018 18:45:39 +0100 Subject: [PATCH] BooleanUtils.doConversionToPositiveNormalForm: take temporal operator bounds into account The formula may have bounds attached to the temporal operators, so we strive to preserve them. Dualizing the operators does not change the bounds, so we can just attach them (see ExpressionTemporal.convertToUntilForm()) to the new temporal operator. --- prism/src/parser/BooleanUtils.java | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/prism/src/parser/BooleanUtils.java b/prism/src/parser/BooleanUtils.java index c75778f5..4c181261 100644 --- a/prism/src/parser/BooleanUtils.java +++ b/prism/src/parser/BooleanUtils.java @@ -200,6 +200,7 @@ public class BooleanUtils Expression a = exprTemp.getOperand1(); Expression b = exprTemp.getOperand2(); Expression aNeg = null, bNeg = null, aCopy = null, bNegCopy = null; + ExpressionTemporal result = null; switch (exprTemp.getOperator()) { case ExpressionTemporal.P_X: bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); @@ -209,27 +210,37 @@ public class BooleanUtils aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl); bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); // !(a U b) == !a R !b - return new ExpressionTemporal(ExpressionTemporal.P_R, aNeg, bNeg); + result = new ExpressionTemporal(ExpressionTemporal.P_R, aNeg, bNeg); + result.setBoundsFrom(exprTemp); + return result; case ExpressionTemporal.P_F: bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); // !(F b) == G !b - return new ExpressionTemporal(ExpressionTemporal.P_G, null, bNeg); + result = new ExpressionTemporal(ExpressionTemporal.P_G, null, bNeg); + result.setBoundsFrom(exprTemp); + return result; case ExpressionTemporal.P_G: bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); // !(G b) == F !b - return new ExpressionTemporal(ExpressionTemporal.P_F, null, bNeg); + result = new ExpressionTemporal(ExpressionTemporal.P_F, null, bNeg); + result.setBoundsFrom(exprTemp); + return result; case ExpressionTemporal.P_W: aCopy = doConversionToPositiveNormalForm(a.deepCopy(), ltl); bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl); bNegCopy = doConversionToPositiveNormalForm(Expression.Not(b.deepCopy()), ltl); // !(a W b) == a&!b U !a&!b - return new ExpressionTemporal(ExpressionTemporal.P_R, Expression.And(aCopy, bNeg), Expression.And(aNeg, bNegCopy)); + result = new ExpressionTemporal(ExpressionTemporal.P_R, Expression.And(aCopy, bNeg), Expression.And(aNeg, bNegCopy)); + result.setBoundsFrom(exprTemp); + return result; case ExpressionTemporal.P_R: aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl); bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl); // !(a R b) == !a U !b - return new ExpressionTemporal(ExpressionTemporal.P_U, aNeg, bNeg); + result = new ExpressionTemporal(ExpressionTemporal.P_U, aNeg, bNeg); + result.setBoundsFrom(exprTemp); + return result; default: // Don't change (shouldn't happen) return expr; @@ -254,11 +265,14 @@ public class BooleanUtils } // Preserve temporal operators if (ltl && expr instanceof ExpressionTemporal) { - Expression a = ((ExpressionTemporal) expr).getOperand1(); - Expression b = ((ExpressionTemporal) expr).getOperand2(); + ExpressionTemporal exprTemp = (ExpressionTemporal)expr; + Expression a = exprTemp.getOperand1(); + Expression b = exprTemp.getOperand2(); Expression aConv = (a == null) ? null : doConversionToPositiveNormalForm(a, ltl); Expression bConv = (b == null) ? null : doConversionToPositiveNormalForm(b, ltl); - return new ExpressionTemporal(((ExpressionTemporal) expr).getOperator(), aConv, bConv); + ExpressionTemporal result = new ExpressionTemporal(exprTemp.getOperator(), aConv, bConv); + result.setBoundsFrom(exprTemp); + return result; } // Proposition return expr;