Skip to content

Commit

Permalink
PTA improvements
Browse files Browse the repository at this point in the history
* color-code PTA nodes in visualization
* remove redundant checks
* fix erroneous construction of merged automata
  • Loading branch information
mtf90 committed Jan 10, 2025
1 parent 983750a commit 2fa3fd0
Show file tree
Hide file tree
Showing 11 changed files with 245 additions and 83 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ public S copy() {

public S copy(@Nullable ArrayStorage<TP> newTPs) {
try {
// we need to clone here, because we want to copy (unknown at this point) sub-class attributes like coloring
@SuppressWarnings("unchecked")
S copy = (S) clone();
copy.transProperties = newTPs;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,9 @@
import java.util.List;
import java.util.function.Consumer;

import de.learnlib.datastructure.pta.visualization.BlueFringeVisualizationHelper;
import net.automatalib.automaton.graph.TransitionEdge;
import net.automatalib.visualization.VisualizationHelper;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.nullness.qual.Nullable;

Expand Down Expand Up @@ -71,4 +74,8 @@ private void makeRed(S qb) {
return merge;
}

@Override
protected VisualizationHelper<S, TransitionEdge<Integer, PTATransition<S>>> getVisualizationHelper() {
return new BlueFringeVisualizationHelper<>(this);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -22,18 +22,17 @@
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Set;

import de.learnlib.datastructure.pta.visualization.PTAVisualizationHelper;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.impl.Alphabets;
import net.automatalib.automaton.FiniteAlphabetAutomaton;
import net.automatalib.automaton.UniversalDeterministicAutomaton;
import net.automatalib.automaton.graph.TransitionEdge;
import net.automatalib.automaton.graph.TransitionEdge.Property;
import net.automatalib.automaton.graph.UniversalAutomatonGraphView;
import net.automatalib.automaton.visualization.AutomatonVisualizationHelper;
import net.automatalib.common.smartcollection.IntSeq;
import net.automatalib.common.util.collection.AbstractSimplifiedIterator;
import net.automatalib.graph.UniversalGraph;
Expand Down Expand Up @@ -255,31 +254,12 @@ public UniversalGraph<S, TransitionEdge<Integer, PTATransition<S>>, SP, Property

@Override
public VisualizationHelper<S, TransitionEdge<Integer, PTATransition<S>>> getVisualizationHelper() {
return new AutomatonVisualizationHelper<S, Integer, PTATransition<S>, BasePTA<S, SP, TP>>(BasePTA.this) {

@Override
public boolean getEdgeProperties(S src,
TransitionEdge<Integer, PTATransition<S>> edge,
S tgt,
Map<String, String> properties) {
super.getEdgeProperties(src, edge, tgt, properties);

final Integer input = edge.getInput();
properties.put(EdgeAttrs.LABEL, input + " / " + src.getTransProperty(input));

return true;
}

@Override
public boolean getNodeProperties(S node, Map<String, String> properties) {
super.getNodeProperties(node, properties);

properties.put(NodeAttrs.LABEL, Objects.toString(node.getProperty()));

return true;
}
};
return BasePTA.this.getVisualizationHelper();
}
};
}

protected VisualizationHelper<S, TransitionEdge<Integer, PTATransition<S>>> getVisualizationHelper() {
return new PTAVisualizationHelper<>(this);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -18,16 +18,16 @@
import java.util.ArrayDeque;
import java.util.Collection;
import java.util.Deque;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.Objects;
import java.util.Queue;
import java.util.Set;
import java.util.function.Consumer;

import net.automatalib.automaton.UniversalDeterministicAutomaton;
import net.automatalib.common.util.Pair;
import net.automatalib.common.util.array.ArrayStorage;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

public class RedBlueMerge<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, TP> {
Expand All @@ -39,7 +39,6 @@ public class RedBlueMerge<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, T
private final int alphabetSize;
private final S qr;
private final S qb;
private boolean merged;

public RedBlueMerge(AbstractBlueFringePTA<S, SP, TP> pta, S qr, S qb) {
this(pta, qr, qb, validateInputs(pta, qr, qb));
Expand Down Expand Up @@ -79,7 +78,6 @@ public S getBlueState() {
}

public boolean merge() {
this.merged = true;
if (!mergeRedProperties(qr, qb)) {
return false;
}
Expand Down Expand Up @@ -161,9 +159,6 @@ public boolean merge() {

private S cloneTopSucc(S succ, int i, Deque<FoldRecord<S>> stack, @Nullable ArrayStorage<TP> newTPs) {
S succClone = (newTPs != null) ? succ.copy(newTPs) : succ.copy();
if (succClone == succ) {
return succ;
}
FoldRecord<S> peek = stack.peek();
assert peek != null;
S top = peek.q;
Expand All @@ -180,9 +175,6 @@ private S cloneTop(S topState, Deque<FoldRecord<S>> stack) {
assert !topState.isRed();

S topClone = topState.copy();
if (topClone == topState) {
return topState;
}
S currTgt = topClone;

Iterator<FoldRecord<S>> it = stack.iterator();
Expand All @@ -198,9 +190,6 @@ private S cloneTop(S topState, Deque<FoldRecord<S>> stack) {
S currSrcClone = currSrc.copy();
assert currSrcClone.successors != null;
currSrcClone.successors.set(currRec.i, currTgt);
if (currSrcClone == currSrc) {
return topClone; // we're done
}
currRec.q = currSrcClone;
currTgt = currSrcClone;

Expand Down Expand Up @@ -321,10 +310,12 @@ private boolean mergeRedStateProperty(S qr, S qb) {
}

/**
* Merges two non-null transition property arrays. The behavior of this method is as follows: <ul> <li>if {@code
* tps1} subsumes {@code tps2}, then {@code tps1} is returned.</li> <li>otherwise, if {@code tps1} and {@code tps2}
* can be merged, a new {@link ArrayStorage} containing the result of the merge is returned. <li>otherwise
* (i.e., if no merge is possible), {@code null} is returned. </ul>
* Merges two non-null transition property arrays. The behavior of this method is as follows:
* <ul>
* <li>if {@code tps1} subsumes {@code tps2}, then {@code tps1} is returned.</li>
* <li>otherwise, if {@code tps1} and {@code tps2} can be merged, a new {@link ArrayStorage} containing the result of the merge is returned.</li>
* <li>otherwise (i.e., if no merge is possible), {@code null} is returned.</li>
* </ul>
*/
@SuppressWarnings("PMD.ReturnEmptyCollectionRatherThanNull") // null is semantically different from an empty list
private @Nullable ArrayStorage<TP> mergeTransProperties(ArrayStorage<TP> tps1, ArrayStorage<TP> tps2) {
Expand Down Expand Up @@ -432,52 +423,42 @@ private void incorporate(S state) {
}
}

/**
* Returns an automaton-based view of the merge. If the merge was not yet {@link #merge() tried}, this view is equal
* to the unmodified PTA.
*
* @return the automaton-based view of this merge
*/
public UniversalDeterministicAutomaton<S, Integer, ?, SP, TP> toMergedAutomaton() {
if (!this.merged) {
throw new IllegalStateException("#merge has not been called yet");
}

return new UniversalDeterministicAutomaton<S, Integer, Pair<S, Integer>, SP, TP>() {
return new UniversalDeterministicAutomaton<S, Integer, PTATransition<S>, SP, TP>() {

private Set<S> states;
private @MonotonicNonNull Set<S> states;

@Override
public @Nullable S getSuccessor(Pair<S, Integer> transition) {
final S source = transition.getFirst();
final Integer input = transition.getSecond();

if (source.isRed() && succMod.get(source.id) != null) {
return succMod.get(source.id).get(input);
}

return pta.getSuccessor(source, input);
public S getSuccessor(PTATransition<S> transition) {
return Objects.requireNonNull(RedBlueMerge.this.getSucc(transition.getSource(), transition.getIndex()));
}

@Override
public SP getStateProperty(S state) {
if (state.isRed() && propMod.get(state.id) != null) {
return propMod.get(state.id);
}

return state.getStateProperty();
return RedBlueMerge.this.getStateProperty(state);
}

@Override
public TP getTransitionProperty(Pair<S, Integer> transition) {
final S source = transition.getFirst();
final Integer input = transition.getSecond();
public TP getTransitionProperty(PTATransition<S> transition) {
ArrayStorage<TP> properties = RedBlueMerge.this.getTransProperties(transition.getSource());

if (source.isRed() && transPropMod.get(source.id) != null) {
return transPropMod.get(source.id).get(input);
if (properties != null) {
return properties.get(transition.getIndex());
}

assert source.transProperties != null;
return source.transProperties.get(input);
return null;
}

@Override
public Pair<S, Integer> getTransition(S state, Integer input) {
return Pair.of(state, input);
public @Nullable PTATransition<S> getTransition(S state, Integer input) {
final S succ = RedBlueMerge.this.getSucc(state, input);
return succ == null ? null : new PTATransition<>(state, input);
}

@Override
Expand All @@ -487,22 +468,21 @@ public Collection<S> getStates() {
return states;
}

states = new HashSet<>();
states = new LinkedHashSet<>();
final Queue<S> discoverQueue = new ArrayDeque<>();

S initialState = getInitialState();
assert initialState != null;
discoverQueue.add(initialState);
states.add(initialState);

S iter;

while ((iter = discoverQueue.poll()) != null) {
states.add(iter);

for (int i = 0; i < alphabetSize; i++) {
final S succ = getSuccessor(iter, i);

if (succ != null && !states.contains(succ)) {
if (succ != null && states.add(succ)) {
discoverQueue.add(succ);
}
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
/* Copyright (C) 2013-2025 TU Dortmund University
* This file is part of LearnLib <https://learnlib.de>.
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package de.learnlib.datastructure.pta.visualization;

import java.util.Map;

import de.learnlib.datastructure.pta.AbstractBlueFringePTA;
import de.learnlib.datastructure.pta.AbstractBlueFringePTAState;
import de.learnlib.datastructure.pta.PTATransition;

public class BlueFringeVisualizationHelper<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, TP>
extends PTAVisualizationHelper<S, Integer, PTATransition<S>, SP, TP, AbstractBlueFringePTA<S, SP, TP>> {

public BlueFringeVisualizationHelper(AbstractBlueFringePTA<S, SP, TP> automaton) {
super(automaton);
}

@Override
public boolean getNodeProperties(S node, Map<String, String> properties) {

// don't put the color directly, because WHITE should render as black
switch (node.getColor()) {
case RED:
case BLUE:
properties.put(NodeAttrs.COLOR, node.getColor().toString());
break;
default:
// to nothing
}

return super.getNodeProperties(node, properties);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
/* Copyright (C) 2013-2025 TU Dortmund University
* This file is part of LearnLib <https://learnlib.de>.
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package de.learnlib.datastructure.pta.visualization;

import java.util.Map;
import java.util.Objects;

import net.automatalib.automaton.UniversalDeterministicAutomaton;
import net.automatalib.automaton.graph.TransitionEdge;
import net.automatalib.automaton.visualization.AutomatonVisualizationHelper;

public class PTAVisualizationHelper<S, I, T, SP, TP, A extends UniversalDeterministicAutomaton<S, I, T, SP, TP>>
extends AutomatonVisualizationHelper<S, I, T, A> {

public PTAVisualizationHelper(A automaton) {
super(automaton);
}

@Override
public boolean getEdgeProperties(S src,
TransitionEdge<I, T> edge,
S tgt,
Map<String, String> properties) {
super.getEdgeProperties(src, edge, tgt, properties);

final I input = edge.getInput();
properties.put(EdgeAttrs.LABEL, input + " / " + automaton.getTransitionProperty(edge.getTransition()));

return true;
}

@Override
public boolean getNodeProperties(S node, Map<String, String> properties) {
super.getNodeProperties(node, properties);

properties.put(NodeAttrs.LABEL, Objects.toString(automaton.getStateProperty(node)));

return true;
}
}
1 change: 1 addition & 0 deletions commons/datastructures/src/main/java/module-info.java
Original file line number Diff line number Diff line change
Expand Up @@ -47,4 +47,5 @@
exports de.learnlib.datastructure.pta;
exports de.learnlib.datastructure.pta.config;
exports de.learnlib.datastructure.pta.wrapper;
exports de.learnlib.datastructure.pta.visualization;
}
Loading

0 comments on commit 2fa3fd0

Please sign in to comment.