Skip to content

Commit 2fa3fd0

Browse files
mtf90mtf90
committed
PTA improvements
* color-code PTA nodes in visualization * remove redundant checks * fix erroneous construction of merged automata
1 parent 983750a commit 2fa3fd0

File tree

11 files changed

+245
-83
lines changed

11 files changed

+245
-83
lines changed

‎commons/datastructures/src/main/java/de/learnlib/datastructure/pta/AbstractBasePTAState.java‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ public S copy() {
4646

4747
public S copy(@Nullable ArrayStorage<TP> newTPs) {
4848
try {
49+
// we need to clone here, because we want to copy (unknown at this point) sub-class attributes like coloring
4950
@SuppressWarnings("unchecked")
5051
S copy = (S) clone();
5152
copy.transProperties = newTPs;

‎commons/datastructures/src/main/java/de/learnlib/datastructure/pta/AbstractBlueFringePTA.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,9 @@
2020
import java.util.List;
2121
import java.util.function.Consumer;
2222

23+
import de.learnlib.datastructure.pta.visualization.BlueFringeVisualizationHelper;
24+
import net.automatalib.automaton.graph.TransitionEdge;
25+
import net.automatalib.visualization.VisualizationHelper;
2326
import org.checkerframework.checker.index.qual.NonNegative;
2427
import org.checkerframework.checker.nullness.qual.Nullable;
2528

@@ -71,4 +74,8 @@ private void makeRed(S qb) {
7174
return merge;
7275
}
7376

77+
@Override
78+
protected VisualizationHelper<S, TransitionEdge<Integer, PTATransition<S>>> getVisualizationHelper() {
79+
return new BlueFringeVisualizationHelper<>(this);
80+
}
7481
}

‎commons/datastructures/src/main/java/de/learnlib/datastructure/pta/BasePTA.java‎

Lines changed: 6 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -22,18 +22,17 @@
2222
import java.util.HashSet;
2323
import java.util.Iterator;
2424
import java.util.List;
25-
import java.util.Map;
2625
import java.util.Objects;
2726
import java.util.Set;
2827

28+
import de.learnlib.datastructure.pta.visualization.PTAVisualizationHelper;
2929
import net.automatalib.alphabet.Alphabet;
3030
import net.automatalib.alphabet.impl.Alphabets;
3131
import net.automatalib.automaton.FiniteAlphabetAutomaton;
3232
import net.automatalib.automaton.UniversalDeterministicAutomaton;
3333
import net.automatalib.automaton.graph.TransitionEdge;
3434
import net.automatalib.automaton.graph.TransitionEdge.Property;
3535
import net.automatalib.automaton.graph.UniversalAutomatonGraphView;
36-
import net.automatalib.automaton.visualization.AutomatonVisualizationHelper;
3736
import net.automatalib.common.smartcollection.IntSeq;
3837
import net.automatalib.common.util.collection.AbstractSimplifiedIterator;
3938
import net.automatalib.graph.UniversalGraph;
@@ -255,31 +254,12 @@ public UniversalGraph<S, TransitionEdge<Integer, PTATransition<S>>, SP, Property
255254

256255
@Override
257256
public VisualizationHelper<S, TransitionEdge<Integer, PTATransition<S>>> getVisualizationHelper() {
258-
return new AutomatonVisualizationHelper<S, Integer, PTATransition<S>, BasePTA<S, SP, TP>>(BasePTA.this) {
259-
260-
@Override
261-
public boolean getEdgeProperties(S src,
262-
TransitionEdge<Integer, PTATransition<S>> edge,
263-
S tgt,
264-
Map<String, String> properties) {
265-
super.getEdgeProperties(src, edge, tgt, properties);
266-
267-
final Integer input = edge.getInput();
268-
properties.put(EdgeAttrs.LABEL, input + " / " + src.getTransProperty(input));
269-
270-
return true;
271-
}
272-
273-
@Override
274-
public boolean getNodeProperties(S node, Map<String, String> properties) {
275-
super.getNodeProperties(node, properties);
276-
277-
properties.put(NodeAttrs.LABEL, Objects.toString(node.getProperty()));
278-
279-
return true;
280-
}
281-
};
257+
return BasePTA.this.getVisualizationHelper();
282258
}
283259
};
284260
}
261+
262+
protected VisualizationHelper<S, TransitionEdge<Integer, PTATransition<S>>> getVisualizationHelper() {
263+
return new PTAVisualizationHelper<>(this);
264+
}
285265
}

‎commons/datastructures/src/main/java/de/learnlib/datastructure/pta/RedBlueMerge.java‎

Lines changed: 30 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -18,16 +18,16 @@
1818
import java.util.ArrayDeque;
1919
import java.util.Collection;
2020
import java.util.Deque;
21-
import java.util.HashSet;
2221
import java.util.Iterator;
22+
import java.util.LinkedHashSet;
2323
import java.util.Objects;
2424
import java.util.Queue;
2525
import java.util.Set;
2626
import java.util.function.Consumer;
2727

2828
import net.automatalib.automaton.UniversalDeterministicAutomaton;
29-
import net.automatalib.common.util.Pair;
3029
import net.automatalib.common.util.array.ArrayStorage;
30+
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
3131
import org.checkerframework.checker.nullness.qual.Nullable;
3232

3333
public class RedBlueMerge<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, TP> {
@@ -39,7 +39,6 @@ public class RedBlueMerge<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, T
3939
private final int alphabetSize;
4040
private final S qr;
4141
private final S qb;
42-
private boolean merged;
4342

4443
public RedBlueMerge(AbstractBlueFringePTA<S, SP, TP> pta, S qr, S qb) {
4544
this(pta, qr, qb, validateInputs(pta, qr, qb));
@@ -79,7 +78,6 @@ public S getBlueState() {
7978
}
8079

8180
public boolean merge() {
82-
this.merged = true;
8381
if (!mergeRedProperties(qr, qb)) {
8482
return false;
8583
}
@@ -161,9 +159,6 @@ public boolean merge() {
161159

162160
private S cloneTopSucc(S succ, int i, Deque<FoldRecord<S>> stack, @Nullable ArrayStorage<TP> newTPs) {
163161
S succClone = (newTPs != null) ? succ.copy(newTPs) : succ.copy();
164-
if (succClone == succ) {
165-
return succ;
166-
}
167162
FoldRecord<S> peek = stack.peek();
168163
assert peek != null;
169164
S top = peek.q;
@@ -180,9 +175,6 @@ private S cloneTop(S topState, Deque<FoldRecord<S>> stack) {
180175
assert !topState.isRed();
181176

182177
S topClone = topState.copy();
183-
if (topClone == topState) {
184-
return topState;
185-
}
186178
S currTgt = topClone;
187179

188180
Iterator<FoldRecord<S>> it = stack.iterator();
@@ -198,9 +190,6 @@ private S cloneTop(S topState, Deque<FoldRecord<S>> stack) {
198190
S currSrcClone = currSrc.copy();
199191
assert currSrcClone.successors != null;
200192
currSrcClone.successors.set(currRec.i, currTgt);
201-
if (currSrcClone == currSrc) {
202-
return topClone; // we're done
203-
}
204193
currRec.q = currSrcClone;
205194
currTgt = currSrcClone;
206195

@@ -321,10 +310,12 @@ private boolean mergeRedStateProperty(S qr, S qb) {
321310
}
322311

323312
/**
324-
* Merges two non-null transition property arrays. The behavior of this method is as follows: <ul> <li>if {@code
325-
* tps1} subsumes {@code tps2}, then {@code tps1} is returned.</li> <li>otherwise, if {@code tps1} and {@code tps2}
326-
* can be merged, a new {@link ArrayStorage} containing the result of the merge is returned. <li>otherwise
327-
* (i.e., if no merge is possible), {@code null} is returned. </ul>
313+
* Merges two non-null transition property arrays. The behavior of this method is as follows:
314+
* <ul>
315+
* <li>if {@code tps1} subsumes {@code tps2}, then {@code tps1} is returned.</li>
316+
* <li>otherwise, if {@code tps1} and {@code tps2} can be merged, a new {@link ArrayStorage} containing the result of the merge is returned.</li>
317+
* <li>otherwise (i.e., if no merge is possible), {@code null} is returned.</li>
318+
* </ul>
328319
*/
329320
@SuppressWarnings("PMD.ReturnEmptyCollectionRatherThanNull") // null is semantically different from an empty list
330321
private @Nullable ArrayStorage<TP> mergeTransProperties(ArrayStorage<TP> tps1, ArrayStorage<TP> tps2) {
@@ -432,52 +423,42 @@ private void incorporate(S state) {
432423
}
433424
}
434425

426+
/**
427+
* Returns an automaton-based view of the merge. If the merge was not yet {@link #merge() tried}, this view is equal
428+
* to the unmodified PTA.
429+
*
430+
* @return the automaton-based view of this merge
431+
*/
435432
public UniversalDeterministicAutomaton<S, Integer, ?, SP, TP> toMergedAutomaton() {
436-
if (!this.merged) {
437-
throw new IllegalStateException("#merge has not been called yet");
438-
}
439-
440-
return new UniversalDeterministicAutomaton<S, Integer, Pair<S, Integer>, SP, TP>() {
433+
return new UniversalDeterministicAutomaton<S, Integer, PTATransition<S>, SP, TP>() {
441434

442-
private Set<S> states;
435+
private @MonotonicNonNull Set<S> states;
443436

444437
@Override
445-
public @Nullable S getSuccessor(Pair<S, Integer> transition) {
446-
final S source = transition.getFirst();
447-
final Integer input = transition.getSecond();
448-
449-
if (source.isRed() && succMod.get(source.id) != null) {
450-
return succMod.get(source.id).get(input);
451-
}
452-
453-
return pta.getSuccessor(source, input);
438+
public S getSuccessor(PTATransition<S> transition) {
439+
return Objects.requireNonNull(RedBlueMerge.this.getSucc(transition.getSource(), transition.getIndex()));
454440
}
455441

456442
@Override
457443
public SP getStateProperty(S state) {
458-
if (state.isRed() && propMod.get(state.id) != null) {
459-
return propMod.get(state.id);
460-
}
461-
462-
return state.getStateProperty();
444+
return RedBlueMerge.this.getStateProperty(state);
463445
}
464446

465447
@Override
466-
public TP getTransitionProperty(Pair<S, Integer> transition) {
467-
final S source = transition.getFirst();
468-
final Integer input = transition.getSecond();
448+
public TP getTransitionProperty(PTATransition<S> transition) {
449+
ArrayStorage<TP> properties = RedBlueMerge.this.getTransProperties(transition.getSource());
469450

470-
if (source.isRed() && transPropMod.get(source.id) != null) {
471-
return transPropMod.get(source.id).get(input);
451+
if (properties != null) {
452+
return properties.get(transition.getIndex());
472453
}
473454

474-
assert source.transProperties != null;
475-
return source.transProperties.get(input);
455+
return null;
476456
}
477457

478458
@Override
479-
public Pair<S, Integer> getTransition(S state, Integer input) {
480-
return Pair.of(state, input);
459+
public @Nullable PTATransition<S> getTransition(S state, Integer input) {
460+
final S succ = RedBlueMerge.this.getSucc(state, input);
461+
return succ == null ? null : new PTATransition<>(state, input);
481462
}
482463

483464
@Override
@@ -487,22 +468,21 @@ public Collection<S> getStates() {
487468
return states;
488469
}
489470

490-
states = new HashSet<>();
471+
states = new LinkedHashSet<>();
491472
final Queue<S> discoverQueue = new ArrayDeque<>();
492473

493474
S initialState = getInitialState();
494475
assert initialState != null;
495476
discoverQueue.add(initialState);
477+
states.add(initialState);
496478

497479
S iter;
498480

499481
while ((iter = discoverQueue.poll()) != null) {
500-
states.add(iter);
501-
502482
for (int i = 0; i < alphabetSize; i++) {
503483
final S succ = getSuccessor(iter, i);
504484

505-
if (succ != null && !states.contains(succ)) {
485+
if (succ != null && states.add(succ)) {
506486
discoverQueue.add(succ);
507487
}
508488
}

‎commons/datastructures/src/main/java/de/learnlib/datastructure/pta/visualization/BlueFringeVisualizationHelper.java‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
/* Copyright (C) 2013-2025 TU Dortmund University
2+
* This file is part of LearnLib <https://learnlib.de>.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.datastructure.pta.visualization;
17+
18+
import java.util.Map;
19+
20+
import de.learnlib.datastructure.pta.AbstractBlueFringePTA;
21+
import de.learnlib.datastructure.pta.AbstractBlueFringePTAState;
22+
import de.learnlib.datastructure.pta.PTATransition;
23+
24+
public class BlueFringeVisualizationHelper<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, TP>
25+
extends PTAVisualizationHelper<S, Integer, PTATransition<S>, SP, TP, AbstractBlueFringePTA<S, SP, TP>> {
26+
27+
public BlueFringeVisualizationHelper(AbstractBlueFringePTA<S, SP, TP> automaton) {
28+
super(automaton);
29+
}
30+
31+
@Override
32+
public boolean getNodeProperties(S node, Map<String, String> properties) {
33+
34+
// don't put the color directly, because WHITE should render as black
35+
switch (node.getColor()) {
36+
case RED:
37+
case BLUE:
38+
properties.put(NodeAttrs.COLOR, node.getColor().toString());
39+
break;
40+
default:
41+
// to nothing
42+
}
43+
44+
return super.getNodeProperties(node, properties);
45+
}
46+
}

‎commons/datastructures/src/main/java/de/learnlib/datastructure/pta/visualization/PTAVisualizationHelper.java‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/* Copyright (C) 2013-2025 TU Dortmund University
2+
* This file is part of LearnLib <https://learnlib.de>.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.datastructure.pta.visualization;
17+
18+
import java.util.Map;
19+
import java.util.Objects;
20+
21+
import net.automatalib.automaton.UniversalDeterministicAutomaton;
22+
import net.automatalib.automaton.graph.TransitionEdge;
23+
import net.automatalib.automaton.visualization.AutomatonVisualizationHelper;
24+
25+
public class PTAVisualizationHelper<S, I, T, SP, TP, A extends UniversalDeterministicAutomaton<S, I, T, SP, TP>>
26+
extends AutomatonVisualizationHelper<S, I, T, A> {
27+
28+
public PTAVisualizationHelper(A automaton) {
29+
super(automaton);
30+
}
31+
32+
@Override
33+
public boolean getEdgeProperties(S src,
34+
TransitionEdge<I, T> edge,
35+
S tgt,
36+
Map<String, String> properties) {
37+
super.getEdgeProperties(src, edge, tgt, properties);
38+
39+
final I input = edge.getInput();
40+
properties.put(EdgeAttrs.LABEL, input + " / " + automaton.getTransitionProperty(edge.getTransition()));
41+
42+
return true;
43+
}
44+
45+
@Override
46+
public boolean getNodeProperties(S node, Map<String, String> properties) {
47+
super.getNodeProperties(node, properties);
48+
49+
properties.put(NodeAttrs.LABEL, Objects.toString(automaton.getStateProperty(node)));
50+
51+
return true;
52+
}
53+
}

‎commons/datastructures/src/main/java/module-info.java‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,4 +47,5 @@
4747
exports de.learnlib.datastructure.pta;
4848
exports de.learnlib.datastructure.pta.config;
4949
exports de.learnlib.datastructure.pta.wrapper;
50+
exports de.learnlib.datastructure.pta.visualization;
5051
}

0 commit comments

Comments
 (0)