s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Add conversion to positive normal form for LTL as well as boolean expressions. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10552 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
6f8b090ef0
commit
0c2e16ec32
1 changed files with 91 additions and 14 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 105
      prism/src/parser/BooleanUtils.java

105
prism/src/parser/BooleanUtils.java
View File

@ -32,6 +32,7 @@ import java.util.List;
import parser.ast.Expression;
import parser.ast.ExpressionBinaryOp;
import parser.ast.ExpressionTemporal;
import parser.ast.ExpressionUnaryOp;
import parser.visitor.ASTTraverseModify;
import prism.PrismException;
@ -86,7 +87,32 @@ public class BooleanUtils
public static Expression convertToPositiveNormalForm(Expression expr) throws PrismLangException
{
// First expand implies/iff/parentheses
Expression exprBool = (Expression) expr.accept(new ASTTraverseModify() {
// Then do conversion to +ve normal form
return doConversionToPositiveNormalForm(removeImpliesIffAndParentheses(expr), false);
}
/**
* Convert an LTL formula to positive normal form,
* i.e., remove any instances of =>, <=> or () and then push
* all negation inwards so that it only occurs on "propositions".
* A "proposition" is any Expression object that
* is not an operator used to define a Boolean expression (!, &, |, =>, <=>, ())
* or an temporal operator (X, U, F, G, R, W).
* The passed in expression is modified, and the result is returned.
*/
public static Expression convertLTLToPositiveNormalForm(Expression expr) throws PrismLangException
{
// First expand implies/iff/parentheses
// Then do conversion to +ve normal form
return doConversionToPositiveNormalForm(removeImpliesIffAndParentheses(expr), true);
}
/**
* Remove any instances of =>, <=> or () by expanding/deleting as appropriate.
*/
private static Expression removeImpliesIffAndParentheses(Expression expr) throws PrismLangException
{
return (Expression) expr.accept(new ASTTraverseModify() {
public Object visit(ExpressionUnaryOp e) throws PrismLangException
{
// Remove parentheses: (a)
@ -116,40 +142,83 @@ public class BooleanUtils
return super.visit(e);
}
});
// Then do conversion to +ve normal form
return doConversionToPositiveNormalForm(exprBool);
}
/**
* Do the main part of the conversion of a Boolean expression to positive normal form,
* i.e., push all negation inwards to the propositions. It is assumed that the Boolean expression
* comprises only the operators !, & and |. Anything else is treated as a proposition.
* i.e., push all negation inwards to the propositions. If {@code ltl} is false, it is assumed
* that the Boolean expression comprises only the Boolean operators !, & and |.
* If {@code ltl} is true, the expression can also contain temporal operators (X, U, F, G, R, W).
* Anything else is treated as a proposition.
* The passed in expression is modified, and the result is returned.
*/
private static Expression doConversionToPositiveNormalForm(Expression expr)
private static Expression doConversionToPositiveNormalForm(Expression expr, boolean ltl)
{
// Remove negation
if (Expression.isNot(expr)) {
Expression neg = ((ExpressionUnaryOp) expr).getOperand();
// Boolean operators
if (Expression.isNot(neg)) {
Expression a = ((ExpressionUnaryOp) neg).getOperand();
// !(!a) == a
return doConversionToPositiveNormalForm(a);
return doConversionToPositiveNormalForm(a, ltl);
} 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);
// !(a | b) == !a & !b
return doConversionToPositiveNormalForm(Expression.And(aNeg, bNeg));
return doConversionToPositiveNormalForm(Expression.And(aNeg, bNeg), ltl);
} 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);
// !(a & b) == !a | !b
return doConversionToPositiveNormalForm(Expression.Or(aNeg, bNeg));
return doConversionToPositiveNormalForm(Expression.Or(aNeg, bNeg), ltl);
}
// Temporal operators (if required)
else if (ltl) {
if (neg instanceof ExpressionTemporal) {
ExpressionTemporal exprTemp = (ExpressionTemporal) neg;
Expression a = exprTemp.getOperand1();
Expression b = exprTemp.getOperand2();
Expression aNeg = null, bNeg = null, aCopy = null, bNegCopy = null;
switch (exprTemp.getOperator()) {
case ExpressionTemporal.P_X:
bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
// !(X b) == X !b
return new ExpressionTemporal(ExpressionTemporal.P_X, null, bNeg);
case ExpressionTemporal.P_U:
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);
case ExpressionTemporal.P_F:
bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
// !(F b) == G !b
return new ExpressionTemporal(ExpressionTemporal.P_G, null, bNeg);
case ExpressionTemporal.P_G:
bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
// !(G b) == F !b
return new ExpressionTemporal(ExpressionTemporal.P_F, null, bNeg);
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));
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);
default:
// Don't change (shouldn't happen)
return expr;
}
}
} else {
// Proposition (negated)
return expr;
@ -157,16 +226,24 @@ public class BooleanUtils
}
// Preserve and
if (Expression.isAnd(expr)) {
Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1());
Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2());
Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1(), ltl);
Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2(), ltl);
return Expression.And(a, b);
}
// Preserve or
if (Expression.isOr(expr)) {
Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1());
Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2());
Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1(), ltl);
Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2(), ltl);
return Expression.Or(a, b);
}
// Preserve temporal operators
if (ltl && expr instanceof ExpressionTemporal) {
Expression a = ((ExpressionTemporal) expr).getOperand1();
Expression b = ((ExpressionTemporal) expr).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);
}
// Proposition
return expr;
}

Write Preview
Loading…
Cancel
Save