package de.bmoth.modelchecker;

import com.microsoft.z3.Expr;
import de.bmoth.parser.Parser;
import de.bmoth.parser.ast.nodes.DeclarationNode;
import de.bmoth.parser.ast.nodes.MachineNode;
import org.junit.Ignore;
import org.junit.Test;

import java.util.HashMap;
import java.util.List;

import static org.junit.Assert.assertEquals;

public class ModelCheckerTest {
    @Test
    public void testSimpleModelsWithoutOperations() throws Exception {
        String dir = "src/test/resources/machines/";

        MachineNode simpleMachineWithViolation = Parser.getMachineFileAsSemanticAst(dir + "OnlyInitViolation.mch");
        boolean result = ModelChecker.doModelCheck(simpleMachineWithViolation);
        assertEquals(false, result);

        MachineNode simpleMachineWithoutViolation = Parser.getMachineFileAsSemanticAst(dir + "OnlyInitNoViolation.mch");
        result = ModelChecker.doModelCheck(simpleMachineWithoutViolation);
        assertEquals(true, result);
    }

    @Test
    public void testSubstitution() throws Exception {
        String machine = "MACHINE test \n";
        machine += "VARIABLES x,y \n";
        machine += "INVARIANT x:NATURAL & y : NATURAL \n";
        machine += "INITIALISATION x,y:= 1,2 \n";
        machine += "END";
        MachineNode machineAsSemanticAst = Parser.getMachineAsSemanticAst(machine);
        ModelChecker.doModelCheck(machineAsSemanticAst);

        //TODO finish test
    }

    @Test
    public void testSimpleMachineWithOperations() throws Exception {
        String machine = "MACHINE SimpleMachine\n";
        machine += "VARIABLES x\n";
        machine += "INVARIANT x : NATURAL & x >= 0 & x <= 2\n";
        machine += "INITIALISATION x := 0\n";
        machine += "OPERATIONS\n";
        machine += "\tInc = SELECT x < 2 THEN x := x + 1 END;\n";
        machine += "\tDec = SELECT x > 0 THEN x := x - 1 END\n";
        machine += "END";

        boolean result = ModelChecker.doModelCheck(machine);
        assertEquals(true, result);
    }

    @Test
    public void testSimpleMachineWithOperations2() throws Exception {
        String machine = "MACHINE SimpleMachine\n";
        machine += "VARIABLES x\n";
        machine += "INVARIANT x : NATURAL & x >= 0 & x <= 2\n";
        machine += "INITIALISATION x := 0\n";
        machine += "OPERATIONS\n";
        machine += "\tBlockSubstitution = BEGIN x := x + 1 END\n";
        machine += "END";

        boolean result = ModelChecker.doModelCheck(machine);
        // the operation BlockSubstitution will finally violate the invariant x<=2
        assertEquals(false, result);
    }
}

@@ -36,110 +36,30 @@
 ort 
-com.microsoft.z3.Expr;%0Aimport de.bmoth.parser.Parser;%0Aimport de.bmoth.parser.ast.nodes.DeclarationNode
+de.bmoth.parser.Parser
 ;%0Aim
@@ -155,58 +155,8 @@
 t;%0A%0A
-import java.util.HashMap;%0Aimport java.util.List;%0A%0A
 impo
@@ -229,16 +229,74 @@
 rTest %7B%0A
+    private String dir = %22src/test/resources/machines/%22;%0A%0A
     @Tes
@@ -372,62 +372,8 @@
 n %7B%0A
-        String dir = %22src/test/resources/machines/%22;%0A%0A
     
@@ -2467,10 +2467,688 @@
 ;%0A    %7D%0A
+%0A    @Test%0A    public void testLeuschelPerformanceMachines1() throws Exception %7B%0A        MachineNode simpleMachineWithViolation = Parser.getMachineFileAsSemanticAst(dir + %22/performance/CounterErr.mch%22);%0A        boolean result = ModelChecker.doModelCheck(simpleMachineWithViolation);%0A        assertEquals(false, result);%0A    %7D%0A%0A    @Test%0A    @Ignore%0A    public void testLeuschelPerformanceMachines2() throws Exception %7B%0A        MachineNode simpleMachineWithoutViolation = Parser.getMachineFileAsSemanticAst(dir + %22/performance/SimpleSetIncrease.mch%22);%0A        boolean result = ModelChecker.doModelCheck(simpleMachineWithoutViolation);%0A        assertEquals(false, result);%0A    %7D%0A%0A
 %7D%0A

add machines from #9a1ea38 as JUnit tests, one currently skipped due to #12