6611855081

Committed 23 Oct 2023 10:13AM UTC coverage: 93.275% (-0.003%) from 93.278%

Build # 6611855081

Build Type

push

github

Committed by

mtf90

Commit Message

partially revert f4f47b4

Make the (Base)PTA Integer-based again and instead use explicit wrapper classes to interpret it as a DFA/MealyMachine/etc.. This simplifies the internals of the (Base)PTA class and allows for more flexible usage (e.g., using the same PTA for different contexts). Performance-wise the number of symbol-to-index transformations should remain identical for the common use-cases (e.g., RPNI-based learning, etc.).

Run Details

98 of 98 new or added lines in 13 files covered. (100.0%)

11553 of 12386 relevant lines covered (93.27%)

1.69 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

92.19

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

/* Copyright (C) 2013-2023 TU Dortmund
 * This file is part of LearnLib, http://www.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;

import java.awt.Color;
import java.util.ArrayDeque;
import java.util.Collection;
import java.util.Deque;
import java.util.HashSet;
import java.util.Iterator;
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.smartcollection.ArrayStorage;
import net.automatalib.common.util.Pair;
import org.checkerframework.checker.nullness.qual.Nullable;

public class RedBlueMerge<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, TP> {

    private final AbstractBlueFringePTA<S, SP, TP> pta;
    private final ArrayStorage<ArrayStorage<S>> succMod;
    private final ArrayStorage<ArrayStorage<TP>> transPropMod;
    private final ArrayStorage<SP> propMod;
    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) {
        if (!qr.isRed()) {
            throw new IllegalArgumentException("Merge target must be a red state");
        }
        if (!qb.isBlue()) {
            throw new IllegalArgumentException("Merge source must be a blue state");
        }

        this.pta = pta;

        int numRedStates = pta.getNumRedStates();
        this.succMod = new ArrayStorage<>(numRedStates);
        this.transPropMod = new ArrayStorage<>(numRedStates);
        this.propMod = new ArrayStorage<>(numRedStates);
        this.alphabetSize = pta.getInputAlphabet().size();

        this.qr = qr;
        this.qb = qb;
    }

    public S getRedState() {
        return qr;
    }

    public S getBlueState() {
        return qb;
    }

    public boolean merge() {
        this.merged = true;
        if (!mergeRedProperties(qr, qb)) {
            return false;
        }
        updateRedTransition(qb.parent, qb.parentInput, qr);

        Deque<FoldRecord<S>> stack = new ArrayDeque<>();
        stack.push(new FoldRecord<>(qr, qb));

        FoldRecord<S> curr;
        while ((curr = stack.peek()) != null) {
            int i = ++curr.i;

            if (i == alphabetSize) {
                stack.pop();
                continue;
            }

            S q = curr.q;
            S r = curr.r;

            S rSucc = r.getSuccessor(i);
            if (rSucc != null) {
                S qSucc = getSucc(q, i);
                if (qSucc != null) {
                    if (qSucc.isRed()) {
                        if (!mergeRedProperties(qSucc, rSucc)) {
                            return false;
                        }
                    } else {
                        SP rSuccSP = rSucc.property, qSuccSP = qSucc.property;

                        SP newSP = null;
                        if (qSuccSP == null && rSuccSP != null) {
                            newSP = rSuccSP;
                        } else if (rSuccSP != null && !rSuccSP.equals(qSuccSP)) {
                            return false;
                        }

                        ArrayStorage<TP> newTPs = null;
                        ArrayStorage<TP> rSuccTPs = rSucc.transProperties;
                        ArrayStorage<TP> qSuccTPs = qSucc.transProperties;

                        if (rSuccTPs != null) {
                            if (qSuccTPs != null) {
                                ArrayStorage<TP> mergedTPs = mergeTransProperties(qSuccTPs, rSuccTPs);
                                if (mergedTPs == null) {
                                    return false;
                                } else if (mergedTPs != qSuccTPs) {
                                    newTPs = mergedTPs;
                                }
                            } else {
                                newTPs = rSuccTPs.clone();
                            }
                        }

                        if (newSP != null || newTPs != null) {
                            qSucc = cloneTopSucc(qSucc, i, stack, newTPs);
                            if (newSP != null) {
                                qSucc.property = newSP;
                            }
                        }
                    }

                    stack.push(new FoldRecord<>(qSucc, rSucc));
                } else {
                    if (q.isRed()) {
                        updateRedTransition(q, i, rSucc, r.getTransProperty(i));
                    } else {
                        q = cloneTop(q, stack);
                        assert q.isCopy;
                        q.setForeignSuccessor(i, rSucc, alphabetSize);
                    }
                }
            }
        }

        return true;
    }

    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;
        if (top.isRed()) {
            updateRedTransition(top, i, succClone);
        } else {
            S topClone = cloneTop(top, stack);
            topClone.setForeignSuccessor(i, succClone, alphabetSize);
        }
        return succClone;
    }

    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();
        FoldRecord<S> currRec = it.next();
        assert currRec.q == topState;
        currRec.q = topClone;

        assert it.hasNext();
        currRec = it.next();
        S currSrc = currRec.q;

        while (!currSrc.isRed()) {
            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;

            assert it.hasNext();
            currRec = it.next();
            currSrc = currRec.q;
        }

        assert currSrc.isRed();
        updateRedTransition(currSrc, currRec.i, currTgt);

        return topClone;
    }

    private @Nullable ArrayStorage<TP> getTransProperties(S q) {
        if (q.isRed()) {
            int qId = q.id;
            ArrayStorage<TP> props = transPropMod.get(qId);
            if (props != null) {
                return props;
            }
        }
        return q.transProperties;
    }

    private SP getStateProperty(S q) {
        if (q.isRed()) {
            int qId = q.id;
            SP prop = propMod.get(qId);
            if (prop != null) {
                return prop;
            }
        }
        return q.property;
    }

    private @Nullable S getSucc(S q, int i) {
        if (q.isRed()) {
            int qId = q.id;
            ArrayStorage<S> modSuccs = succMod.get(qId);
            if (modSuccs != null) {
                return modSuccs.get(i);
            }
        }
        return q.getSuccessor(i);
    }

    private void updateRedTransition(S redSrc, int input, S tgt) {
        updateRedTransition(redSrc, input, tgt, null);
    }

    private void updateRedTransition(S redSrc, int input, S tgt, @Nullable TP transProp) {
        assert redSrc.isRed();

        int id = redSrc.id;
        ArrayStorage<S> newSuccs = succMod.get(id);
        if (newSuccs == null) {
            if (redSrc.successors == null) {
                newSuccs = new ArrayStorage<>(alphabetSize);
            } else {
                newSuccs = redSrc.successors.clone();
            }
            succMod.set(id, newSuccs);
        }
        newSuccs.set(input, tgt);
        if (transProp != null) {
            ArrayStorage<TP> newTransProps = transPropMod.get(id);
            if (newTransProps == null) {
                if (redSrc.transProperties == null) {
                    newTransProps = new ArrayStorage<>(alphabetSize);
                } else {
                    newTransProps = redSrc.transProperties.clone();
                }
                transPropMod.set(id, newTransProps);
            }
            newTransProps.set(input, transProp);
        }
    }

    private boolean mergeRedProperties(S qr, S qb) {
        return mergeRedStateProperty(qr, qb) && mergeRedTransProperties(qr, qb);
    }

    private boolean mergeRedTransProperties(S qr, S qb) {
        assert qr.isRed();

        ArrayStorage<TP> qbProps = qb.transProperties;
        if (qbProps == null) {
            return true;
        }
        ArrayStorage<TP> qrProps = getTransProperties(qr);
        ArrayStorage<TP> mergedProps = qbProps;
        if (qrProps != null) {
            mergedProps = mergeTransProperties(qrProps, qbProps);
            if (mergedProps == null) {
                return false;
            }
        }
        if (mergedProps != qrProps) {
            transPropMod.set(qr.id, mergedProps);
        }
        return true;
    }

    private boolean mergeRedStateProperty(S qr, S qb) {
        assert qr.isRed();

        SP qbProp = qb.property;
        if (qbProp == null) {
            return true;
        }
        SP qrProp = getStateProperty(qr);
        if (qrProp != null) {
            return Objects.equals(qbProp, qrProp);
        }
        propMod.set(qr.id, qbProp);
        return true;
    }

    /**
     * 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>
     */
    private @Nullable ArrayStorage<TP> mergeTransProperties(ArrayStorage<TP> tps1, ArrayStorage<TP> tps2) {
        int len = tps1.size();
        int i;

        ArrayStorage<TP> tps1OrCopy = tps1;

        for (i = 0; i < len; i++) {
            TP tp1 = tps1OrCopy.get(i);
            TP tp2 = tps2.get(i);
            if (tp2 != null) {
                if (tp1 != null) {
                    if (!Objects.equals(tp1, tp2)) {
                        return null;
                    }
                } else {
                    tps1OrCopy = tps1.clone();
                    tps1OrCopy.set(i++, tp2);
                    break;
                }
            }
        }

        for (; i < len; i++) {
            TP tp1 = tps1OrCopy.get(i);
            TP tp2 = tps2.get(i);
            if (tp2 != null) {
                if (tp1 != null) {
                    if (!Objects.equals(tp1, tp2)) {
                        return null;
                    }
                } else {
                    tps1OrCopy.set(i, tp2);
                }
            }
        }

        return tps1OrCopy;
    }

    public void apply(AbstractBlueFringePTA<S, SP, TP> pta, Consumer<? super PTATransition<S>> newFrontierConsumer) {
        int alphabetSize = pta.getInputAlphabet().size();

        for (int i = 0; i < succMod.size(); i++) {
            S redState = pta.redStates.get(i);
            assert redState.isRed();
            ArrayStorage<S> newSuccs = succMod.get(i);
            if (newSuccs != null) {
                int len = newSuccs.size();
                for (int j = 0; j < len; j++) {
                    S newSucc = newSuccs.get(j);
                    if (newSucc != null) {
                        redState.setForeignSuccessor(j, newSucc, alphabetSize);
                        Color c = newSucc.getColor();
                        if (c != Color.RED) {
                            newSucc.parent = redState;
                            newSucc.parentInput = j;
                            incorporate(newSucc);
                            if (c != Color.BLUE) {
                                newFrontierConsumer.accept(newSucc.makeBlue());
                            }
                        }
                    }
                }
            }

            SP newProp = propMod.get(i);
            if (newProp != null) {
                redState.property = newProp;
            }
            ArrayStorage<TP> newTransProps = transPropMod.get(i);
            if (newTransProps != null) {
                redState.transProperties = newTransProps;
            }
        }
    }

    private void incorporate(S state) {
        if (!state.isCopy) {
            return;
        }
        state.isCopy = false;
        Deque<S> queue = new ArrayDeque<>();
        queue.offer(state);

        S curr;

        while ((curr = queue.poll()) != null) {
            ArrayStorage<S> succs = curr.successors;
            if (succs == null) {
                continue;
            }
            for (int i = 0; i < alphabetSize; i++) {
                S succ = succs.get(i);
                if (succ != null) {
                    succ.parent = curr;
                    succ.parentInput = i;
                    if (succ.isCopy) {
                        succ.isCopy = false;
                        queue.offer(succ);
                    }
                }
            }
        }
    }

    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>() {

            private 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);
            }

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

                return state.getStateProperty();
            }

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

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

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

            @Override
            public Pair<S, Integer> getTransition(S state, Integer input) {
                return Pair.of(state, input);
            }

            @Override
            public Collection<S> getStates() {

                if (states != null) {
                    return states;
                }

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

                S initialState = getInitialState();
                assert initialState != null;
                discoverQueue.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)) {
                            discoverQueue.add(succ);
                        }
                    }
                }

                return states;
            }

            @Override
            public S getInitialState() {
                return pta.getInitialState();
            }
        };
    }

    static final class FoldRecord<S extends AbstractBlueFringePTAState<S, ?, ?>> {

        public final S r;
        public S q;
        public int i = -1;

        FoldRecord(S q, S r) {
            this.q = q;
            this.r = r;
        }
    }
}

1	/* Copyright (C) 2013-2023 TU Dortmund
2	* This file is part of LearnLib, http://www.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;
17
18	import java.awt.Color;
19	import java.util.ArrayDeque;
20	import java.util.Collection;
21	import java.util.Deque;
22	import java.util.HashSet;
23	import java.util.Iterator;
24	import java.util.Objects;
25	import java.util.Queue;
26	import java.util.Set;
27	import java.util.function.Consumer;
28
29	import net.automatalib.automaton.UniversalDeterministicAutomaton;
30	import net.automatalib.common.smartcollection.ArrayStorage;
31	import net.automatalib.common.util.Pair;
32	import org.checkerframework.checker.nullness.qual.Nullable;
33
34	public class RedBlueMerge<S extends AbstractBlueFringePTAState<S, SP, TP>, SP, TP> {	2✔
35
36	private final AbstractBlueFringePTA<S, SP, TP> pta;
37	private final ArrayStorage<ArrayStorage<S>> succMod;
38	private final ArrayStorage<ArrayStorage<TP>> transPropMod;
39	private final ArrayStorage<SP> propMod;
40	private final int alphabetSize;
41	private final S qr;
42	private final S qb;
43	private boolean merged;
44
45	public RedBlueMerge(AbstractBlueFringePTA<S, SP, TP> pta, S qr, S qb) {	2✔
46	if (!qr.isRed()) {	2✔
47	throw new IllegalArgumentException("Merge target must be a red state");	×
48	}
49	if (!qb.isBlue()) {	2✔
50	throw new IllegalArgumentException("Merge source must be a blue state");	×
51	}
52
53	this.pta = pta;	2✔
54
55	int numRedStates = pta.getNumRedStates();	2✔
56	this.succMod = new ArrayStorage<>(numRedStates);	2✔
57	this.transPropMod = new ArrayStorage<>(numRedStates);	2✔
58	this.propMod = new ArrayStorage<>(numRedStates);	2✔
59	this.alphabetSize = pta.getInputAlphabet().size();	2✔
60
61	this.qr = qr;	2✔
62	this.qb = qb;	2✔
63	}	2✔
64
65	public S getRedState() {
66	return qr;	×
67	}
68
69	public S getBlueState() {
70	return qb;	×
71	}
72
73	public boolean merge() {
74	this.merged = true;	2✔
75	if (!mergeRedProperties(qr, qb)) {	2✔
76	return false;	1✔
77	}
78	updateRedTransition(qb.parent, qb.parentInput, qr);	2✔
79
80	Deque<FoldRecord<S>> stack = new ArrayDeque<>();	2✔
81	stack.push(new FoldRecord<>(qr, qb));	2✔
82
83	FoldRecord<S> curr;
84	while ((curr = stack.peek()) != null) {	2✔
85	int i = ++curr.i;	2✔
86
87	if (i == alphabetSize) {	2✔
88	stack.pop();	2✔
89	continue;	2✔
90	}
91
92	S q = curr.q;	2✔
93	S r = curr.r;	2✔
94
95	S rSucc = r.getSuccessor(i);	2✔
96	if (rSucc != null) {	2✔
97	S qSucc = getSucc(q, i);	2✔
98	if (qSucc != null) {	2✔
99	if (qSucc.isRed()) {	2✔
100	if (!mergeRedProperties(qSucc, rSucc)) {	1✔
101	return false;	1✔
102	}
103	} else {
104	SP rSuccSP = rSucc.property, qSuccSP = qSucc.property;	2✔
105
106	SP newSP = null;	2✔
107	if (qSuccSP == null && rSuccSP != null) {	2✔
108	newSP = rSuccSP;	1✔
109	} else if (rSuccSP != null && !rSuccSP.equals(qSuccSP)) {	2✔
110	return false;	1✔
111	}
112
113	ArrayStorage<TP> newTPs = null;	2✔
114	ArrayStorage<TP> rSuccTPs = rSucc.transProperties;	2✔
115	ArrayStorage<TP> qSuccTPs = qSucc.transProperties;	2✔
116
117	if (rSuccTPs != null) {	2✔
118	if (qSuccTPs != null) {	1✔
119	ArrayStorage<TP> mergedTPs = mergeTransProperties(qSuccTPs, rSuccTPs);	1✔
120	if (mergedTPs == null) {	1✔
121	return false;	1✔
122	} else if (mergedTPs != qSuccTPs) {	1✔
123	newTPs = mergedTPs;	1✔
124	}
125	} else {	1✔
126	newTPs = rSuccTPs.clone();	1✔
127	}
128	}
129
130	if (newSP != null \|\| newTPs != null) {	2✔
131	qSucc = cloneTopSucc(qSucc, i, stack, newTPs);	1✔
132	if (newSP != null) {	1✔
133	qSucc.property = newSP;	1✔
134	}
135	}
136	}
137
138	stack.push(new FoldRecord<>(qSucc, rSucc));	2✔
139	} else {
140	if (q.isRed()) {	2✔
141	updateRedTransition(q, i, rSucc, r.getTransProperty(i));	2✔
142	} else {
143	q = cloneTop(q, stack);	1✔
144	assert q.isCopy;	1✔
145	q.setForeignSuccessor(i, rSucc, alphabetSize);	1✔
146	}
147	}
148	}
149	}	2✔
150
151	return true;	2✔
152	}
153
154	private S cloneTopSucc(S succ, int i, Deque<FoldRecord<S>> stack, @Nullable ArrayStorage<TP> newTPs) {
155	S succClone = (newTPs != null) ? succ.copy(newTPs) : succ.copy();	1✔
156	if (succClone == succ) {	1✔
157	return succ;	×
158	}
159	FoldRecord<S> peek = stack.peek();	1✔
160	assert peek != null;	1✔
161	S top = peek.q;	1✔
162	if (top.isRed()) {	1✔
163	updateRedTransition(top, i, succClone);	1✔
164	} else {
165	S topClone = cloneTop(top, stack);	1✔
166	topClone.setForeignSuccessor(i, succClone, alphabetSize);	1✔
167	}
168	return succClone;	1✔
169	}
170
171	private S cloneTop(S topState, Deque<FoldRecord<S>> stack) {
172	assert !topState.isRed();	1✔
173
174	S topClone = topState.copy();	1✔
175	if (topClone == topState) {	1✔
176	return topState;	×
177	}
178	S currTgt = topClone;	1✔
179
180	Iterator<FoldRecord<S>> it = stack.iterator();	1✔
181	FoldRecord<S> currRec = it.next();	1✔
182	assert currRec.q == topState;	1✔
183	currRec.q = topClone;	1✔
184
185	assert it.hasNext();	1✔
186	currRec = it.next();	1✔
187	S currSrc = currRec.q;	1✔
188
189	while (!currSrc.isRed()) {	1✔
190	S currSrcClone = currSrc.copy();	1✔
191	assert currSrcClone.successors != null;	1✔
192	currSrcClone.successors.set(currRec.i, currTgt);	1✔
193	if (currSrcClone == currSrc) {	1✔
194	return topClone; // we're done	×
195	}
196	currRec.q = currSrcClone;	1✔
197	currTgt = currSrcClone;	1✔
198
199	assert it.hasNext();	1✔
200	currRec = it.next();	1✔
201	currSrc = currRec.q;	1✔
202	}	1✔
203
204	assert currSrc.isRed();	1✔
205	updateRedTransition(currSrc, currRec.i, currTgt);	1✔
206
207	return topClone;	1✔
208	}
209
210	private @Nullable ArrayStorage<TP> getTransProperties(S q) {
211	if (q.isRed()) {	1✔
212	int qId = q.id;	1✔
213	ArrayStorage<TP> props = transPropMod.get(qId);	1✔
214	if (props != null) {	1✔
215	return props;	1✔
216	}
217	}
218	return q.transProperties;	1✔
219	}
220
221	private SP getStateProperty(S q) {
222	if (q.isRed()) {	1✔
223	int qId = q.id;	1✔
224	SP prop = propMod.get(qId);	1✔
225	if (prop != null) {	1✔
226	return prop;	1✔
227	}
228	}
229	return q.property;	1✔
230	}
231
232	private @Nullable S getSucc(S q, int i) {
233	if (q.isRed()) {	2✔
234	int qId = q.id;	2✔
235	ArrayStorage<S> modSuccs = succMod.get(qId);	2✔
236	if (modSuccs != null) {	2✔
237	return modSuccs.get(i);	2✔
238	}
239	}
240	return q.getSuccessor(i);	2✔
241	}
242
243	private void updateRedTransition(S redSrc, int input, S tgt) {
244	updateRedTransition(redSrc, input, tgt, null);	2✔
245	}	2✔
246
247	private void updateRedTransition(S redSrc, int input, S tgt, @Nullable TP transProp) {
248	assert redSrc.isRed();	2✔
249
250	int id = redSrc.id;	2✔
251	ArrayStorage<S> newSuccs = succMod.get(id);	2✔
252	if (newSuccs == null) {	2✔
253	if (redSrc.successors == null) {	2✔
254	newSuccs = new ArrayStorage<>(alphabetSize);	×
255	} else {
256	newSuccs = redSrc.successors.clone();	2✔
257	}
258	succMod.set(id, newSuccs);	2✔
259	}
260	newSuccs.set(input, tgt);	2✔
261	if (transProp != null) {	2✔
262	ArrayStorage<TP> newTransProps = transPropMod.get(id);	1✔
263	if (newTransProps == null) {	1✔
264	if (redSrc.transProperties == null) {	×
265	newTransProps = new ArrayStorage<>(alphabetSize);	×
266	} else {
267	newTransProps = redSrc.transProperties.clone();	×
268	}
269	transPropMod.set(id, newTransProps);	×
270	}
271	newTransProps.set(input, transProp);	1✔
272	}
273	}	2✔
274
275	private boolean mergeRedProperties(S qr, S qb) {
276	return mergeRedStateProperty(qr, qb) && mergeRedTransProperties(qr, qb);	2✔
277	}
278
279	private boolean mergeRedTransProperties(S qr, S qb) {
280	assert qr.isRed();	2✔
281
282	ArrayStorage<TP> qbProps = qb.transProperties;	2✔
283	if (qbProps == null) {	2✔
284	return true;	2✔
285	}
286	ArrayStorage<TP> qrProps = getTransProperties(qr);	1✔
287	ArrayStorage<TP> mergedProps = qbProps;	1✔
288	if (qrProps != null) {	1✔
289	mergedProps = mergeTransProperties(qrProps, qbProps);	1✔
290	if (mergedProps == null) {	1✔
291	return false;	1✔
292	}
293	}
294	if (mergedProps != qrProps) {	1✔
295	transPropMod.set(qr.id, mergedProps);	1✔
296	}
297	return true;	1✔
298	}
299
300	private boolean mergeRedStateProperty(S qr, S qb) {
301	assert qr.isRed();	2✔
302
303	SP qbProp = qb.property;	2✔
304	if (qbProp == null) {	2✔
305	return true;	2✔
306	}
307	SP qrProp = getStateProperty(qr);	1✔
308	if (qrProp != null) {	1✔
309	return Objects.equals(qbProp, qrProp);	1✔
310	}
311	propMod.set(qr.id, qbProp);	1✔
312	return true;	1✔
313	}
314
315	/**
316	* Merges two non-null transition property arrays. The behavior of this method is as follows: <ul> <li>if {@code
317	* tps1} subsumes {@code tps2}, then {@code tps1} is returned.</li> <li>otherwise, if {@code tps1} and {@code tps2}
318	* can be merged, a new {@link ArrayStorage} containing the result of the merge is returned. <li>otherwise
319	* (i.e., if no merge is possible), {@code null} is returned. </ul>
320	*/
321	private @Nullable ArrayStorage<TP> mergeTransProperties(ArrayStorage<TP> tps1, ArrayStorage<TP> tps2) {
322	int len = tps1.size();	1✔
323	int i;
324
325	ArrayStorage<TP> tps1OrCopy = tps1;	1✔
326
327	for (i = 0; i < len; i++) {	1✔
328	TP tp1 = tps1OrCopy.get(i);	1✔
329	TP tp2 = tps2.get(i);	1✔
330	if (tp2 != null) {	1✔
331	if (tp1 != null) {	1✔
332	if (!Objects.equals(tp1, tp2)) {	1✔
333	return null;	1✔
334	}
335	} else {
336	tps1OrCopy = tps1.clone();	1✔
337	tps1OrCopy.set(i++, tp2);	1✔
338	break;	1✔
339	}
340	}
341	}
342
343	for (; i < len; i++) {	1✔
344	TP tp1 = tps1OrCopy.get(i);	1✔
345	TP tp2 = tps2.get(i);	1✔
346	if (tp2 != null) {	1✔
347	if (tp1 != null) {	1✔
348	if (!Objects.equals(tp1, tp2)) {	1✔
349	return null;	1✔
350	}
351	} else {
352	tps1OrCopy.set(i, tp2);	1✔
353	}
354	}
355	}
356
357	return tps1OrCopy;	1✔
358	}
359
360	public void apply(AbstractBlueFringePTA<S, SP, TP> pta, Consumer<? super PTATransition<S>> newFrontierConsumer) {
361	int alphabetSize = pta.getInputAlphabet().size();	1✔
362
363	for (int i = 0; i < succMod.size(); i++) {	1✔
364	S redState = pta.redStates.get(i);	1✔
365	assert redState.isRed();	1✔
366	ArrayStorage<S> newSuccs = succMod.get(i);	1✔
367	if (newSuccs != null) {	1✔
368	int len = newSuccs.size();	1✔
369	for (int j = 0; j < len; j++) {	1✔
370	S newSucc = newSuccs.get(j);	1✔
371	if (newSucc != null) {	1✔
372	redState.setForeignSuccessor(j, newSucc, alphabetSize);	1✔
373	Color c = newSucc.getColor();	1✔
374	if (c != Color.RED) {	1✔
375	newSucc.parent = redState;	1✔
376	newSucc.parentInput = j;	1✔
377	incorporate(newSucc);	1✔
378	if (c != Color.BLUE) {	1✔
379	newFrontierConsumer.accept(newSucc.makeBlue());	1✔
380	}
381	}
382	}
383	}
384	}
385
386	SP newProp = propMod.get(i);	1✔
387	if (newProp != null) {	1✔
388	redState.property = newProp;	1✔
389	}
390	ArrayStorage<TP> newTransProps = transPropMod.get(i);	1✔
391	if (newTransProps != null) {	1✔
392	redState.transProperties = newTransProps;	1✔
393	}
394	}
395	}	1✔
396
397	private void incorporate(S state) {
398	if (!state.isCopy) {	1✔
399	return;	1✔
400	}
401	state.isCopy = false;	1✔
402	Deque<S> queue = new ArrayDeque<>();	1✔
403	queue.offer(state);	1✔
404
405	S curr;
406
407	while ((curr = queue.poll()) != null) {	1✔
408	ArrayStorage<S> succs = curr.successors;	1✔
409	if (succs == null) {	1✔
410	continue;	×
411	}
412	for (int i = 0; i < alphabetSize; i++) {	1✔
413	S succ = succs.get(i);	1✔
414	if (succ != null) {	1✔
415	succ.parent = curr;	1✔
416	succ.parentInput = i;	1✔
417	if (succ.isCopy) {	1✔
418	succ.isCopy = false;	1✔
419	queue.offer(succ);	1✔
420	}
421	}
422	}
423	}	1✔
424	}	1✔
425
426	public UniversalDeterministicAutomaton<S, Integer, ?, SP, TP> toMergedAutomaton() {
427	if (!this.merged) {	2✔
428	throw new IllegalStateException("#merge has not been called yet");	×
429	}
430
431	return new UniversalDeterministicAutomaton<S, Integer, Pair<S, Integer>, SP, TP>() {	2✔
432
433	private Set<S> states;
434
435	@Override
436	public @Nullable S getSuccessor(Pair<S, Integer> transition) {
437	final S source = transition.getFirst();	2✔
438	final Integer input = transition.getSecond();	2✔
439
440	if (source.isRed() && succMod.get(source.id) != null) {	2✔
441	return succMod.get(source.id).get(input);	2✔
442	}
443
444	return pta.getSuccessor(source, input);	2✔
445	}
446
447	@Override
448	public SP getStateProperty(S state) {
449	if (state.isRed() && propMod.get(state.id) != null) {	1✔
450	return propMod.get(state.id);	1✔
451	}
452
453	return state.getStateProperty();	1✔
454	}
455
456	@Override
457	public TP getTransitionProperty(Pair<S, Integer> transition) {
458	final S source = transition.getFirst();	×
459	final Integer input = transition.getSecond();	×
460
461	if (source.isRed() && transPropMod.get(source.id) != null) {	×
462	return transPropMod.get(source.id).get(input);	×
463	}
464
465	assert source.transProperties != null;	×
466	return source.transProperties.get(input);	×
467	}
468
469	@Override
470	public Pair<S, Integer> getTransition(S state, Integer input) {
471	return Pair.of(state, input);	2✔
472	}
473
474	@Override
475	public Collection<S> getStates() {
476
477	if (states != null) {	2✔
478	return states;	×
479	}
480
481	states = new HashSet<>();	2✔
482	final Queue<S> discoverQueue = new ArrayDeque<>();	2✔
483
484	S initialState = getInitialState();	2✔
485	assert initialState != null;	2✔
486	discoverQueue.add(initialState);	2✔
487
488	S iter;
489
490	while ((iter = discoverQueue.poll()) != null) {	2✔
491	states.add(iter);	2✔
492
493	for (int i = 0; i < alphabetSize; i++) {	2✔
494	final S succ = getSuccessor(iter, i);	2✔
495
496	if (succ != null && !states.contains(succ)) {	2✔
497	discoverQueue.add(succ);	2✔
498	}
499	}
500	}
501
502	return states;	2✔
503	}
504
505	@Override
506	public S getInitialState() {
507	return pta.getInitialState();	2✔
508	}
509	};
510	}
511
512	static final class FoldRecord<S extends AbstractBlueFringePTAState<S, ?, ?>> {
513
514	public final S r;
515	public S q;
516	public int i = -1;	2✔
517
518	FoldRecord(S q, S r) {	2✔
519	this.q = q;	2✔
520	this.r = r;	2✔
521	}	2✔
522	}
523	}

LearnLib / learnlib / 6611855081

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous