Merge e94e0b1 into d8d7d96

LearnLib · Mar 10, 2020 · f87329f · f87329f
2 parents d8d7d96 + e94e0b1
commit f87329f
Show file tree

Hide file tree

Showing 2 changed files with 98 additions and 4 deletions.
diff --git a/core/src/main/java/net/automatalib/automata/vpda/AbstractOneSEVPA.java b/core/src/main/java/net/automatalib/automata/vpda/AbstractOneSEVPA.java
@@ -125,7 +125,7 @@ public Collection<SevpaViewEdge<L, I>> getOutgoingEdges(final L location) {
             for (final L loc : getLocations()) {
                 for (final I stackSymbol : alphabet.getCallAlphabet()) {
                     final int sym = encodeStackSym(loc, stackSymbol);
-                    final L succ = getReturnSuccessor(loc, i, sym);
+                    final L succ = getReturnSuccessor(location, i, sym);
 
                     if (succ != null) {
                         result.add(new SevpaViewEdge<>(i, sym, succ));
@@ -195,9 +195,9 @@ public I getCallSym(final int stackSym) {
 
     static class SevpaViewEdge<S, I> {
 
-        private final I input;
-        private final int stack;
-        private final S target;
+        final I input;
+        final int stack;
+        final S target;
 
         SevpaViewEdge(I input, int stack, S target) {
             this.target = target;

diff --git a/core/src/test/java/net/automatalib/automata/vpda/VPDATest.java b/core/src/test/java/net/automatalib/automata/vpda/VPDATest.java
@@ -16,7 +16,10 @@
 package net.automatalib.automata.vpda;
 
 import java.util.Collections;
+import java.util.HashSet;
 
+import net.automatalib.automata.vpda.AbstractOneSEVPA.SevpaViewEdge;
+import net.automatalib.graphs.Graph;
 import net.automatalib.words.Alphabet;
 import net.automatalib.words.VPDAlphabet;
 import net.automatalib.words.Word;
@@ -61,4 +64,95 @@ public void testBracketLanguage() {
         Assert.assertFalse(vpda.accepts(Word.fromCharSequence(")(")));
         Assert.assertFalse(vpda.accepts(Word.fromCharSequence("()()")));
     }
+
+    /**
+     * Test case for reported issue <a href="https://github.com/LearnLib/automatalib/pull/39">#39</a>.
+     */
+    @Test
+    public void testGraphRepresentation() {
+
+        final Alphabet<Integer> callAlphabet = Alphabets.integers(1, 10);
+        final Alphabet<Integer> internalAlphabet = Alphabets.integers(11, 20);
+        final Alphabet<Integer> returnAlphabet = Alphabets.integers(21, 30);
+        final VPDAlphabet<Integer> alphabet = new DefaultVPDAlphabet<>(internalAlphabet, callAlphabet, returnAlphabet);
+
+        // create arbitrary VPA
+        final DefaultOneSEVPA<Integer> vpa = new DefaultOneSEVPA<>(alphabet);
+        final Location init = vpa.addInitialLocation(false);
+        final Location accepting = vpa.addLocation(true);
+
+        // criss-cross internal successors
+        for (final Integer i : internalAlphabet) {
+            final Location initSucc;
+            final Location accSucc;
+
+            if (i % 2 == 0) {
+                initSucc = init;
+                accSucc = accepting;
+            } else {
+                initSucc = accepting;
+                accSucc = initSucc;
+            }
+
+            vpa.setInternalSuccessor(init, i, initSucc);
+            vpa.setInternalSuccessor(accepting, i, accSucc);
+        }
+
+        // criss-cross return successors
+        for (final Integer r : returnAlphabet) {
+
+            for (int i = 0; i < callAlphabet.size(); i++) {
+
+                final Location initSucc;
+                final Location accSucc;
+
+                final int initSym = vpa.encodeStackSym(init, i);
+                final int accSym = vpa.encodeStackSym(accepting, i);
+
+                if (i % 2 == 0) {
+                    initSucc = init;
+                    accSucc = accepting;
+                } else {
+                    initSucc = accepting;
+                    accSucc = initSucc;
+                }
+
+                vpa.setReturnSuccessor(init, r, initSym, initSucc);
+                vpa.setReturnSuccessor(init, r, accSym, accSucc);
+                vpa.setReturnSuccessor(accepting, r, initSym, accSucc);
+                vpa.setReturnSuccessor(accepting, r, accSym, initSucc);
+            }
+        }
+
+        verifyGraphRepresentation(alphabet, vpa, vpa);
+    }
+
+    private static <L, I> void verifyGraphRepresentation(VPDAlphabet<I> alphabet,
+                                                         OneSEVPA<L, I> vpa,
+                                                         Graph<L, SevpaViewEdge<L, I>> graph) {
+
+        Assert.assertEquals(new HashSet<>(vpa.getLocations()), new HashSet<>(graph.getNodes()));
+
+        for (final L loc : vpa.getLocations()) {
+            for (SevpaViewEdge<L, I> edge : graph.getOutgoingEdges(loc)) {
+
+                final I input = edge.input;
+                final int stack = edge.stack;
+                final L target = edge.target;
+
+                switch (alphabet.getSymbolType(input)) {
+                    case CALL:
+                        throw new IllegalStateException("Call edges are implicit in a 1-SEVPA");
+                    case INTERNAL:
+                        Assert.assertEquals(vpa.getInternalSuccessor(loc, input), target);
+                        continue;
+                    case RETURN:
+                        Assert.assertEquals(vpa.getReturnSuccessor(loc, input, stack), target);
+                        continue;
+                    default:
+                        throw new IllegalStateException("Unknown symbol type: " + alphabet.getSymbolType(input));
+                }
+            }
+        }
+    }
 }