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

90.43

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

import java.util.LinkedHashSet;
import java.util.List;
import java.util.Objects;
import java.util.Set;

import de.learnlib.algorithms.oml.ttt.dt.AbstractDecisionTree;
import de.learnlib.algorithms.oml.ttt.dt.DTLeaf;
import de.learnlib.algorithms.oml.ttt.pt.PTNode;
import de.learnlib.algorithms.oml.ttt.pt.PrefixTree;
import de.learnlib.algorithms.oml.ttt.st.SuffixTrie;
import de.learnlib.api.algorithm.LearningAlgorithm;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import net.automatalib.SupportsGrowingAlphabet;
import net.automatalib.automata.concepts.InputAlphabetHolder;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;

public abstract class AbstractOptimalTTT<M, I, D>
        implements LearningAlgorithm<M, I, D>, SupportsGrowingAlphabet<I>, InputAlphabetHolder<I> {

    private final MembershipOracle<I, D> ceqs;
    private final Alphabet<I> alphabet;
    protected final SuffixTrie<I> strie;
    protected final PrefixTree<I, D> ptree;

    protected AbstractOptimalTTT(Alphabet<I> alphabet, MembershipOracle<I, D> ceqs) {
        this.alphabet = alphabet;
        this.ceqs = ceqs;

        this.strie = new SuffixTrie<>();
        this.ptree = new PrefixTree<>();
    }

    protected abstract int maxSearchIndex(int ceLength);

    protected abstract D hypOutput(Word<I> word, int length);

    protected abstract DTLeaf<I, D> getState(Word<I> prefix);

    protected abstract AbstractDecisionTree<I, D> dtree();

    protected abstract D suffix(D output, int length);

    protected abstract boolean isCanonical();

    @Override
    public void startLearning() {
        assert dtree() != null && getHypothesisModel() != null;
        dtree().sift(ptree.root());
        makeConsistent();
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
        Set<DefaultQuery<I, D>> witnesses = new LinkedHashSet<>();
        witnesses.add(counterexample);
        boolean refined = refineWithWitness(counterexample, witnesses);
        if (!refined) {
            return false;
        }

        if (isCanonical()) {
            return true;
        }

        do {
            for (DefaultQuery<I, D> w : witnesses) {
                refined = refineWithWitness(w, witnesses);
                if (refined) {
                    break;
                }
            }

        } while (refined && isCanonical());
        return true;
    }

    @Override
    public void addAlphabetSymbol(I symbol) {
        if (!this.alphabet.containsSymbol(symbol)) {
            Alphabets.toGrowingAlphabetOrThrowException(this.alphabet).addSymbol(symbol);
        }

        // check if symbol is already part of ptree/hypothesis
        if (ptree.root().succ(symbol) == null) {

            List<DTLeaf<I, D>> leaves = dtree().leaves();

            for (DTLeaf<I, D> leaf : leaves) {
                PTNode<I, D> u = leaf.getShortPrefixes().get(0);
                assert u != null;
                PTNode<I, D> ua = u.append(symbol);
                assert ua != null;
                dtree().sift(ua);
            }

            makeConsistent();
        }
    }

    @Override
    public Alphabet<I> getInputAlphabet() {
        return this.alphabet;
    }

    private boolean refineWithWitness(DefaultQuery<I, D> counterexample, Set<DefaultQuery<I, D>> witnesses) {
        if (counterexample.getOutput() == null) {
            counterexample.answer(ceqs.answerQuery(counterexample.getInput()));
        }
        D hypOut = hypOutput(counterexample.getInput(), counterexample.getSuffix().length());
        if (Objects.equals(hypOut, counterexample.getOutput())) {
            return false;
        }
        do {
            analyzeCounterexample(counterexample.getInput(), witnesses);
            makeConsistent();
            hypOut = hypOutput(counterexample.getInput(), counterexample.getSuffix().length());
        } while (!Objects.equals(hypOut, counterexample.getOutput()));
        return true;
    }

    private void makeConsistent() {
        while (dtree().makeConsistent()) {
            // do nothing ...
        }
    }

    private PTNode<I, D> longestShortPrefixOf(Word<I> ce) {
        PTNode<I, D> cur = ptree.root();
        int i = 0;
        do {
            cur = cur.succ(ce.getSymbol(i++));
            assert cur != null;
        } while (cur.state().getShortPrefixes().contains(cur) && i < ce.length());

        assert !cur.state().getShortPrefixes().contains(cur);
        return cur;
    }

    private void analyzeCounterexample(Word<I> ce, Set<DefaultQuery<I, D>> witnesses) {
        PTNode<I, D> ua = null;
        PTNode<I, D> lsp = longestShortPrefixOf(ce);
        int upper = maxSearchIndex(ce.length());
        int lower = lsp.word().length() -1;
        D hypOut = hypOutput(ce, ce.length());
        while (upper - lower > 1) {
            int mid = (upper + lower) / 2;
            Word<I> prefix = ce.prefix(mid);
            Word<I> suffix = ce.suffix(ce.length() - mid);

            DTLeaf<I, D> q = getState(prefix);
            assert q != null;

            boolean stillCe = false;
            for (PTNode<I, D> u : q.getShortPrefixes()) {
                D sysOut = suffix(ceqs.answerQuery(u.word(), suffix), suffix.size());
                if (!Objects.equals(sysOut, suffix(hypOut, suffix.size()))) {
                    ua = u.succ(suffix.firstSymbol());
                    lower = mid;
                    stillCe = true;
                    break;
                }
            }
            if (stillCe) {
                continue;
            }
            upper = mid;
        }

        if (ua == null) {
            assert lower == lsp.word().length()-1;
            ua = lsp;
        }

        // add witnesses
        int mid = (upper + lower) / 2;
        Word<I> sprime = ce.suffix(ce.length() - (mid + 1));
        DTLeaf<I, D> qnext = getState(ua.word());
        for (PTNode<I, D> uprime : qnext.getShortPrefixes()) {
            witnesses.add(new DefaultQuery<>(uprime.word(), sprime));
        }
        witnesses.add(new DefaultQuery<>(ua.word(), sprime));

        ua.makeShortPrefix();
    }
}

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.oml.ttt;
17
18	import java.util.LinkedHashSet;
19	import java.util.List;
20	import java.util.Objects;
21	import java.util.Set;
22
23	import de.learnlib.algorithms.oml.ttt.dt.AbstractDecisionTree;
24	import de.learnlib.algorithms.oml.ttt.dt.DTLeaf;
25	import de.learnlib.algorithms.oml.ttt.pt.PTNode;
26	import de.learnlib.algorithms.oml.ttt.pt.PrefixTree;
27	import de.learnlib.algorithms.oml.ttt.st.SuffixTrie;
28	import de.learnlib.api.algorithm.LearningAlgorithm;
29	import de.learnlib.api.oracle.MembershipOracle;
30	import de.learnlib.api.query.DefaultQuery;
31	import net.automatalib.SupportsGrowingAlphabet;
32	import net.automatalib.automata.concepts.InputAlphabetHolder;
33	import net.automatalib.words.Alphabet;
34	import net.automatalib.words.Word;
35	import net.automatalib.words.impl.Alphabets;
36
37	public abstract class AbstractOptimalTTT<M, I, D>	2✔
38	implements LearningAlgorithm<M, I, D>, SupportsGrowingAlphabet<I>, InputAlphabetHolder<I> {
39
40	private final MembershipOracle<I, D> ceqs;
41	private final Alphabet<I> alphabet;
42	protected final SuffixTrie<I> strie;
43	protected final PrefixTree<I, D> ptree;
44
45	protected AbstractOptimalTTT(Alphabet<I> alphabet, MembershipOracle<I, D> ceqs) {	2✔
46	this.alphabet = alphabet;	2✔
47	this.ceqs = ceqs;	2✔
48
49	this.strie = new SuffixTrie<>();	2✔
50	this.ptree = new PrefixTree<>();	2✔
51	}	2✔
52
53	protected abstract int maxSearchIndex(int ceLength);
54
55	protected abstract D hypOutput(Word<I> word, int length);
56
57	protected abstract DTLeaf<I, D> getState(Word<I> prefix);
58
59	protected abstract AbstractDecisionTree<I, D> dtree();
60
61	protected abstract D suffix(D output, int length);
62
63	protected abstract boolean isCanonical();
64
65	@Override
66	public void startLearning() {
67	assert dtree() != null && getHypothesisModel() != null;	2✔
68	dtree().sift(ptree.root());	2✔
69	makeConsistent();	2✔
70	}	2✔
71
72	@Override
73	public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
74	Set<DefaultQuery<I, D>> witnesses = new LinkedHashSet<>();	2✔
75	witnesses.add(counterexample);	2✔
76	boolean refined = refineWithWitness(counterexample, witnesses);	2✔
77	if (!refined) {	2✔
78	return false;	2✔
79	}
80
81	if (isCanonical()) {	2✔
82	return true;	2✔
83	}
84
85	do {
86	for (DefaultQuery<I, D> w : witnesses) {	×
87	refined = refineWithWitness(w, witnesses);	×
88	if (refined) {	×
89	break;	×
90	}
91	}	×
92
93	} while (refined && isCanonical());	×
94	return true;	×
95	}
96
97	@Override
98	public void addAlphabetSymbol(I symbol) {
99	if (!this.alphabet.containsSymbol(symbol)) {	2✔
100	Alphabets.toGrowingAlphabetOrThrowException(this.alphabet).addSymbol(symbol);	2✔
101	}
102
103	// check if symbol is already part of ptree/hypothesis
104	if (ptree.root().succ(symbol) == null) {	2✔
105
106	List<DTLeaf<I, D>> leaves = dtree().leaves();	2✔
107
108	for (DTLeaf<I, D> leaf : leaves) {	2✔
109	PTNode<I, D> u = leaf.getShortPrefixes().get(0);	2✔
110	assert u != null;	2✔
111	PTNode<I, D> ua = u.append(symbol);	2✔
112	assert ua != null;	2✔
113	dtree().sift(ua);	2✔
114	}	2✔
115
116	makeConsistent();	2✔
117	}
118	}	2✔
119
120	@Override
121	public Alphabet<I> getInputAlphabet() {
122	return this.alphabet;	×
123	}
124
125	private boolean refineWithWitness(DefaultQuery<I, D> counterexample, Set<DefaultQuery<I, D>> witnesses) {
126	if (counterexample.getOutput() == null) {	2✔
127	counterexample.answer(ceqs.answerQuery(counterexample.getInput()));	×
128	}
129	D hypOut = hypOutput(counterexample.getInput(), counterexample.getSuffix().length());	2✔
130	if (Objects.equals(hypOut, counterexample.getOutput())) {	2✔
131	return false;	2✔
132	}
133	do {
134	analyzeCounterexample(counterexample.getInput(), witnesses);	2✔
135	makeConsistent();	2✔
136	hypOut = hypOutput(counterexample.getInput(), counterexample.getSuffix().length());	2✔
137	} while (!Objects.equals(hypOut, counterexample.getOutput()));	2✔
138	return true;	2✔
139	}
140
141	private void makeConsistent() {
142	while (dtree().makeConsistent()) {	2✔
143	// do nothing ...
144	}
145	}	2✔
146
147	private PTNode<I, D> longestShortPrefixOf(Word<I> ce) {
148	PTNode<I, D> cur = ptree.root();	2✔
149	int i = 0;	2✔
150	do {
151	cur = cur.succ(ce.getSymbol(i++));	2✔
152	assert cur != null;	2✔
153	} while (cur.state().getShortPrefixes().contains(cur) && i < ce.length());	2✔
154
155	assert !cur.state().getShortPrefixes().contains(cur);	2✔
156	return cur;	2✔
157	}
158
159	private void analyzeCounterexample(Word<I> ce, Set<DefaultQuery<I, D>> witnesses) {
160	PTNode<I, D> ua = null;	2✔
161	PTNode<I, D> lsp = longestShortPrefixOf(ce);	2✔
162	int upper = maxSearchIndex(ce.length());	2✔
163	int lower = lsp.word().length() -1;	2✔
164	D hypOut = hypOutput(ce, ce.length());	2✔
165	while (upper - lower > 1) {	2✔
166	int mid = (upper + lower) / 2;	2✔
167	Word<I> prefix = ce.prefix(mid);	2✔
168	Word<I> suffix = ce.suffix(ce.length() - mid);	2✔
169
170	DTLeaf<I, D> q = getState(prefix);	2✔
171	assert q != null;	2✔
172
173	boolean stillCe = false;	2✔
174	for (PTNode<I, D> u : q.getShortPrefixes()) {	2✔
175	D sysOut = suffix(ceqs.answerQuery(u.word(), suffix), suffix.size());	2✔
176	if (!Objects.equals(sysOut, suffix(hypOut, suffix.size()))) {	2✔
177	ua = u.succ(suffix.firstSymbol());	2✔
178	lower = mid;	2✔
179	stillCe = true;	2✔
180	break;	2✔
181	}
182	}	2✔
183	if (stillCe) {	2✔
184	continue;	2✔
185	}
186	upper = mid;	2✔
187	}	2✔
188
189	if (ua == null) {	2✔
190	assert lower == lsp.word().length()-1;	2✔
191	ua = lsp;	2✔
192	}
193
194	// add witnesses
195	int mid = (upper + lower) / 2;	2✔
196	Word<I> sprime = ce.suffix(ce.length() - (mid + 1));	2✔
197	DTLeaf<I, D> qnext = getState(ua.word());	2✔
198	for (PTNode<I, D> uprime : qnext.getShortPrefixes()) {	2✔
199	witnesses.add(new DefaultQuery<>(uprime.word(), sprime));	2✔
200	}	2✔
201	witnesses.add(new DefaultQuery<>(ua.word(), sprime));	2✔
202
203	ua.makeShortPrefix();	2✔
204	}	2✔
205	}

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