Dealing with Expressions
As mentioned in #1 (closed), I have been taking a look at different ways in which we can sanity check our expressions. I'll summarize my findings here and then we can try to identify what exactly we need.
-
We can check if our property is either F or U by using
Expression.isSimplePathFormula()
. This will also return true if the expression is enclosed by parenthesis or if it is negated. In these cases we can follow the next two steps. -
If Expression is enclosed by parenthesis or negated, then
if (expr instanceof ExpressionUnaryOp) {
ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
// Parentheses
if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
// Call model check on exprUnary.getOperand()
}
else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
// Call model check on exprUnary.getOperand()
}
}
But I guess we had more to think about negation, and hence can ignore that part for now.
- Once we know that our expression is a simple path formula, we can use the
convertToUntilForm()
method fromExpressionTemporal
to get whatever we have as aP_U
expression then pass on both the operands to the explorer class.
@incaseoftrouble is this what you wanted to have or did I misunderstand?