package de.bmoth.ltl;

import de.bmoth.backend.ltl.LTLTransformations;
import de.bmoth.parser.Parser;
import de.bmoth.parser.ParserException;
import de.bmoth.parser.ast.nodes.ltl.LTLFormula;
import de.bmoth.parser.ast.nodes.ltl.LTLNode;
import org.junit.Test;

import static org.junit.Assert.assertEquals;

public class LTLTransformationTest {

    @Test
    public void testTransformation1() throws ParserException {
        String formula = "not(G { 1=1 })";
        LTLFormula ltlFormula = Parser.getLTLFormulaAsSemanticAst(formula);
        LTLNode node1 = LTLTransformations.transformLTLNode(ltlFormula.getLTLNode());
        assertEquals("FINALLY(NOT(EQUAL(1,1)))", node1.toString());
    }

    @Test
    public void testTransformation2() throws ParserException {
        String formula = "not(GG { 1=1 })";
        LTLFormula ltlFormula = Parser.getLTLFormulaAsSemanticAst(formula);
        LTLNode node1 = LTLTransformations.transformLTLNode(ltlFormula.getLTLNode());
        assertEquals("FINALLY(NOT(EQUAL(1,1)))", node1.toString());
    }

    @Test
    public void testTransformation3() throws ParserException {
        String formula = "G not(E { 1=1 })";
        LTLFormula ltlFormula = Parser.getLTLFormulaAsSemanticAst(formula);
        LTLNode node1 = LTLTransformations.transformLTLNode(ltlFormula.getLTLNode());
        assertEquals("GLOBALLY(NOT(EQUAL(1,1)))", node1.toString());
    }

    @Test
    public void testTransformation4() throws ParserException {
        String formula = "{1=1} U ({1=1} U {2=2})";
        LTLFormula ltlFormula = Parser.getLTLFormulaAsSemanticAst(formula);
        LTLNode node1 = LTLTransformations.transformLTLNode(ltlFormula.getLTLNode());
        assertEquals("UNTIL(EQUAL(1,1),EQUAL(2,2))", node1.toString());
    }

    @Test
    public void testTransformation5() throws ParserException {
        String formula = "({1=1} U {2=2}) U {2=2}";
        LTLFormula ltlFormula = Parser.getLTLFormulaAsSemanticAst(formula);
        LTLNode node1 = LTLTransformations.transformLTLNode(ltlFormula.getLTLNode());
        assertEquals("UNTIL(EQUAL(1,1),EQUAL(2,2))", node1.toString());
    }
}

@@ -135,16 +135,72 @@
 eption;%0A
+import de.bmoth.parser.ast.nodes.ltl.LTLBPredicateNode;%0A
 import d
@@ -282,24 +282,109 @@
 tl.LTLNode;%0A
+import de.bmoth.parser.ast.nodes.ltl.LTLPrefixOperatorNode;%0Aimport org.junit.Ignore;%0A
 import org.j
@@ -439,16 +439,59 @@
 tEquals;
+%0Aimport static org.junit.Assert.assertTrue;
 %0A%0Apublic
@@ -2315,11 +2315,714 @@
 );%0A    %7D
+%0A%0A    @Test%0A    @Ignore%0A    public void testTransformation6() throws ParserException %7B%0A        String formula = %22not(G %7B 1=1 %7D)%22;%0A        LTLFormula ltlFormula = Parser.getLTLFormulaAsSemanticAst(formula);%0A        LTLNode node1 = LTLTransformations.transformLTLNode(ltlFormula.getLTLNode());%0A%0A        assertEquals(%22FINALLY(NOT(EQUAL(1,1)))%22, node1.toString());%0A%0A        // check if we have the B not, not the LTL not%0A        assertTrue(node1 instanceof LTLPrefixOperatorNode);%0A        LTLPrefixOperatorNode node1PO = (LTLPrefixOperatorNode) node1;%0A        assertEquals(LTLPrefixOperatorNode.Kind.FINALLY, node1PO.getKind());%0A%0A        assertTrue(node1PO.getArgument() instanceof LTLBPredicateNode);%0A    %7D
 %0A%7D%0A

add test verifying if LTL not is pushed into the B predicate