|
16 | 16 | package net.automatalib.automata.vpda;
|
17 | 17 |
|
18 | 18 | import java.util.Collections;
|
| 19 | +import java.util.HashSet; |
19 | 20 |
|
| 21 | +import net.automatalib.automata.vpda.AbstractOneSEVPA.SevpaViewEdge; |
| 22 | +import net.automatalib.graphs.Graph; |
20 | 23 | import net.automatalib.words.Alphabet;
|
21 | 24 | import net.automatalib.words.VPDAlphabet;
|
22 | 25 | import net.automatalib.words.Word;
|
@@ -61,4 +64,95 @@ public void testBracketLanguage() {
|
61 | 64 | Assert.assertFalse(vpda.accepts(Word.fromCharSequence(")(")));
|
62 | 65 | Assert.assertFalse(vpda.accepts(Word.fromCharSequence("()()")));
|
63 | 66 | }
|
| 67 | + |
| 68 | + /** |
| 69 | + * Test case for reported issue <a href="https://github.com/LearnLib/automatalib/pull/39">#39</a>. |
| 70 | + */ |
| 71 | + @Test |
| 72 | + public void testGraphRepresentation() { |
| 73 | + |
| 74 | + final Alphabet<Integer> callAlphabet = Alphabets.integers(1, 10); |
| 75 | + final Alphabet<Integer> internalAlphabet = Alphabets.integers(11, 20); |
| 76 | + final Alphabet<Integer> returnAlphabet = Alphabets.integers(21, 30); |
| 77 | + final VPDAlphabet<Integer> alphabet = new DefaultVPDAlphabet<>(internalAlphabet, callAlphabet, returnAlphabet); |
| 78 | + |
| 79 | + // create arbitrary VPA |
| 80 | + final DefaultOneSEVPA<Integer> vpa = new DefaultOneSEVPA<>(alphabet); |
| 81 | + final Location init = vpa.addInitialLocation(false); |
| 82 | + final Location accepting = vpa.addLocation(true); |
| 83 | + |
| 84 | + // criss-cross internal successors |
| 85 | + for (final Integer i : internalAlphabet) { |
| 86 | + final Location initSucc; |
| 87 | + final Location accSucc; |
| 88 | + |
| 89 | + if (i % 2 == 0) { |
| 90 | + initSucc = init; |
| 91 | + accSucc = accepting; |
| 92 | + } else { |
| 93 | + initSucc = accepting; |
| 94 | + accSucc = initSucc; |
| 95 | + } |
| 96 | + |
| 97 | + vpa.setInternalSuccessor(init, i, initSucc); |
| 98 | + vpa.setInternalSuccessor(accepting, i, accSucc); |
| 99 | + } |
| 100 | + |
| 101 | + // criss-cross return successors |
| 102 | + for (final Integer r : returnAlphabet) { |
| 103 | + |
| 104 | + for (int i = 0; i < callAlphabet.size(); i++) { |
| 105 | + |
| 106 | + final Location initSucc; |
| 107 | + final Location accSucc; |
| 108 | + |
| 109 | + final int initSym = vpa.encodeStackSym(init, i); |
| 110 | + final int accSym = vpa.encodeStackSym(accepting, i); |
| 111 | + |
| 112 | + if (i % 2 == 0) { |
| 113 | + initSucc = init; |
| 114 | + accSucc = accepting; |
| 115 | + } else { |
| 116 | + initSucc = accepting; |
| 117 | + accSucc = initSucc; |
| 118 | + } |
| 119 | + |
| 120 | + vpa.setReturnSuccessor(init, r, initSym, initSucc); |
| 121 | + vpa.setReturnSuccessor(init, r, accSym, accSucc); |
| 122 | + vpa.setReturnSuccessor(accepting, r, initSym, accSucc); |
| 123 | + vpa.setReturnSuccessor(accepting, r, accSym, initSucc); |
| 124 | + } |
| 125 | + } |
| 126 | + |
| 127 | + verifyGraphRepresentation(alphabet, vpa, vpa); |
| 128 | + } |
| 129 | + |
| 130 | + private static <L, I> void verifyGraphRepresentation(VPDAlphabet<I> alphabet, |
| 131 | + OneSEVPA<L, I> vpa, |
| 132 | + Graph<L, SevpaViewEdge<L, I>> graph) { |
| 133 | + |
| 134 | + Assert.assertEquals(new HashSet<>(vpa.getLocations()), new HashSet<>(graph.getNodes())); |
| 135 | + |
| 136 | + for (final L loc : vpa.getLocations()) { |
| 137 | + for (SevpaViewEdge<L, I> edge : graph.getOutgoingEdges(loc)) { |
| 138 | + |
| 139 | + final I input = edge.input; |
| 140 | + final int stack = edge.stack; |
| 141 | + final L target = edge.target; |
| 142 | + |
| 143 | + switch (alphabet.getSymbolType(input)) { |
| 144 | + case CALL: |
| 145 | + throw new IllegalStateException("Call edges are implicit in a 1-SEVPA"); |
| 146 | + case INTERNAL: |
| 147 | + Assert.assertEquals(vpa.getInternalSuccessor(loc, input), target); |
| 148 | + continue; |
| 149 | + case RETURN: |
| 150 | + Assert.assertEquals(vpa.getReturnSuccessor(loc, input, stack), target); |
| 151 | + continue; |
| 152 | + default: |
| 153 | + throw new IllegalStateException("Unknown symbol type: " + alphabet.getSymbolType(input)); |
| 154 | + } |
| 155 | + } |
| 156 | + } |
| 157 | + } |
64 | 158 | }
|
0 commit comments