@@ -0,0 +1,950 @@
+package de.bmoth.modelchecker;%0A%0Aimport com.microsoft.z3.Expr;%0Aimport de.bmoth.parser.Parser;%0Aimport de.bmoth.parser.ast.nodes.DeclarationNode;%0Aimport de.bmoth.parser.ast.nodes.MachineNode;%0Aimport org.junit.Test;%0A%0Aimport java.util.HashMap;%0Aimport java.util.List;%0A%0Aimport static org.junit.Assert.assertEquals;%0A%0Apublic class ModelCheckerTest %7B%0A    @Test%0A    public void testSimpleModelsWithoutOperations() throws Exception %7B%0A        String dir = %22src/test/resources/machines/%22;%0A%0A        MachineNode simpleMachineWithViolation = Parser.getMachineFileAsSemanticAst(dir + %22OnlyInitViolation.mch%22);%0A        boolean result = ModelChecker.doModelCheck(simpleMachineWithViolation);%0A        assertEquals(false, result);%0A%0A        MachineNode simpleMachineWithoutViolation = Parser.getMachineFileAsSemanticAst(dir + %22OnlyInitNoViolation.mch%22);%0A        result = ModelChecker.doModelCheck(simpleMachineWithoutViolation);%0A        assertEquals(true, result);%0A    %7D%0A%7D%0A

add first model checker test case :-)