package de.bmoth.modelchecker.ltl;

import de.bmoth.TestParser;
import de.bmoth.modelchecker.ModelCheckingResult;
import de.bmoth.modelchecker.esmc.ExplicitStateModelChecker;
import de.bmoth.parser.ast.nodes.MachineNode;
import org.junit.Before;
import org.junit.Test;

import static org.junit.Assert.*;

public class LTLModelCheckerTest extends TestParser {

    private MachineBuilder builder;
    private MachineNode machine;
    private ModelCheckingResult result;

    @Before
    public void init() {
        builder = new MachineBuilder();
        machine = null;
        result = null;
    }

    @Test
    public void testObviouslyBrokenProperty() {
        machine = builder
            .setName("CorrectCounter")
            .setDefinitions("ASSERT_LTL_1 == \"G({0=1})\"")
            .setSets("")
            .setVariables("c")
            .setInvariant("c:NAT")
            .setInitialization("c := 0")
            .addOperation("inc = PRE c < 2 THEN c:=c+1 END")
            .addOperation("reset = c:=0")
            .build();

        result = new ExplicitStateModelChecker(machine).check();
        assertFalse(result.isCorrect());
        assertEquals(3, result.getSteps());
    }

    @Test
    public void testObviouslyCorrectProperty() {
        machine = builder
            .setName("CorrectCounter")
            .setDefinitions("ASSERT_LTL_1 == \"G {1=1}\"")
            .setSets("")
            .setVariables("c")
            .setInvariant("c:NAT")
            .setInitialization("c := 0")
            .addOperation("inc = PRE c < 2 THEN c:=c+1 END")
            .addOperation("reset = c:=0")
            .build();

        result = new ExplicitStateModelChecker(machine).check();
        assertTrue(result.isCorrect());
        assertEquals(3, result.getSteps());
    }

    @Test
    public void testCorrectCounter() {
        machine = builder
            .setName("CorrectCounter")
            .setDefinitions("ASSERT_LTL_1 == \"G {c<5}\"")
            .setSets("")
            .setVariables("c")
            .setInvariant("c:NAT")
            .setInitialization("c := 0")
            .addOperation("inc = PRE c < 2 THEN c:=c+1 END")
            .addOperation("reset = c:=0")
            .build();

        result = new ExplicitStateModelChecker(machine).check();
        assertTrue(result.isCorrect());
        assertEquals(3, result.getSteps());
    }

    @Test
    public void testBrokenCounter() {
        machine = builder
            .setName("BrokenCounter")
            .setDefinitions("ASSERT_LTL_1 == \"G X {c<0}\"")
            .setSets("")
            .setVariables("c")
            .setInvariant("c:NAT")
            .setInitialization("c := 0")
            .addOperation("inc = PRE c < 2 THEN c:=c+1 END")
            .addOperation("reset = c:=0")
            .build();

        result = new ExplicitStateModelChecker(machine).check();
        assertFalse(result.isCorrect());
        assertEquals(3, result.getSteps());
    }
}

@@ -2480,32 +2480,626 @@
 BrokenCounter%22)%0A
+            .setDefinitions(%22ASSERT_LTL_1 == %5C%22G %7Bc%3C0%7D%5C%22%22)%0A            .setSets(%22%22)%0A            .setVariables(%22c%22)%0A            .setInvariant(%22c:NAT%22)%0A            .setInitialization(%22c := 0%22)%0A            .addOperation(%22inc = PRE c %3C 2 THEN c:=c+1 END%22)%0A            .addOperation(%22reset = c:=0%22)%0A            .build();%0A%0A        result = new ExplicitStateModelChecker(machine).check();%0A        assertFalse(result.isCorrect());%0A        assertEquals(3, result.getSteps());%0A    %7D%0A%0A    @Test%0A    public void testBrokenCounterWithNext() %7B%0A        machine = builder%0A            .setName(%22BrokenCounter%22)%0A
             .set

add LTL test case without next