@@ -0,0 +1,1931 @@
+package de.bmoth.backend.ltl.transformation;%0A%0Aimport de.bmoth.parser.ast.nodes.Node;%0Aimport de.bmoth.parser.ast.nodes.ltl.LTLInfixOperatorNode;%0Aimport de.bmoth.parser.ast.nodes.ltl.LTLNode;%0Aimport de.bmoth.parser.ast.nodes.ltl.LTLPrefixOperatorNode;%0Aimport de.bmoth.parser.ast.visitors.AbstractASTTransformation;%0A%0Apublic class ConvertNotUntil extends AbstractASTTransformation%7B%0A%0A%09@Override%0A%09public boolean canHandleNode(Node node) %7B%0A%09%09return node instanceof LTLPrefixOperatorNode;%0A%09%7D%0A%0A%09@Override%0A%09public Node transformNode(Node oldNode) %7B%0A%09%09LTLPrefixOperatorNode notOperator = (LTLPrefixOperatorNode) oldNode;%0A        if (notOperator.getKind() == LTLPrefixOperatorNode.Kind.NOT) %7B%0A            LTLNode argument = notOperator.getArgument();%0A            if (argument instanceof LTLInfixOperatorNode) %7B%0A            %09LTLInfixOperatorNode untilOperator = (LTLInfixOperatorNode) argument;%0A            %09%09if (untilOperator.getKind() == LTLInfixOperatorNode.Kind.UNTIL) %7B%0A            %09%09%09LTLPrefixOperatorNode untilsLeft = (LTLPrefixOperatorNode) untilOperator.getLeft();%0A            %09%09%09LTLPrefixOperatorNode untilsRight = (LTLPrefixOperatorNode) untilOperator.getRight();%0A            %09%09%09LTLPrefixOperatorNode notUntilsRight = new LTLPrefixOperatorNode(LTLPrefixOperatorNode.Kind.NOT, untilsRight);%0A            %09%09%09LTLInfixOperatorNode untilsLeftAndNotUntilsRight = new LTLInfixOperatorNode(LTLInfixOperatorNode.Kind.AND, untilsLeft, notUntilsRight);%0A            %09%09%09LTLPrefixOperatorNode notUntilsLeft = new LTLPrefixOperatorNode(LTLPrefixOperatorNode.Kind.NOT, untilsLeft);%0A            %09%09%09LTLInfixOperatorNode notUntilsLeftAndNotUntilsRight = new LTLInfixOperatorNode(LTLInfixOperatorNode.Kind.AND, notUntilsLeft, notUntilsRight);%0A            %09%09%09return new LTLInfixOperatorNode(LTLInfixOperatorNode.Kind.WEAK_UNTIL, untilsLeftAndNotUntilsRight, notUntilsLeftAndNotUntilsRight);%0A            %09%09%7D%0A            %7D%0A        %7D%0A%09%09return oldNode;%0A%09%7D%0A%0A%7D%0A

Convert Not until