diff --git a/CHANGELOG.md b/CHANGELOG.md index 2c08cd25d1..2330705bbf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Fixed * Correctly enquote outputs containing whitespaces in `TAFWriter` ([#37](https://github.com/LearnLib/automatalib/issues/37), thanks to [Alexander Schieweck](https://github.com/aschieweck)). +* Fixed a bug in the `Graph` representation of `AbstractOneSEVPA`s ([#39](https://github.com/LearnLib/automatalib/pull/39), thanks to [DonatoClun](https://github.com/DonatoClun)). ## [0.9.0](https://github.com/LearnLib/automatalib/releases/tag/automatalib-0.9.0) - 2020-02-05 diff --git a/core/src/main/java/net/automatalib/automata/vpda/AbstractOneSEVPA.java b/core/src/main/java/net/automatalib/automata/vpda/AbstractOneSEVPA.java index 8ab860ecc8..8fb932c41a 100644 --- 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> 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 { - 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 index d6cc261f54..1e014b685c 100644 --- 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 #39. + */ + @Test + public void testGraphRepresentation() { + + final Alphabet callAlphabet = Alphabets.integers(1, 10); + final Alphabet internalAlphabet = Alphabets.integers(11, 20); + final Alphabet returnAlphabet = Alphabets.integers(21, 30); + final VPDAlphabet alphabet = new DefaultVPDAlphabet<>(internalAlphabet, callAlphabet, returnAlphabet); + + // create arbitrary VPA + final DefaultOneSEVPA 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 void verifyGraphRepresentation(VPDAlphabet alphabet, + OneSEVPA vpa, + Graph> graph) { + + Assert.assertEquals(new HashSet<>(vpa.getLocations()), new HashSet<>(graph.getNodes())); + + for (final L loc : vpa.getLocations()) { + for (SevpaViewEdge 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)); + } + } + } + } }