@@ -0,0 +1,1664 @@
+package de.bmoth.modelchecker.kinduction;%0A%0Aimport de.bmoth.TestParser;%0Aimport de.bmoth.modelchecker.kind.KinductionModelChecker;%0Aimport de.bmoth.modelchecker.kind.KinductionModelCheckingResult;%0Aimport org.junit.Test;%0A%0Aimport static de.bmoth.modelchecker.kind.KinductionModelCheckingResult.Type.COUNTER_EXAMPLE_FOUND;%0Aimport static de.bmoth.modelchecker.kind.KinductionModelCheckingResult.Type.EXCEEDED_MAX_STEPS;%0Aimport static org.junit.Assert.assertEquals;%0A%0Apublic class KInductionModelCheckerTest extends TestParser %7B%0A%0A    @Test%0A    public void test1() %7B%0A        String machine = %22MACHINE infInc%5Cn%22 +%0A            %22VARIABLES c%5Cn%22 +%0A            %22INVARIANT c : NATURAL%5Cn%22 +%0A            %22INITIALISATION c := 0%5Cn%22 +%0A            %22OPERATIONS%5Cn%22 +%0A            %22%5Ctinc = BEGIN c := c + 1 END%5Cn%22 +%0A            %22END%5Cn%22;%0A%0A        KinductionModelCheckingResult result = new KinductionModelChecker(parseMachine(machine), 20).check();%0A        assertEquals(EXCEEDED_MAX_STEPS, result.getType());%0A    %7D%0A%0A    @Test%0A    public void test2() %7B%0A        String machine = %22MACHINE ebr%5Cn%22 +%0A            %22VARIABLES c, b%5Cn%22 +%0A            %22INVARIANT c : INTEGER &%5Cn%22 +%0A            %22%5Ctb = TRUE%5Cn%22 +%0A            %22INITIALISATION c := 0 %7C%7C b := TRUE%5Cn%22 +%0A            %22OPERATIONS%5Cn%22 +%0A            %22%5Ctinc = ANY x WHERE x:INTEGER THEN c := c + x END;%5Cn%22 +%0A            %22%5Cterr = PRE c %3E 99999 THEN b := FALSE END%5Cn%22 +%0A            %22END%5Cn%22;%0A%0A        KinductionModelCheckingResult result = new KinductionModelChecker(parseMachine(machine), 20).check();%0A        assertEquals(COUNTER_EXAMPLE_FOUND, result.getType());%0A        assertEquals(%22%7Bb=false, c=100000%7D%22, result.getLastState().toString());%0A    %7D%0A%7D%0A

add test cases for kinduction