6433387082

Committed 06 Oct 2023 03:10PM UTC coverage: 92.296% (-0.007%) from 92.303%

Build # 6433387082

Build Type

push

github

Committed by

mtf90

Commit Message

update Falk's developer id

Run Details

11573 of 12539 relevant lines covered (92.3%)

1.67 hits per line

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

97.3

/algorithms/active/ttt/src/main/java/de/learnlib/algorithms/ttt/dfa/PrefixTTTLearnerDFA.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.algorithms.ttt.dfa;

import java.util.Iterator;

import com.google.common.collect.AbstractIterator;
import de.learnlib.acex.AbstractCounterexample;
import de.learnlib.acex.AcexAnalyzer;
import de.learnlib.algorithms.ttt.base.TTTState;
import de.learnlib.algorithms.ttt.base.TTTTransition;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import net.automatalib.commons.smartcollections.ArrayStorage;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;

public class PrefixTTTLearnerDFA<I> extends TTTLearnerDFA<I> {

    private final ExtDTNode<I> unlabeledList = new ExtDTNode<>();

    public PrefixTTTLearnerDFA(Alphabet<I> alphabet, MembershipOracle<I, Boolean> oracle, AcexAnalyzer analyzer) {
        super(alphabet, oracle, analyzer, ExtDTNode::new);
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
        boolean refined = refineHypothesisSingle(ceQuery);
        if (!refined) {
            return false;
        }

        while (refineHypothesisSingle(ceQuery)) {}

        return true;
    }

    @Override
    protected boolean refineHypothesisSingle(DefaultQuery<I, Boolean> ceQuery) {
        if (getHypothesisModel().computeSuffixOutput(ceQuery.getPrefix(), ceQuery.getSuffix())
                                .equals(ceQuery.getOutput())) {
            return false;
        }

        Word<I> ceWord = ceQuery.getInput();
        int currReachInconsLength = ceWord.length();

        EasyTTTPrefAcex acex = new EasyTTTPrefAcex(ceWord);
        do {
            acex.update(currReachInconsLength);
            int breakpoint = analyzer.analyzeAbstractCounterexample(acex, 0, currReachInconsLength);
            ExtDTNode<I> toSplit = acex.getHypNode(breakpoint);
            TTTState<I, Boolean> splitState = toSplit.getData();
            ExtDTNode<I> lca = acex.getLCA(breakpoint + 1);
            I sym = ceWord.getSymbol(breakpoint);
            Word<I> newDiscr = lca.getDiscriminator().prepend(sym);
            ExtDTNode<I> succHyp = acex.getHypNode(breakpoint + 1);
            Boolean hypOut = lca.subtreeLabel(succHyp);
            assert hypOut != null;
            openTransitions.insertAllIncoming(toSplit.getIncoming());
            ExtDTNode<I>.SplitResult splitResult = toSplit.split(newDiscr, hypOut, !hypOut);
            link(splitResult.nodeOld, splitState);
            ExtDTNode<I> extUnlabeled = (ExtDTNode<I>) splitResult.nodeNew;
            extUnlabeled.tempPrefix = currReachInconsLength;
            unlabeledList.addUnlabeled(extUnlabeled);
            closeTransitions();

            currReachInconsLength = findMinReachIncons();
        } while (currReachInconsLength != -1);

        return true;
    }

    @Override
    protected TTTState<I, Boolean> makeTree(TTTTransition<I, Boolean> trans) {
        ExtDTNode<I> node = (ExtDTNode<I>) trans.getNonTreeTarget();
        if (node.tempPrefix != -1) {
            node.removeFromUnlabeledList();
        }
        return super.makeTree(trans);
    }

    private int findMinReachIncons() {
        int minLength = -1;
        for (ExtDTNode<I> n : unlabeledList.unlabeled()) {
            int len = n.tempPrefix;
            if (minLength == -1 || len < minLength) {
                minLength = len;
            }
        }
        return minLength;
    }

    protected static class ExtDTNode<I> extends TTTDTNodeDFA<I> {

        private ExtDTNode<I> prevUnlabeled, nextUnlabeled;
        private int tempPrefix = -1;

        public ExtDTNode() {
            // default constructor
        }

        public ExtDTNode(ExtDTNode<I> parent, Boolean parentOut) {
            super(parent, parentOut);
        }

        public void removeFromUnlabeledList() {
            prevUnlabeled.nextUnlabeled = nextUnlabeled;
            if (nextUnlabeled != null) {
                nextUnlabeled.prevUnlabeled = prevUnlabeled;
            }
        }

        @Override
        protected ExtDTNode<I> createChild(Boolean outcome, TTTState<I, Boolean> data) {
            return new ExtDTNode<>(this, outcome);
        }

        public boolean hasUnlabeled() {
            return nextUnlabeled != null;
        }

        public void addUnlabeled(ExtDTNode<I> node) {
            node.nextUnlabeled = nextUnlabeled;
            if (nextUnlabeled != null) {
                nextUnlabeled.prevUnlabeled = node;
            }
            node.prevUnlabeled = this;
            this.nextUnlabeled = node;
        }

        public Iterable<ExtDTNode<I>> unlabeled() {
            return this::unlabeledIterator;
        }

        public Iterator<ExtDTNode<I>> unlabeledIterator() {
            return new UnlabeledIterator<>(this);
        }

        private static class UnlabeledIterator<I> extends AbstractIterator<ExtDTNode<I>> {

            private ExtDTNode<I> curr;

            UnlabeledIterator(ExtDTNode<I> curr) {
                this.curr = curr;
            }

            @Override
            protected ExtDTNode<I> computeNext() {
                curr = curr.nextUnlabeled;
                if (curr == null) {
                    return endOfData();
                }
                return curr;
            }
        }
    }

    private final class EasyTTTPrefAcex implements AbstractCounterexample<Boolean> {

        private final Word<I> ceWord;
        private final ArrayStorage<ExtDTNode<I>> hypNodes;
        private final ArrayStorage<ExtDTNode<I>> siftNodes;

        EasyTTTPrefAcex(Word<I> ceWord) {
            this.ceWord = ceWord;
            this.hypNodes = new ArrayStorage<>(ceWord.length() + 1);
            this.siftNodes = new ArrayStorage<>(ceWord.length() + 1);

            update(ceWord.length());
        }

        public void update(int len) {
            TTTStateDFA<I> curr = (TTTStateDFA<I>) hypothesis.getInitialState();
            assert curr != null;
            hypNodes.set(0, (ExtDTNode<I>) curr.getDTLeaf());
            siftNodes.set(0, (ExtDTNode<I>) curr.getDTLeaf());

            boolean wasTree = true;
            for (int i = 0; i < len; i++) {
                I sym = ceWord.getSymbol(i);
                TTTTransition<I, Boolean> trans = hypothesis.getInternalTransition(curr, sym);
                curr = (TTTStateDFA<I>) trans.getTarget();

                hypNodes.set(i + 1, (ExtDTNode<I>) curr.getDTLeaf());
                if (wasTree) {
                    siftNodes.set(i + 1, (ExtDTNode<I>) curr.getDTLeaf());
                    if (!trans.isTree()) {
                        wasTree = false;
                    }
                }

            }
        }

        @Override
        public int getLength() {
            return ceWord.length() + 1;
        }

        @Override
        public boolean checkEffects(Boolean eff1, Boolean eff2) {
            return !eff1 || eff2;
        }

        @Override
        public Boolean effect(int index) {
            ExtDTNode<I> hypNode = hypNodes.get(index);
            ExtDTNode<I> siftNode = siftNodes.get(index);
            if (siftNode == null) {
                siftNode = (ExtDTNode<I>) dtree.getRoot();
            }

            ExtDTNode<I> lca = (ExtDTNode<I>) dtree.leastCommonAncestor(hypNode, siftNode);
            Word<I> cePref = ceWord.prefix(index);
            while (lca == siftNode && siftNode != hypNode) {
                Boolean out = oracle.answerQuery(cePref, siftNode.getDiscriminator());
                siftNode = (ExtDTNode<I>) siftNode.getChild(out);
                lca = (ExtDTNode<I>) dtree.leastCommonAncestor(hypNode, siftNode);
            }
            siftNodes.set(index, siftNode);

            return siftNode == hypNode;
        }

        public ExtDTNode<I> getLCA(int index) {
            return (ExtDTNode<I>) dtree.leastCommonAncestor(hypNodes.get(index), siftNodes.get(index));
        }

        public ExtDTNode<I> getHypNode(int index) {
            return hypNodes.get(index);
        }

    }

}

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.algorithms.ttt.dfa;
17
18	import java.util.Iterator;
19
20	import com.google.common.collect.AbstractIterator;
21	import de.learnlib.acex.AbstractCounterexample;
22	import de.learnlib.acex.AcexAnalyzer;
23	import de.learnlib.algorithms.ttt.base.TTTState;
24	import de.learnlib.algorithms.ttt.base.TTTTransition;
25	import de.learnlib.api.oracle.MembershipOracle;
26	import de.learnlib.api.query.DefaultQuery;
27	import net.automatalib.commons.smartcollections.ArrayStorage;
28	import net.automatalib.words.Alphabet;
29	import net.automatalib.words.Word;
30
31	public class PrefixTTTLearnerDFA<I> extends TTTLearnerDFA<I> {	2✔
32
33	private final ExtDTNode<I> unlabeledList = new ExtDTNode<>();	2✔
34
35	public PrefixTTTLearnerDFA(Alphabet<I> alphabet, MembershipOracle<I, Boolean> oracle, AcexAnalyzer analyzer) {
36	super(alphabet, oracle, analyzer, ExtDTNode::new);	2✔
37	}	2✔
38
39	@Override
40	public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
41	boolean refined = refineHypothesisSingle(ceQuery);	2✔
42	if (!refined) {	2✔
43	return false;	×
44	}
45
46	while (refineHypothesisSingle(ceQuery)) {}	2✔
47
48	return true;	2✔
49	}
50
51	@Override
52	protected boolean refineHypothesisSingle(DefaultQuery<I, Boolean> ceQuery) {
53	if (getHypothesisModel().computeSuffixOutput(ceQuery.getPrefix(), ceQuery.getSuffix())	2✔
54	.equals(ceQuery.getOutput())) {	2✔
55	return false;	2✔
56	}
57
58	Word<I> ceWord = ceQuery.getInput();	2✔
59	int currReachInconsLength = ceWord.length();	2✔
60
61	EasyTTTPrefAcex acex = new EasyTTTPrefAcex(ceWord);	2✔
62	do {
63	acex.update(currReachInconsLength);	2✔
64	int breakpoint = analyzer.analyzeAbstractCounterexample(acex, 0, currReachInconsLength);	2✔
65	ExtDTNode<I> toSplit = acex.getHypNode(breakpoint);	2✔
66	TTTState<I, Boolean> splitState = toSplit.getData();	2✔
67	ExtDTNode<I> lca = acex.getLCA(breakpoint + 1);	2✔
68	I sym = ceWord.getSymbol(breakpoint);	2✔
69	Word<I> newDiscr = lca.getDiscriminator().prepend(sym);	2✔
70	ExtDTNode<I> succHyp = acex.getHypNode(breakpoint + 1);	2✔
71	Boolean hypOut = lca.subtreeLabel(succHyp);	2✔
72	assert hypOut != null;	2✔
73	openTransitions.insertAllIncoming(toSplit.getIncoming());	2✔
74	ExtDTNode<I>.SplitResult splitResult = toSplit.split(newDiscr, hypOut, !hypOut);	2✔
75	link(splitResult.nodeOld, splitState);	2✔
76	ExtDTNode<I> extUnlabeled = (ExtDTNode<I>) splitResult.nodeNew;	2✔
77	extUnlabeled.tempPrefix = currReachInconsLength;	2✔
78	unlabeledList.addUnlabeled(extUnlabeled);	2✔
79	closeTransitions();	2✔
80
81	currReachInconsLength = findMinReachIncons();	2✔
82	} while (currReachInconsLength != -1);	2✔
83
84	return true;	2✔
85	}
86
87	@Override
88	protected TTTState<I, Boolean> makeTree(TTTTransition<I, Boolean> trans) {
89	ExtDTNode<I> node = (ExtDTNode<I>) trans.getNonTreeTarget();	2✔
90	if (node.tempPrefix != -1) {	2✔
91	node.removeFromUnlabeledList();	2✔
92	}
93	return super.makeTree(trans);	2✔
94	}
95
96	private int findMinReachIncons() {
97	int minLength = -1;	2✔
98	for (ExtDTNode<I> n : unlabeledList.unlabeled()) {	2✔
99	int len = n.tempPrefix;	2✔
100	if (minLength == -1 \|\| len < minLength) {	2✔
101	minLength = len;	2✔
102	}
103	}	2✔
104	return minLength;	2✔
105	}
106
107	protected static class ExtDTNode<I> extends TTTDTNodeDFA<I> {
108
109	private ExtDTNode<I> prevUnlabeled, nextUnlabeled;
110	private int tempPrefix = -1;	2✔
111
112	public ExtDTNode() {	2✔
113	// default constructor
114	}	2✔
115
116	public ExtDTNode(ExtDTNode<I> parent, Boolean parentOut) {
117	super(parent, parentOut);	2✔
118	}	2✔
119
120	public void removeFromUnlabeledList() {
121	prevUnlabeled.nextUnlabeled = nextUnlabeled;	2✔
122	if (nextUnlabeled != null) {	2✔
123	nextUnlabeled.prevUnlabeled = prevUnlabeled;	2✔
124	}
125	}	2✔
126
127	@Override
128	protected ExtDTNode<I> createChild(Boolean outcome, TTTState<I, Boolean> data) {
129	return new ExtDTNode<>(this, outcome);	2✔
130	}
131
132	public boolean hasUnlabeled() {
133	return nextUnlabeled != null;	×
134	}
135
136	public void addUnlabeled(ExtDTNode<I> node) {
137	node.nextUnlabeled = nextUnlabeled;	2✔
138	if (nextUnlabeled != null) {	2✔
139	nextUnlabeled.prevUnlabeled = node;	2✔
140	}
141	node.prevUnlabeled = this;	2✔
142	this.nextUnlabeled = node;	2✔
143	}	2✔
144
145	public Iterable<ExtDTNode<I>> unlabeled() {
146	return this::unlabeledIterator;	2✔
147	}
148
149	public Iterator<ExtDTNode<I>> unlabeledIterator() {
150	return new UnlabeledIterator<>(this);	2✔
151	}
152
153	private static class UnlabeledIterator<I> extends AbstractIterator<ExtDTNode<I>> {
154
155	private ExtDTNode<I> curr;
156
157	UnlabeledIterator(ExtDTNode<I> curr) {	2✔
158	this.curr = curr;	2✔
159	}	2✔
160
161	@Override
162	protected ExtDTNode<I> computeNext() {
163	curr = curr.nextUnlabeled;	2✔
164	if (curr == null) {	2✔
165	return endOfData();	2✔
166	}
167	return curr;	2✔
168	}
169	}
170	}
171
172	private final class EasyTTTPrefAcex implements AbstractCounterexample<Boolean> {	2✔
173
174	private final Word<I> ceWord;
175	private final ArrayStorage<ExtDTNode<I>> hypNodes;
176	private final ArrayStorage<ExtDTNode<I>> siftNodes;
177
178	EasyTTTPrefAcex(Word<I> ceWord) {	2✔
179	this.ceWord = ceWord;	2✔
180	this.hypNodes = new ArrayStorage<>(ceWord.length() + 1);	2✔
181	this.siftNodes = new ArrayStorage<>(ceWord.length() + 1);	2✔
182
183	update(ceWord.length());	2✔
184	}	2✔
185
186	public void update(int len) {
187	TTTStateDFA<I> curr = (TTTStateDFA<I>) hypothesis.getInitialState();	2✔
188	assert curr != null;	2✔
189	hypNodes.set(0, (ExtDTNode<I>) curr.getDTLeaf());	2✔
190	siftNodes.set(0, (ExtDTNode<I>) curr.getDTLeaf());	2✔
191
192	boolean wasTree = true;	2✔
193	for (int i = 0; i < len; i++) {	2✔
194	I sym = ceWord.getSymbol(i);	2✔
195	TTTTransition<I, Boolean> trans = hypothesis.getInternalTransition(curr, sym);	2✔
196	curr = (TTTStateDFA<I>) trans.getTarget();	2✔
197
198	hypNodes.set(i + 1, (ExtDTNode<I>) curr.getDTLeaf());	2✔
199	if (wasTree) {	2✔
200	siftNodes.set(i + 1, (ExtDTNode<I>) curr.getDTLeaf());	2✔
201	if (!trans.isTree()) {	2✔
202	wasTree = false;	2✔
203	}
204	}
205
206	}
207	}	2✔
208
209	@Override
210	public int getLength() {
211	return ceWord.length() + 1;	×
212	}
213
214	@Override
215	public boolean checkEffects(Boolean eff1, Boolean eff2) {
216	return !eff1 \|\| eff2;	2✔
217	}
218
219	@Override
220	public Boolean effect(int index) {
221	ExtDTNode<I> hypNode = hypNodes.get(index);	2✔
222	ExtDTNode<I> siftNode = siftNodes.get(index);	2✔
223	if (siftNode == null) {	2✔
224	siftNode = (ExtDTNode<I>) dtree.getRoot();	2✔
225	}
226
227	ExtDTNode<I> lca = (ExtDTNode<I>) dtree.leastCommonAncestor(hypNode, siftNode);	2✔
228	Word<I> cePref = ceWord.prefix(index);	2✔
229	while (lca == siftNode && siftNode != hypNode) {	2✔
230	Boolean out = oracle.answerQuery(cePref, siftNode.getDiscriminator());	2✔
231	siftNode = (ExtDTNode<I>) siftNode.getChild(out);	2✔
232	lca = (ExtDTNode<I>) dtree.leastCommonAncestor(hypNode, siftNode);	2✔
233	}	2✔
234	siftNodes.set(index, siftNode);	2✔
235
236	return siftNode == hypNode;	2✔
237	}
238
239	public ExtDTNode<I> getLCA(int index) {
240	return (ExtDTNode<I>) dtree.leastCommonAncestor(hypNodes.get(index), siftNodes.get(index));	2✔
241	}
242
243	public ExtDTNode<I> getHypNode(int index) {
244	return hypNodes.get(index);	2✔
245	}
246
247	}
248
249	}

LearnLib / learnlib / 6433387082

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