k/kernel/src/test/java/org/kframework/utils/PosetTest.java at dapphub · https-github-com-goodman-ops/k · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
// Copyright (c) 2014-2016 K Team. All Rights Reserved.
package org.kframework.utils;

import junit.framework.Assert;

import org.junit.Before;
import org.junit.Test;

import com.google.common.collect.Sets;

import java.util.List;

public class PosetTest {

    private Poset<String> poset;

    @Before
    public void setUp() {
        poset = Poset.create();
        poset.addRelation("Top", "A0");
        poset.addRelation("Top", "A1");
        poset.addRelation("Top", "A2");
        poset.addRelation("A0", "B0");
        poset.addRelation("A1", "B0");
        poset.addRelation("A2", "B0");
        poset.addRelation("A0", "B1");
        poset.addRelation("A1", "B1");
        poset.addRelation("A2", "B1");
        poset.addRelation("B0", "Bot");
        poset.addRelation("B1", "Bot");
        poset.transitiveClosure();
    }

    @Test
    public void testGetMaximalLowerBounds() throws Exception {
        Assert.assertEquals(Sets.newHashSet("B0", "B1"),
                poset.getMaximalLowerBounds(Sets.newHashSet("A0", "A1", "A2")));
    }

    @Test
    public void testGetMinimalUpperBounds() throws Exception {
        Assert.assertEquals(Sets.newHashSet("A0", "A1", "A2"),
                poset.getMinimalUpperBounds(Sets.newHashSet("B0", "B1")));
    }

    @Test
    public void testGetGLB() throws Exception {
        // multiple lower bounds, but no GLB
        Assert.assertNull(poset.getGLB(Sets.newHashSet("A0", "A1", "A2")));

        // create a GLB for A0, A1, and A2
        poset.addRelation("A0", "GLB");
        poset.addRelation("A1", "GLB");
        poset.addRelation("A2", "GLB");
        poset.addRelation("GLB", "B0");
        poset.addRelation("GLB", "B1");
        poset.transitiveClosure();
        Assert.assertEquals("GLB", poset.getGLB(Sets.newHashSet("A0", "A1", "A2")));
    }

    @Test
    public void testGetLUB() throws Exception {
        // multiple upper bounds, but no LUB
        Assert.assertNull(poset.getLUB(Sets.newHashSet("B0", "B1")));

        // create a LUB for B0, B1
        poset.addRelation("A0", "LUB");
        poset.addRelation("A1", "LUB");
        poset.addRelation("A2", "LUB");
        poset.addRelation("LUB", "B0");
        poset.addRelation("LUB", "B1");
        poset.transitiveClosure();
        Assert.assertEquals("LUB", poset.getLUB(Sets.newHashSet("B0", "B1")));
    }

    @Test
    public void testCircularity() throws Exception {
        poset.addRelation("S1", "S2");
        poset.addRelation("S2", "S1");
        List<String> circle = poset.checkForCycles();
        Assert.assertNotNull("The circuit should have 2 elements.", circle);
        Assert.assertEquals("The circuit should have 2 elements.", 2, circle.size());
    }
}