|
|
|
@ -298,28 +298,28 @@ public class ExpressionTemporal extends Expression |
|
|
|
// F a == true U a |
|
|
|
op1 = Expression.True(); |
|
|
|
exprTemp = new ExpressionTemporal(P_U, op1, operand2); |
|
|
|
exprTemp.setBoundsFrom(this); |
|
|
|
exprTemp.copyBoundsFrom(this); |
|
|
|
return exprTemp; |
|
|
|
case P_G: |
|
|
|
// G a == !(true U !a) |
|
|
|
op1 = Expression.True(); |
|
|
|
op2 = Expression.Not(operand2); |
|
|
|
exprTemp = new ExpressionTemporal(P_U, op1, op2); |
|
|
|
exprTemp.setBoundsFrom(this); |
|
|
|
exprTemp.copyBoundsFrom(this); |
|
|
|
return Expression.Not(exprTemp); |
|
|
|
case P_W: |
|
|
|
// a W b == !(a&!b U !a&!b) |
|
|
|
op1 = Expression.And(operand1, Expression.Not(operand2)); |
|
|
|
op2 = Expression.And(Expression.Not(operand1), Expression.Not(operand2)); |
|
|
|
exprTemp = new ExpressionTemporal(P_U, op1, op2); |
|
|
|
exprTemp.setBoundsFrom(this); |
|
|
|
exprTemp.copyBoundsFrom(this); |
|
|
|
return Expression.Not(exprTemp); |
|
|
|
case P_R: |
|
|
|
// a R b == !(!a U !b) |
|
|
|
op1 = Expression.Not(operand1); |
|
|
|
op2 = Expression.Not(operand2); |
|
|
|
exprTemp = new ExpressionTemporal(P_U, op1, op2); |
|
|
|
exprTemp.setBoundsFrom(this); |
|
|
|
exprTemp.copyBoundsFrom(this); |
|
|
|
return Expression.Not(exprTemp); |
|
|
|
} |
|
|
|
throw new PrismLangException("Cannot convert " + getOperatorSymbol() + " to until form"); |
|
|
|
|