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

89.29

/algorithms/active/nlstar/src/main/java/de/learnlib/algorithms/nlstar/NLStarLearner.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.nlstar;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;

import com.github.misberner.buildergen.annotations.GenerateBuilder;
import de.learnlib.api.algorithm.NFALearner;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import de.learnlib.util.MQUtil;
import net.automatalib.automata.fsa.impl.compact.CompactDFA;
import net.automatalib.automata.fsa.impl.compact.CompactNFA;
import net.automatalib.util.automata.fsa.NFAs;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;

/**
 * The NL* algorithm, as described in the paper <a href="http://ijcai.org/papers09/Papers/IJCAI09-170.pdf">"Angluin-Style
 * Learning of NFA"</a> by B. Bollig et al. (IJCAI'09).
 *
 * @param <I>
 *         input symbol type
 */
public class NLStarLearner<I> implements NFALearner<I> {

    private final Alphabet<I> alphabet;
    private final ObservationTable<I> table;

    private CompactNFA<I> hypothesis;

    /**
     * Constructor.
     *
     * @param alphabet
     *         the input alphabet
     * @param oracle
     *         the membership oracle
     */
    @GenerateBuilder
    public NLStarLearner(Alphabet<I> alphabet, MembershipOracle<I, Boolean> oracle) {
        this.alphabet = alphabet;
        this.table = new ObservationTable<>(alphabet, oracle);
    }

    @Override
    public void startLearning() {
        if (hypothesis != null) {
            throw new IllegalStateException();
        }

        List<List<Row<I>>> unclosed = table.initialize();
        completeConsistentTable(unclosed);

        constructHypothesis();
    }

    /**
     * Retrieves a view of this learner as a DFA learner. The DFA is obtained by determinizing and minimizing the NFA
     * hypothesis.
     *
     * @return a DFA learner view of this learner
     *
     * @see #getDeterminizedHypothesis()
     */
    public DFALearner<I> asDFALearner() {
        return new DFALearner<I>() {

            @Override
            public String toString() {
                return NLStarLearner.this.toString();
            }

            @Override
            public void startLearning() {
                NLStarLearner.this.startLearning();
            }

            @Override
            public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
                return NLStarLearner.this.refineHypothesis(ceQuery);
            }

            @Override
            public CompactDFA<I> getHypothesisModel() {
                return NLStarLearner.this.getDeterminizedHypothesis();
            }

        };
    }

    /**
     * Retrieves a deterministic version of the hypothesis. The DFA is obtained through {@link
     * NFAs#determinize(net.automatalib.automata.fsa.NFA)}.
     *
     * @return a deterministic version of the hypothesis
     */
    public CompactDFA<I> getDeterminizedHypothesis() {
        if (hypothesis == null) {
            throw new IllegalStateException();
        }
        return NFAs.determinize(hypothesis);
    }

    private void completeConsistentTable(List<List<Row<I>>> initialUnclosed) {
        List<List<Row<I>>> unclosed = initialUnclosed;

        Inconsistency<I> incons;

        do {
            while (!unclosed.isEmpty()) {
                unclosed = fixUnclosed(unclosed);
            }

            incons = table.findInconsistency();
            if (incons != null) {
                unclosed = fixInconsistency(incons);
            }
        } while (!unclosed.isEmpty() || incons != null);
    }

    private List<List<Row<I>>> fixUnclosed(List<List<Row<I>>> unclosed) {
        List<Row<I>> newShort = new ArrayList<>(unclosed.size());

        for (List<Row<I>> unclosedClass : unclosed) {
            newShort.add(unclosedClass.get(0));
        }

        return table.makeUpper(newShort);
    }

    private List<List<Row<I>>> fixInconsistency(Inconsistency<I> incons) {
        I sym = alphabet.getSymbol(incons.getSymbolIdx());
        Word<I> oldSuffix = table.getSuffix(incons.getSuffixIdx());

        Word<I> newSuffix = oldSuffix.prepend(sym);

        return table.addSuffix(newSuffix);
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
        if (hypothesis == null) {
            throw new IllegalStateException();
        }

        boolean refined = false;
        while (MQUtil.isCounterexample(ceQuery, hypothesis)) {
            Word<I> ceWord = ceQuery.getInput();

            List<List<Row<I>>> unclosed = table.addSuffixes(ceWord.suffixes(false));
            completeConsistentTable(unclosed);
            constructHypothesis();

            refined = true;
        }
        return refined;
    }

    private void constructHypothesis() {
        hypothesis = new CompactNFA<>(alphabet);

        int[] stateMap = new int[table.getNumUpperRows()];
        Arrays.fill(stateMap, -1);

        List<Row<I>> upperPrimes = table.getUpperPrimes();

        for (Row<I> row : upperPrimes) {
            int state = hypothesis.addIntState(row.getContent(0));
            stateMap[row.getUpperId()] = state;
        }

        Row<I> firstRow = table.getUpperRow(0);

        if (firstRow.isPrime()) {
            int state = stateMap[firstRow.getUpperId()];
            hypothesis.setInitial(state, true);
        } else {
            for (Row<I> row : table.getCoveredRows(firstRow)) {
                if (row.isPrime()) {
                    int state = stateMap[row.getUpperId()];
                    hypothesis.setInitial(state, true);
                }
            }
        }

        // Transition relation
        for (Row<I> row : upperPrimes) {
            int state = stateMap[row.getUpperId()];

            for (int i = 0; i < alphabet.size(); i++) {
                Row<I> succRow = row.getSuccessorRow(i);

                if (succRow.isPrime()) {
                    int succState = stateMap[succRow.getUpperId()];
                    hypothesis.addTransition(state, i, succState);
                } else {
                    for (Row<I> r : succRow.getCoveredRows()) {
                        if (r.isPrime()) {
                            int succState = stateMap[r.getUpperId()];
                            hypothesis.addTransition(state, i, succState);
                        }
                    }
                }
            }
        }
    }

    @Override
    public CompactNFA<I> getHypothesisModel() {
        if (hypothesis == null) {
            throw new IllegalStateException();
        }
        return hypothesis;
    }

    public ObservationTable<I> getObservationTable() {
        return table;
    }

}

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.nlstar;
17
18	import java.util.ArrayList;
19	import java.util.Arrays;
20	import java.util.List;
21
22	import com.github.misberner.buildergen.annotations.GenerateBuilder;
23	import de.learnlib.api.algorithm.NFALearner;
24	import de.learnlib.api.oracle.MembershipOracle;
25	import de.learnlib.api.query.DefaultQuery;
26	import de.learnlib.util.MQUtil;
27	import net.automatalib.automata.fsa.impl.compact.CompactDFA;
28	import net.automatalib.automata.fsa.impl.compact.CompactNFA;
29	import net.automatalib.util.automata.fsa.NFAs;
30	import net.automatalib.words.Alphabet;
31	import net.automatalib.words.Word;
32
33	/**
34	* The NL* algorithm, as described in the paper <a href="http://ijcai.org/papers09/Papers/IJCAI09-170.pdf">"Angluin-Style
35	* Learning of NFA"</a> by B. Bollig et al. (IJCAI'09).
36	*
37	* @param <I>
38	* input symbol type
39	*/
40	public class NLStarLearner<I> implements NFALearner<I> {
41
42	private final Alphabet<I> alphabet;
43	private final ObservationTable<I> table;
44
45	private CompactNFA<I> hypothesis;
46
47	/**
48	* Constructor.
49	*
50	* @param alphabet
51	* the input alphabet
52	* @param oracle
53	* the membership oracle
54	*/
55	@GenerateBuilder
56	public NLStarLearner(Alphabet<I> alphabet, MembershipOracle<I, Boolean> oracle) {	2✔
57	this.alphabet = alphabet;	2✔
58	this.table = new ObservationTable<>(alphabet, oracle);	2✔
59	}	2✔
60
61	@Override
62	public void startLearning() {
63	if (hypothesis != null) {	2✔
64	throw new IllegalStateException();	×
65	}
66
67	List<List<Row<I>>> unclosed = table.initialize();	2✔
68	completeConsistentTable(unclosed);	2✔
69
70	constructHypothesis();	2✔
71	}	2✔
72
73	/**
74	* Retrieves a view of this learner as a DFA learner. The DFA is obtained by determinizing and minimizing the NFA
75	* hypothesis.
76	*
77	* @return a DFA learner view of this learner
78	*
79	* @see #getDeterminizedHypothesis()
80	*/
81	public DFALearner<I> asDFALearner() {
82	return new DFALearner<I>() {	2✔
83
84	@Override
85	public String toString() {
86	return NLStarLearner.this.toString();	2✔
87	}
88
89	@Override
90	public void startLearning() {
91	NLStarLearner.this.startLearning();	2✔
92	}	2✔
93
94	@Override
95	public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
96	return NLStarLearner.this.refineHypothesis(ceQuery);	2✔
97	}
98
99	@Override
100	public CompactDFA<I> getHypothesisModel() {
101	return NLStarLearner.this.getDeterminizedHypothesis();	2✔
102	}
103
104	};
105	}
106
107	/**
108	* Retrieves a deterministic version of the hypothesis. The DFA is obtained through {@link
109	* NFAs#determinize(net.automatalib.automata.fsa.NFA)}.
110	*
111	* @return a deterministic version of the hypothesis
112	*/
113	public CompactDFA<I> getDeterminizedHypothesis() {
114	if (hypothesis == null) {	2✔
115	throw new IllegalStateException();	×
116	}
117	return NFAs.determinize(hypothesis);	2✔
118	}
119
120	private void completeConsistentTable(List<List<Row<I>>> initialUnclosed) {
121	List<List<Row<I>>> unclosed = initialUnclosed;	2✔
122
123	Inconsistency<I> incons;
124
125	do {
126	while (!unclosed.isEmpty()) {	2✔
127	unclosed = fixUnclosed(unclosed);	2✔
128	}
129
130	incons = table.findInconsistency();	2✔
131	if (incons != null) {	2✔
132	unclosed = fixInconsistency(incons);	2✔
133	}
134	} while (!unclosed.isEmpty() \|\| incons != null);	2✔
135	}	2✔
136
137	private List<List<Row<I>>> fixUnclosed(List<List<Row<I>>> unclosed) {
138	List<Row<I>> newShort = new ArrayList<>(unclosed.size());	2✔
139
140	for (List<Row<I>> unclosedClass : unclosed) {	2✔
141	newShort.add(unclosedClass.get(0));	2✔
142	}	2✔
143
144	return table.makeUpper(newShort);	2✔
145	}
146
147	private List<List<Row<I>>> fixInconsistency(Inconsistency<I> incons) {
148	I sym = alphabet.getSymbol(incons.getSymbolIdx());	2✔
149	Word<I> oldSuffix = table.getSuffix(incons.getSuffixIdx());	2✔
150
151	Word<I> newSuffix = oldSuffix.prepend(sym);	2✔
152
153	return table.addSuffix(newSuffix);	2✔
154	}
155
156	@Override
157	public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
158	if (hypothesis == null) {	2✔
159	throw new IllegalStateException();	×
160	}
161
162	boolean refined = false;	2✔
163	while (MQUtil.isCounterexample(ceQuery, hypothesis)) {	2✔
164	Word<I> ceWord = ceQuery.getInput();	2✔
165
166	List<List<Row<I>>> unclosed = table.addSuffixes(ceWord.suffixes(false));	2✔
167	completeConsistentTable(unclosed);	2✔
168	constructHypothesis();	2✔
169
170	refined = true;	2✔
171	}	2✔
172	return refined;	2✔
173	}
174
175	private void constructHypothesis() {
176	hypothesis = new CompactNFA<>(alphabet);	2✔
177
178	int[] stateMap = new int[table.getNumUpperRows()];	2✔
179	Arrays.fill(stateMap, -1);	2✔
180
181	List<Row<I>> upperPrimes = table.getUpperPrimes();	2✔
182
183	for (Row<I> row : upperPrimes) {	2✔
184	int state = hypothesis.addIntState(row.getContent(0));	2✔
185	stateMap[row.getUpperId()] = state;	2✔
186	}	2✔
187
188	Row<I> firstRow = table.getUpperRow(0);	2✔
189
190	if (firstRow.isPrime()) {	2✔
191	int state = stateMap[firstRow.getUpperId()];	2✔
192	hypothesis.setInitial(state, true);	2✔
193	} else {	2✔
194	for (Row<I> row : table.getCoveredRows(firstRow)) {	2✔
195	if (row.isPrime()) {	×
196	int state = stateMap[row.getUpperId()];	×
197	hypothesis.setInitial(state, true);	×
198	}
199	}	×
200	}
201
202	// Transition relation
203	for (Row<I> row : upperPrimes) {	2✔
204	int state = stateMap[row.getUpperId()];	2✔
205
206	for (int i = 0; i < alphabet.size(); i++) {	2✔
207	Row<I> succRow = row.getSuccessorRow(i);	2✔
208
209	if (succRow.isPrime()) {	2✔
210	int succState = stateMap[succRow.getUpperId()];	2✔
211	hypothesis.addTransition(state, i, succState);	2✔
212	} else {	2✔
213	for (Row<I> r : succRow.getCoveredRows()) {	2✔
214	if (r.isPrime()) {	2✔
215	int succState = stateMap[r.getUpperId()];	2✔
216	hypothesis.addTransition(state, i, succState);	2✔
217	}
218	}	2✔
219	}
220	}
221	}	2✔
222	}	2✔
223
224	@Override
225	public CompactNFA<I> getHypothesisModel() {
226	if (hypothesis == null) {	2✔
227	throw new IllegalStateException();	×
228	}
229	return hypothesis;	2✔
230	}
231
232	public ObservationTable<I> getObservationTable() {
233	return table;	×
234	}
235
236	}

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