13166566074

Committed 05 Feb 2025 09:05PM UTC coverage: 94.368% (+0.04%) from 94.324%

Build # 13166566074

Build Type

push

github

Committed by

mtf90

Commit Message

test api conformance

when provided with a non-counterexample, refineHypothesis should return false and not throw an exception.

Run Details

12 of 12 new or added lines in 4 files covered. (100.0%)

19 existing lines in 4 files now uncovered.

12484 of 13229 relevant lines covered (94.37%)

1.72 hits per line

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

89.47

/algorithms/active/nlstar/src/main/java/de/learnlib/algorithm/nlstar/NLStarLearner.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of LearnLib <https://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.algorithm.nlstar;

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

import de.learnlib.algorithm.LearningAlgorithm.NFALearner;
import de.learnlib.oracle.MembershipOracle;
import de.learnlib.query.DefaultQuery;
import de.learnlib.tooling.annotation.builder.GenerateBuilder;
import de.learnlib.util.MQUtil;
import de.learnlib.util.nfa.NFALearnerWrapper;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.fsa.NFA;
import net.automatalib.automaton.fsa.impl.CompactNFA;
import net.automatalib.word.Word;

/**
 * The NL* learner.
 *
 * @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
     */
    public DFALearner<I> asDFALearner() {
        return new NFALearnerWrapper<>(this.alphabet, this);
    }

    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 NFA<?, I> getHypothesisModel() {
        if (hypothesis == null) {
            throw new IllegalStateException();
        }
        return hypothesis;
    }

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

}

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.algorithm.nlstar;
17
18	import java.util.ArrayList;
19	import java.util.Arrays;
20	import java.util.List;
21
22	import de.learnlib.algorithm.LearningAlgorithm.NFALearner;
23	import de.learnlib.oracle.MembershipOracle;
24	import de.learnlib.query.DefaultQuery;
25	import de.learnlib.tooling.annotation.builder.GenerateBuilder;
26	import de.learnlib.util.MQUtil;
27	import de.learnlib.util.nfa.NFALearnerWrapper;
28	import net.automatalib.alphabet.Alphabet;
29	import net.automatalib.automaton.fsa.NFA;
30	import net.automatalib.automaton.fsa.impl.CompactNFA;
31	import net.automatalib.word.Word;
32
33	/**
34	* The NL* learner.
35	*
36	* @param <I>
37	* input symbol type
38	*/
39	public class NLStarLearner<I> implements NFALearner<I> {
40
41	private final Alphabet<I> alphabet;
42	private final ObservationTable<I> table;
43
44	private CompactNFA<I> hypothesis;
45
46	/**
47	* Constructor.
48	*
49	* @param alphabet
50	* the input alphabet
51	* @param oracle
52	* the membership oracle
53	*/
54	@GenerateBuilder
55	public NLStarLearner(Alphabet<I> alphabet, MembershipOracle<I, Boolean> oracle) {	2✔
56	this.alphabet = alphabet;	2✔
57	this.table = new ObservationTable<>(alphabet, oracle);	2✔
58	}	2✔
59
60	@Override
61	public void startLearning() {
62	if (hypothesis != null) {	2✔
UNCOV 63	throw new IllegalStateException();	×
64	}
65
66	List<List<Row<I>>> unclosed = table.initialize();	2✔
67	completeConsistentTable(unclosed);	2✔
68
69	constructHypothesis();	2✔
70	}	2✔
71
72	/**
73	* Retrieves a view of this learner as a DFA learner. The DFA is obtained by determinizing and minimizing the NFA
74	* hypothesis.
75	*
76	* @return a DFA learner view of this learner
77	*/
78	public DFALearner<I> asDFALearner() {
79	return new NFALearnerWrapper<>(this.alphabet, this);	2✔
80	}
81
82	private void completeConsistentTable(List<List<Row<I>>> initialUnclosed) {
83	List<List<Row<I>>> unclosed = initialUnclosed;	2✔
84
85	Inconsistency<I> incons;
86
87	do {
88	while (!unclosed.isEmpty()) {	2✔
89	unclosed = fixUnclosed(unclosed);	2✔
90	}
91
92	incons = table.findInconsistency();	2✔
93	if (incons != null) {	2✔
94	unclosed = fixInconsistency(incons);	2✔
95	}
96	} while (!unclosed.isEmpty() \|\| incons != null);	2✔
97	}	2✔
98
99	private List<List<Row<I>>> fixUnclosed(List<List<Row<I>>> unclosed) {
100	List<Row<I>> newShort = new ArrayList<>(unclosed.size());	2✔
101
102	for (List<Row<I>> unclosedClass : unclosed) {	2✔
103	newShort.add(unclosedClass.get(0));	2✔
104	}	2✔
105
106	return table.makeUpper(newShort);	2✔
107	}
108
109	private List<List<Row<I>>> fixInconsistency(Inconsistency<I> incons) {
110	I sym = alphabet.getSymbol(incons.getSymbolIdx());	2✔
111	Word<I> oldSuffix = table.getSuffix(incons.getSuffixIdx());	2✔
112
113	Word<I> newSuffix = oldSuffix.prepend(sym);	2✔
114
115	return table.addSuffix(newSuffix);	2✔
116	}
117
118	@Override
119	public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
120	if (hypothesis == null) {	2✔
UNCOV 121	throw new IllegalStateException();	×
122	}
123
124	boolean refined = false;	2✔
125	while (MQUtil.isCounterexample(ceQuery, hypothesis)) {	2✔
126	Word<I> ceWord = ceQuery.getInput();	2✔
127
128	List<List<Row<I>>> unclosed = table.addSuffixes(ceWord.suffixes(false));	2✔
129	completeConsistentTable(unclosed);	2✔
130	constructHypothesis();	2✔
131
132	refined = true;	2✔
133	}	2✔
134	return refined;	2✔
135	}
136
137	private void constructHypothesis() {
138	hypothesis = new CompactNFA<>(alphabet);	2✔
139
140	int[] stateMap = new int[table.getNumUpperRows()];	2✔
141	Arrays.fill(stateMap, -1);	2✔
142
143	List<Row<I>> upperPrimes = table.getUpperPrimes();	2✔
144
145	for (Row<I> row : upperPrimes) {	2✔
146	int state = hypothesis.addIntState(row.getContent(0));	2✔
147	stateMap[row.getUpperId()] = state;	2✔
148	}	2✔
149
150	Row<I> firstRow = table.getUpperRow(0);	2✔
151
152	if (firstRow.isPrime()) {	2✔
153	int state = stateMap[firstRow.getUpperId()];	2✔
154	hypothesis.setInitial(state, true);	2✔
155	} else {	2✔
156	for (Row<I> row : table.getCoveredRows(firstRow)) {	2✔
157	if (row.isPrime()) {	×
158	int state = stateMap[row.getUpperId()];	×
UNCOV 159	hypothesis.setInitial(state, true);	×
160	}
UNCOV 161	}	×
162	}
163
164	// Transition relation
165	for (Row<I> row : upperPrimes) {	2✔
166	int state = stateMap[row.getUpperId()];	2✔
167
168	for (int i = 0; i < alphabet.size(); i++) {	2✔
169	Row<I> succRow = row.getSuccessorRow(i);	2✔
170
171	if (succRow.isPrime()) {	2✔
172	int succState = stateMap[succRow.getUpperId()];	2✔
173	hypothesis.addTransition(state, i, succState);	2✔
174	} else {	2✔
175	for (Row<I> r : succRow.getCoveredRows()) {	2✔
176	if (r.isPrime()) {	2✔
177	int succState = stateMap[r.getUpperId()];	2✔
178	hypothesis.addTransition(state, i, succState);	2✔
179	}
180	}	2✔
181	}
182	}
183	}	2✔
184	}	2✔
185
186	@Override
187	public NFA<?, I> getHypothesisModel() {
188	if (hypothesis == null) {	2✔
UNCOV 189	throw new IllegalStateException();	×
190	}
191	return hypothesis;	2✔
192	}
193
194	public ObservationTable<I> getObservationTable() {
UNCOV 195	return table;	×
196	}
197
198	}

LearnLib / learnlib / 13166566074

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