@@ -0,0 +1,2545 @@
+package de.bmoth.modelchecker.esmc;%0A%0Aimport de.bmoth.TestParser;%0Aimport de.bmoth.modelchecker.ModelCheckingResult;%0Aimport de.bmoth.modelchecker.StateSpaceNode;%0Aimport de.bmoth.parser.ast.nodes.MachineNode;%0Aimport org.junit.Before;%0Aimport org.junit.Test;%0A%0Aimport java.util.Set;%0A%0Aimport static org.junit.Assert.*;%0A%0Apublic class FullStateSpaceTest extends TestParser %7B%0A%0A    private MachineBuilder builder;%0A    private MachineNode machine;%0A    private ModelCheckingResult result;%0A%0A    @Before%0A    public void init() %7B%0A        builder = new MachineBuilder();%0A        machine = null;%0A        result = null;%0A    %7D%0A%0A    @Test%0A    public void testFullStateSpace1() %7B%0A        machine = builder%0A            .setName(%22SimpleMachine%22)%0A            .setSets(%22%22)%0A            .setVariables(%22x%22)%0A            .setInvariant(%22x:NATURAL%22)%0A            .setInitialization(%22x := 1%22)%0A            .addOperation(%22incSome = PRE x %3C 3 THEN x := x+1 END%22)%0A            .build();%0A%0A        result = new ExplicitStateModelChecker(machine).check();%0A        assertTrue(result.isCorrect());%0A        assertEquals(3, result.getSteps());%0A%0A        Set%3CStateSpaceNode%3E stateSpace = result.getStateSpaceRoot();%0A        assertEquals(1, stateSpace.size());%0A%0A        // as we have not added an LTL formula, each root node should be in the Buechi default node%0A        for (StateSpaceNode ssNode : stateSpace) %7B%0A            assertEquals(ssNode.getState().getBuechiNodes().size(), 1);%0A        %7D%0A    %7D%0A%0A    @Test%0A    public void testFullStateSpace1WithLTL() %7B%0A        machine = builder%0A            .setName(%22SimpleMachine%22)%0A            .setDefinitions(%22ASSERT_LTL_1 == %5C%22G %7Bx=2%7D%5C%22%22)%0A            .setSets(%22%22)%0A            .setVariables(%22x%22)%0A            .setInvariant(%22x:NATURAL%22)%0A            .setInitialization(%22x := 1%22)%0A            .addOperation(%22incSome = PRE x %3C 3 THEN x := x+1 END%22)%0A            .build();%0A%0A        result = new ExplicitStateModelChecker(machine).check();%0A        assertTrue(result.isCorrect());%0A        assertEquals(3, result.getSteps());%0A%0A        Set%3CStateSpaceNode%3E rootNodes = result.getStateSpaceRoot();%0A        assertEquals(1, rootNodes.size());%0A%0A        for (StateSpaceNode ssNode : rootNodes) %7B%0A            assertEquals(ssNode.getState().getBuechiNodes().size(), 1);%0A            Set%3CStateSpaceNode%3E successors = ssNode.getSuccessors();%0A            for (StateSpaceNode successor : successors) %7B%0A                assertNotEquals(ssNode.getState().getBuechiNodes().iterator().next(), successor.getState().getBuechiNodes().iterator().next());%0A            %7D%0A        %7D%0A    %7D%0A%7D%0A

add test case