6605620268

Committed 22 Oct 2023 06:53PM UTC coverage: 93.218% (+0.9%) from 92.296%

Build # 6605620268

Build Type

push

github

Committed by

mtf90

Commit Message

cleanup passive integration tests

Run Details

11546 of 12386 relevant lines covered (93.22%)

1.68 hits per line

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

97.34

/algorithms/active/kearns-vazirani/src/main/java/de/learnlib/algorithm/kv/dfa/KearnsVaziraniDFA.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.algorithm.kv.dfa;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Deque;
import java.util.Iterator;
import java.util.List;
import java.util.function.BooleanSupplier;

import com.github.misberner.buildergen.annotations.GenerateBuilder;
import de.learnlib.acex.AcexAnalyzer;
import de.learnlib.acex.analyzer.AcexAnalyzers;
import de.learnlib.acex.impl.AbstractBaseCounterexample;
import de.learnlib.algorithm.kv.StateInfo;
import de.learnlib.api.Resumable;
import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner;
import de.learnlib.api.logging.Category;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import de.learnlib.datastructure.discriminationtree.BinaryDTree;
import de.learnlib.datastructure.discriminationtree.model.AbstractWordBasedDTNode;
import de.learnlib.datastructure.discriminationtree.model.LCAInfo;
import net.automatalib.SupportsGrowingAlphabet;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.impl.Alphabets;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.automaton.fsa.impl.compact.CompactDFA;
import net.automatalib.common.smartcollection.ArrayStorage;
import net.automatalib.word.Word;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * The Kearns/Vazirani algorithm for learning DFA, as described in the book "An Introduction to Computational Learning
 * Theory" by Michael Kearns and Umesh Vazirani.
 *
 * @param <I>
 *         input symbol type
 */
public class KearnsVaziraniDFA<I>
        implements DFALearner<I>, SupportsGrowingAlphabet<I>, Resumable<KearnsVaziraniDFAState<I>> {

    private static final Logger LOGGER = LoggerFactory.getLogger(KearnsVaziraniDFA.class);

    private final Alphabet<I> alphabet;
    private final MembershipOracle<I, Boolean> oracle;
    private final boolean repeatedCounterexampleEvaluation;
    private final AcexAnalyzer ceAnalyzer;
    private BinaryDTree<I, StateInfo<I, Boolean>> discriminationTree;
    protected List<StateInfo<I, Boolean>> stateInfos = new ArrayList<>();
    private CompactDFA<I> hypothesis;

    /**
     * Constructor.
     *
     * @param alphabet
     *         the learning alphabet
     * @param oracle
     *         the membership oracle
     */
    @GenerateBuilder
    public KearnsVaziraniDFA(Alphabet<I> alphabet,
                             MembershipOracle<I, Boolean> oracle,
                             boolean repeatedCounterexampleEvaluation,
                             AcexAnalyzer counterexampleAnalyzer) {
        this.alphabet = alphabet;
        this.hypothesis = new CompactDFA<>(alphabet);
        this.discriminationTree = new BinaryDTree<>(oracle);
        this.oracle = oracle;
        this.repeatedCounterexampleEvaluation = repeatedCounterexampleEvaluation;
        this.ceAnalyzer = counterexampleAnalyzer;
    }

    @Override
    public void startLearning() {
        initialize();
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
        if (hypothesis.size() == 0) {
            throw new IllegalStateException("Not initialized");
        }
        Word<I> input = ceQuery.getInput();
        boolean output = ceQuery.getOutput();
        if (!refineHypothesisSingle(input, output)) {
            return false;
        }
        if (repeatedCounterexampleEvaluation) {
            while (refineHypothesisSingle(input, output)) {}
        }
        return true;
    }

    @Override
    public DFA<?, I> getHypothesisModel() {
        if (hypothesis.size() == 0) {
            throw new IllegalStateException("Not started");
        }
        return hypothesis;
    }

    public BinaryDTree<I, StateInfo<I, Boolean>> getDiscriminationTree() {
        return discriminationTree;
    }

    private boolean refineHypothesisSingle(Word<I> input, boolean output) {
        int inputLen = input.length();

        if (inputLen < 2) {
            return false;
        }

        if (hypothesis.accepts(input) == output) {
            return false;
        }

        KVAbstractCounterexample acex = new KVAbstractCounterexample(input, output, oracle);
        int idx = ceAnalyzer.analyzeAbstractCounterexample(acex, 1);

        Word<I> prefix = input.prefix(idx);
        StateInfo<I, Boolean> srcStateInfo = acex.getStateInfo(idx);
        I sym = input.getSymbol(idx);
        LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> lca = acex.getLCA(idx + 1);
        assert lca != null;

        splitState(srcStateInfo, prefix, sym, lca);

        return true;
    }

    private void splitState(StateInfo<I, Boolean> stateInfo,
                            Word<I> newPrefix,
                            I sym,
                            LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> separatorInfo) {
        int state = stateInfo.id;
        boolean oldAccepting = hypothesis.isAccepting(state);
        // TLongList oldIncoming = stateInfo.fetchIncoming();
        List<Long> oldIncoming = stateInfo.fetchIncoming(); // TODO: replace with primitive specialization

        StateInfo<I, Boolean> newStateInfo = createState(newPrefix, oldAccepting);

        AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> stateLeaf = stateInfo.dtNode;

        AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> separator = separatorInfo.leastCommonAncestor;
        Word<I> newDiscriminator = newDiscriminator(sym, separator.getDiscriminator());

        AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>.SplitResult sr = stateLeaf.split(newDiscriminator,
                                                                                                    separatorInfo.subtree1Label,
                                                                                                    separatorInfo.subtree2Label,
                                                                                                    newStateInfo);

        stateInfo.dtNode = sr.nodeOld;
        newStateInfo.dtNode = sr.nodeNew;

        initState(newStateInfo);

        updateTransitions(oldIncoming, stateLeaf);
    }

    // private void updateTransitions(TLongList transList, DTNode<I, Boolean, StateInfo<I>> oldDtTarget) {
    private void updateTransitions(List<Long> transList,
                                   AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> oldDtTarget) { // TODO: replace with primitive specialization
        int numTrans = transList.size();

        final List<Word<I>> transAs = new ArrayList<>(numTrans);

        for (int i = 0; i < numTrans; i++) {
            long encodedTrans = transList.get(i);

            int sourceState = (int) (encodedTrans >> Integer.SIZE);
            int transIdx = (int) (encodedTrans);

            StateInfo<I, Boolean> sourceInfo = stateInfos.get(sourceState);
            I symbol = alphabet.getSymbol(transIdx);

            transAs.add(sourceInfo.accessSequence.append(symbol));
        }

        final List<StateInfo<I, Boolean>> succs = sift(Collections.nCopies(numTrans, oldDtTarget), transAs);

        for (int i = 0; i < numTrans; i++) {
            long encodedTrans = transList.get(i);

            int sourceState = (int) (encodedTrans >> Integer.SIZE);
            int transIdx = (int) (encodedTrans);

            setTransition(sourceState, transIdx, succs.get(i));
        }
    }

    private Word<I> newDiscriminator(I symbol, Word<I> succDiscriminator) {
        return succDiscriminator.prepend(symbol);
    }

    private void initialize() {
        boolean initAccepting = oracle.answerQuery(Word.epsilon());
        StateInfo<I, Boolean> initStateInfo = createInitialState(initAccepting);

        AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> root = discriminationTree.getRoot();
        root.setData(initStateInfo);
        initStateInfo.dtNode = root.split(Word.epsilon(), initAccepting, !initAccepting).nodeOld;

        initState(initStateInfo);
    }

    private StateInfo<I, Boolean> createInitialState(boolean accepting) {
        int state = hypothesis.addIntInitialState(accepting);
        StateInfo<I, Boolean> si = new StateInfo<>(state, Word.epsilon());
        assert stateInfos.size() == state;
        stateInfos.add(si);

        return si;
    }

    private StateInfo<I, Boolean> createState(Word<I> accessSequence, boolean accepting) {
        int state = hypothesis.addIntState(accepting);
        StateInfo<I, Boolean> si = new StateInfo<>(state, accessSequence);
        assert stateInfos.size() == state;
        stateInfos.add(si);

        return si;
    }

    private void initState(StateInfo<I, Boolean> stateInfo) {
        int alphabetSize = alphabet.size();

        int state = stateInfo.id;
        Word<I> accessSequence = stateInfo.accessSequence;

        final ArrayStorage<Word<I>> transAs = new ArrayStorage<>(alphabetSize);

        for (int i = 0; i < alphabetSize; i++) {
            I sym = alphabet.getSymbol(i);
            transAs.set(i, accessSequence.append(sym));
        }

        final List<StateInfo<I, Boolean>> succs = sift(transAs);

        for (int i = 0; i < alphabetSize; i++) {
            setTransition(state, i, succs.get(i));
        }
    }

    private void setTransition(int state, int symIdx, StateInfo<I, Boolean> succInfo) {
        succInfo.addIncoming(state, symIdx);
        hypothesis.setTransition(state, symIdx, succInfo.id);
    }

    private List<StateInfo<I, Boolean>> sift(List<Word<I>> prefixes) {
        return sift(Collections.nCopies(prefixes.size(), discriminationTree.getRoot()), prefixes);
    }

    private List<StateInfo<I, Boolean>> sift(List<AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> starts,
                                             List<Word<I>> prefixes) {

        final List<AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> leaves =
                discriminationTree.sift(starts, prefixes);
        final ArrayStorage<StateInfo<I, Boolean>> result = new ArrayStorage<>(leaves.size());

        for (int i = 0; i < leaves.size(); i++) {
            final AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> leaf = leaves.get(i);

            StateInfo<I, Boolean> succStateInfo = leaf.getData();
            if (succStateInfo == null) {
                // Special case: this is the *first* state of a different
                // acceptance than the initial state
                boolean initAccepting = hypothesis.isAccepting(hypothesis.getIntInitialState());
                succStateInfo = createState(prefixes.get(i), !initAccepting);
                leaf.setData(succStateInfo);
                succStateInfo.dtNode = leaf;

                initState(succStateInfo);
            }

            result.set(i, succStateInfo);
        }

        return result;
    }

    @Override
    public void addAlphabetSymbol(I symbol) {

        if (!this.alphabet.containsSymbol(symbol)) {
            Alphabets.toGrowingAlphabetOrThrowException(this.alphabet).addSymbol(symbol);
        }

        this.hypothesis.addAlphabetSymbol(symbol);

        // check if we already have information about the symbol (then the transition is defined) so we don't post
        // redundant queries
        if (this.hypothesis.getInitialState() != null &&
            this.hypothesis.getSuccessor(this.hypothesis.getInitialState(), symbol) == null) {
            // use new list to prevent concurrent modification exception
            final List<Word<I>> transAs = new ArrayList<>(this.stateInfos.size());
            for (StateInfo<I, Boolean> si : this.stateInfos) {
                transAs.add(si.accessSequence.append(symbol));
            }

            final List<StateInfo<I, Boolean>> succs = sift(transAs);

            final Iterator<StateInfo<I, Boolean>> stateIter = this.stateInfos.iterator();
            final Iterator<StateInfo<I, Boolean>> leafsIter = succs.iterator();
            final int inputIdx = this.alphabet.getSymbolIndex(symbol);

            while (stateIter.hasNext() && leafsIter.hasNext()) {
                setTransition(stateIter.next().id, inputIdx, leafsIter.next());
            }

            // in case the new symbol added a new state (see sift method) we allow at max one additional state
            assert !stateIter.hasNext() || !((BooleanSupplier) () -> {
                stateIter.next();
                return stateIter.hasNext();
            }).getAsBoolean();
            assert !leafsIter.hasNext();
        }
    }

    @Override
    public KearnsVaziraniDFAState<I> suspend() {
        return new KearnsVaziraniDFAState<>(hypothesis, discriminationTree, stateInfos);
    }

    @Override
    public void resume(KearnsVaziraniDFAState<I> state) {
        this.hypothesis = state.getHypothesis();
        this.discriminationTree = state.getDiscriminationTree();
        this.discriminationTree.setOracle(oracle);
        this.stateInfos = state.getStateInfos();

        final Alphabet<I> oldAlphabet = this.hypothesis.getInputAlphabet();
        if (!oldAlphabet.equals(this.alphabet)) {
            LOGGER.warn(Category.DATASTRUCTURE,
                        "The current alphabet '{}' differs from the resumed alphabet '{}'. Future behavior may be inconsistent",
                        this.alphabet,
                        oldAlphabet);
        }
    }

    public static final class BuilderDefaults {

        private BuilderDefaults() {
            // prevent instantiation
        }

        public static boolean repeatedCounterexampleEvaluation() {
            return true;
        }

        public static AcexAnalyzer counterexampleAnalyzer() {
            return AcexAnalyzers.LINEAR_FWD;
        }
    }

    protected class KVAbstractCounterexample extends AbstractBaseCounterexample<Boolean> {

        private final Word<I> ceWord;
        private final MembershipOracle<I, Boolean> oracle;
        private final StateInfo<I, Boolean>[] states;
        private final LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>>[] lcas;

        @SuppressWarnings("unchecked")
        public KVAbstractCounterexample(Word<I> ceWord, boolean output, MembershipOracle<I, Boolean> oracle) {
            super(ceWord.length() + 1);
            this.ceWord = ceWord;
            this.oracle = oracle;

            int m = ceWord.length();
            this.states = new StateInfo[m + 1];
            this.lcas = new LCAInfo[m + 1];
            int i = 0;

            int currState = hypothesis.getIntInitialState();
            states[i++] = stateInfos.get(currState);
            for (I sym : ceWord) {
                currState = hypothesis.getSuccessor(currState, sym);
                states[i++] = stateInfos.get(currState);
            }

            // Acceptance/Non-acceptance separates hypothesis from target
            lcas[m] = new LCAInfo<>(discriminationTree.getRoot(), !output, output);
        }

        public StateInfo<I, Boolean> getStateInfo(int idx) {
            return states[idx];
        }

        public LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> getLCA(int idx) {
            return lcas[idx];
        }

        @Override
        protected Boolean computeEffect(int index) {
            Word<I> prefix = ceWord.prefix(index);
            StateInfo<I, Boolean> info = states[index];

            // Save the expected outcomes on the path from the leaf representing the state
            // to the root on a stack
            AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> node = info.dtNode;
            Deque<Boolean> expect = new ArrayDeque<>();
            while (!node.isRoot()) {
                Boolean parentOutcome = node.getParentOutcome();
                assert parentOutcome != null;
                expect.push(parentOutcome);
                node = node.getParent();
            }

            AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> currNode = discriminationTree.getRoot();

            while (!expect.isEmpty()) {
                Word<I> suffix = currNode.getDiscriminator();
                boolean out = oracle.answerQuery(prefix, suffix);
                if (out != expect.pop()) {
                    lcas[index] = new LCAInfo<>(currNode, !out, out);
                    return false;
                }
                currNode = currNode.child(out);
            }

            assert currNode.isLeaf() && expect.isEmpty();
            return true;
        }

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

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.algorithm.kv.dfa;
17
18	import java.util.ArrayDeque;
19	import java.util.ArrayList;
20	import java.util.Collections;
21	import java.util.Deque;
22	import java.util.Iterator;
23	import java.util.List;
24	import java.util.function.BooleanSupplier;
25
26	import com.github.misberner.buildergen.annotations.GenerateBuilder;
27	import de.learnlib.acex.AcexAnalyzer;
28	import de.learnlib.acex.analyzer.AcexAnalyzers;
29	import de.learnlib.acex.impl.AbstractBaseCounterexample;
30	import de.learnlib.algorithm.kv.StateInfo;
31	import de.learnlib.api.Resumable;
32	import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner;
33	import de.learnlib.api.logging.Category;
34	import de.learnlib.api.oracle.MembershipOracle;
35	import de.learnlib.api.query.DefaultQuery;
36	import de.learnlib.datastructure.discriminationtree.BinaryDTree;
37	import de.learnlib.datastructure.discriminationtree.model.AbstractWordBasedDTNode;
38	import de.learnlib.datastructure.discriminationtree.model.LCAInfo;
39	import net.automatalib.SupportsGrowingAlphabet;
40	import net.automatalib.alphabet.Alphabet;
41	import net.automatalib.alphabet.impl.Alphabets;
42	import net.automatalib.automaton.fsa.DFA;
43	import net.automatalib.automaton.fsa.impl.compact.CompactDFA;
44	import net.automatalib.common.smartcollection.ArrayStorage;
45	import net.automatalib.word.Word;
46	import org.slf4j.Logger;
47	import org.slf4j.LoggerFactory;
48
49	/**
50	* The Kearns/Vazirani algorithm for learning DFA, as described in the book "An Introduction to Computational Learning
51	* Theory" by Michael Kearns and Umesh Vazirani.
52	*
53	* @param <I>
54	* input symbol type
55	*/
56	public class KearnsVaziraniDFA<I>
57	implements DFALearner<I>, SupportsGrowingAlphabet<I>, Resumable<KearnsVaziraniDFAState<I>> {
58
59	private static final Logger LOGGER = LoggerFactory.getLogger(KearnsVaziraniDFA.class);	2✔
60
61	private final Alphabet<I> alphabet;
62	private final MembershipOracle<I, Boolean> oracle;
63	private final boolean repeatedCounterexampleEvaluation;
64	private final AcexAnalyzer ceAnalyzer;
65	private BinaryDTree<I, StateInfo<I, Boolean>> discriminationTree;
66	protected List<StateInfo<I, Boolean>> stateInfos = new ArrayList<>();	2✔
67	private CompactDFA<I> hypothesis;
68
69	/**
70	* Constructor.
71	*
72	* @param alphabet
73	* the learning alphabet
74	* @param oracle
75	* the membership oracle
76	*/
77	@GenerateBuilder
78	public KearnsVaziraniDFA(Alphabet<I> alphabet,
79	MembershipOracle<I, Boolean> oracle,
80	boolean repeatedCounterexampleEvaluation,
81	AcexAnalyzer counterexampleAnalyzer) {	2✔
82	this.alphabet = alphabet;	2✔
83	this.hypothesis = new CompactDFA<>(alphabet);	2✔
84	this.discriminationTree = new BinaryDTree<>(oracle);	2✔
85	this.oracle = oracle;	2✔
86	this.repeatedCounterexampleEvaluation = repeatedCounterexampleEvaluation;	2✔
87	this.ceAnalyzer = counterexampleAnalyzer;	2✔
88	}	2✔
89
90	@Override
91	public void startLearning() {
92	initialize();	2✔
93	}	2✔
94
95	@Override
96	public boolean refineHypothesis(DefaultQuery<I, Boolean> ceQuery) {
97	if (hypothesis.size() == 0) {	2✔
98	throw new IllegalStateException("Not initialized");	×
99	}
100	Word<I> input = ceQuery.getInput();	2✔
101	boolean output = ceQuery.getOutput();	2✔
102	if (!refineHypothesisSingle(input, output)) {	2✔
103	return false;	2✔
104	}
105	if (repeatedCounterexampleEvaluation) {	2✔
106	while (refineHypothesisSingle(input, output)) {}	2✔
107	}
108	return true;	2✔
109	}
110
111	@Override
112	public DFA<?, I> getHypothesisModel() {
113	if (hypothesis.size() == 0) {	2✔
114	throw new IllegalStateException("Not started");	×
115	}
116	return hypothesis;	2✔
117	}
118
119	public BinaryDTree<I, StateInfo<I, Boolean>> getDiscriminationTree() {
120	return discriminationTree;	×
121	}
122
123	private boolean refineHypothesisSingle(Word<I> input, boolean output) {
124	int inputLen = input.length();	2✔
125
126	if (inputLen < 2) {	2✔
127	return false;	×
128	}
129
130	if (hypothesis.accepts(input) == output) {	2✔
131	return false;	2✔
132	}
133
134	KVAbstractCounterexample acex = new KVAbstractCounterexample(input, output, oracle);	2✔
135	int idx = ceAnalyzer.analyzeAbstractCounterexample(acex, 1);	2✔
136
137	Word<I> prefix = input.prefix(idx);	2✔
138	StateInfo<I, Boolean> srcStateInfo = acex.getStateInfo(idx);	2✔
139	I sym = input.getSymbol(idx);	2✔
140	LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> lca = acex.getLCA(idx + 1);	2✔
141	assert lca != null;	2✔
142
143	splitState(srcStateInfo, prefix, sym, lca);	2✔
144
145	return true;	2✔
146	}
147
148	private void splitState(StateInfo<I, Boolean> stateInfo,
149	Word<I> newPrefix,
150	I sym,
151	LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> separatorInfo) {
152	int state = stateInfo.id;	2✔
153	boolean oldAccepting = hypothesis.isAccepting(state);	2✔
154	// TLongList oldIncoming = stateInfo.fetchIncoming();
155	List<Long> oldIncoming = stateInfo.fetchIncoming(); // TODO: replace with primitive specialization	2✔
156
157	StateInfo<I, Boolean> newStateInfo = createState(newPrefix, oldAccepting);	2✔
158
159	AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> stateLeaf = stateInfo.dtNode;	2✔
160
161	AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> separator = separatorInfo.leastCommonAncestor;	2✔
162	Word<I> newDiscriminator = newDiscriminator(sym, separator.getDiscriminator());	2✔
163
164	AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>.SplitResult sr = stateLeaf.split(newDiscriminator,	2✔
165	separatorInfo.subtree1Label,
166	separatorInfo.subtree2Label,
167	newStateInfo);
168
169	stateInfo.dtNode = sr.nodeOld;	2✔
170	newStateInfo.dtNode = sr.nodeNew;	2✔
171
172	initState(newStateInfo);	2✔
173
174	updateTransitions(oldIncoming, stateLeaf);	2✔
175	}	2✔
176
177	// private void updateTransitions(TLongList transList, DTNode<I, Boolean, StateInfo<I>> oldDtTarget) {
178	private void updateTransitions(List<Long> transList,
179	AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> oldDtTarget) { // TODO: replace with primitive specialization
180	int numTrans = transList.size();	2✔
181
182	final List<Word<I>> transAs = new ArrayList<>(numTrans);	2✔
183
184	for (int i = 0; i < numTrans; i++) {	2✔
185	long encodedTrans = transList.get(i);	2✔
186
187	int sourceState = (int) (encodedTrans >> Integer.SIZE);	2✔
188	int transIdx = (int) (encodedTrans);	2✔
189
190	StateInfo<I, Boolean> sourceInfo = stateInfos.get(sourceState);	2✔
191	I symbol = alphabet.getSymbol(transIdx);	2✔
192
193	transAs.add(sourceInfo.accessSequence.append(symbol));	2✔
194	}
195
196	final List<StateInfo<I, Boolean>> succs = sift(Collections.nCopies(numTrans, oldDtTarget), transAs);	2✔
197
198	for (int i = 0; i < numTrans; i++) {	2✔
199	long encodedTrans = transList.get(i);	2✔
200
201	int sourceState = (int) (encodedTrans >> Integer.SIZE);	2✔
202	int transIdx = (int) (encodedTrans);	2✔
203
204	setTransition(sourceState, transIdx, succs.get(i));	2✔
205	}
206	}	2✔
207
208	private Word<I> newDiscriminator(I symbol, Word<I> succDiscriminator) {
209	return succDiscriminator.prepend(symbol);	2✔
210	}
211
212	private void initialize() {
213	boolean initAccepting = oracle.answerQuery(Word.epsilon());	2✔
214	StateInfo<I, Boolean> initStateInfo = createInitialState(initAccepting);	2✔
215
216	AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> root = discriminationTree.getRoot();	2✔
217	root.setData(initStateInfo);	2✔
218	initStateInfo.dtNode = root.split(Word.epsilon(), initAccepting, !initAccepting).nodeOld;	2✔
219
220	initState(initStateInfo);	2✔
221	}	2✔
222
223	private StateInfo<I, Boolean> createInitialState(boolean accepting) {
224	int state = hypothesis.addIntInitialState(accepting);	2✔
225	StateInfo<I, Boolean> si = new StateInfo<>(state, Word.epsilon());	2✔
226	assert stateInfos.size() == state;	2✔
227	stateInfos.add(si);	2✔
228
229	return si;	2✔
230	}
231
232	private StateInfo<I, Boolean> createState(Word<I> accessSequence, boolean accepting) {
233	int state = hypothesis.addIntState(accepting);	2✔
234	StateInfo<I, Boolean> si = new StateInfo<>(state, accessSequence);	2✔
235	assert stateInfos.size() == state;	2✔
236	stateInfos.add(si);	2✔
237
238	return si;	2✔
239	}
240
241	private void initState(StateInfo<I, Boolean> stateInfo) {
242	int alphabetSize = alphabet.size();	2✔
243
244	int state = stateInfo.id;	2✔
245	Word<I> accessSequence = stateInfo.accessSequence;	2✔
246
247	final ArrayStorage<Word<I>> transAs = new ArrayStorage<>(alphabetSize);	2✔
248
249	for (int i = 0; i < alphabetSize; i++) {	2✔
250	I sym = alphabet.getSymbol(i);	2✔
251	transAs.set(i, accessSequence.append(sym));	2✔
252	}
253
254	final List<StateInfo<I, Boolean>> succs = sift(transAs);	2✔
255
256	for (int i = 0; i < alphabetSize; i++) {	2✔
257	setTransition(state, i, succs.get(i));	2✔
258	}
259	}	2✔
260
261	private void setTransition(int state, int symIdx, StateInfo<I, Boolean> succInfo) {
262	succInfo.addIncoming(state, symIdx);	2✔
263	hypothesis.setTransition(state, symIdx, succInfo.id);	2✔
264	}	2✔
265
266	private List<StateInfo<I, Boolean>> sift(List<Word<I>> prefixes) {
267	return sift(Collections.nCopies(prefixes.size(), discriminationTree.getRoot()), prefixes);	2✔
268	}
269
270	private List<StateInfo<I, Boolean>> sift(List<AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> starts,
271	List<Word<I>> prefixes) {
272
273	final List<AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> leaves =	2✔
274	discriminationTree.sift(starts, prefixes);	2✔
275	final ArrayStorage<StateInfo<I, Boolean>> result = new ArrayStorage<>(leaves.size());	2✔
276
277	for (int i = 0; i < leaves.size(); i++) {	2✔
278	final AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> leaf = leaves.get(i);	2✔
279
280	StateInfo<I, Boolean> succStateInfo = leaf.getData();	2✔
281	if (succStateInfo == null) {	2✔
282	// Special case: this is the first state of a different
283	// acceptance than the initial state
284	boolean initAccepting = hypothesis.isAccepting(hypothesis.getIntInitialState());	2✔
285	succStateInfo = createState(prefixes.get(i), !initAccepting);	2✔
286	leaf.setData(succStateInfo);	2✔
287	succStateInfo.dtNode = leaf;	2✔
288
289	initState(succStateInfo);	2✔
290	}
291
292	result.set(i, succStateInfo);	2✔
293	}
294
295	return result;	2✔
296	}
297
298	@Override
299	public void addAlphabetSymbol(I symbol) {
300
301	if (!this.alphabet.containsSymbol(symbol)) {	2✔
302	Alphabets.toGrowingAlphabetOrThrowException(this.alphabet).addSymbol(symbol);	2✔
303	}
304
305	this.hypothesis.addAlphabetSymbol(symbol);	2✔
306
307	// check if we already have information about the symbol (then the transition is defined) so we don't post
308	// redundant queries
309	if (this.hypothesis.getInitialState() != null &&	2✔
310	this.hypothesis.getSuccessor(this.hypothesis.getInitialState(), symbol) == null) {	2✔
311	// use new list to prevent concurrent modification exception
312	final List<Word<I>> transAs = new ArrayList<>(this.stateInfos.size());	2✔
313	for (StateInfo<I, Boolean> si : this.stateInfos) {	2✔
314	transAs.add(si.accessSequence.append(symbol));	2✔
315	}	2✔
316
317	final List<StateInfo<I, Boolean>> succs = sift(transAs);	2✔
318
319	final Iterator<StateInfo<I, Boolean>> stateIter = this.stateInfos.iterator();	2✔
320	final Iterator<StateInfo<I, Boolean>> leafsIter = succs.iterator();	2✔
321	final int inputIdx = this.alphabet.getSymbolIndex(symbol);	2✔
322
323	while (stateIter.hasNext() && leafsIter.hasNext()) {	2✔
324	setTransition(stateIter.next().id, inputIdx, leafsIter.next());	2✔
325	}
326
327	// in case the new symbol added a new state (see sift method) we allow at max one additional state
328	assert !stateIter.hasNext() \|\| !((BooleanSupplier) () -> {	2✔
329	stateIter.next();	1✔
330	return stateIter.hasNext();	1✔
331	}).getAsBoolean();	1✔
332	assert !leafsIter.hasNext();	2✔
333	}
334	}	2✔
335
336	@Override
337	public KearnsVaziraniDFAState<I> suspend() {
338	return new KearnsVaziraniDFAState<>(hypothesis, discriminationTree, stateInfos);	2✔
339	}
340
341	@Override
342	public void resume(KearnsVaziraniDFAState<I> state) {
343	this.hypothesis = state.getHypothesis();	2✔
344	this.discriminationTree = state.getDiscriminationTree();	2✔
345	this.discriminationTree.setOracle(oracle);	2✔
346	this.stateInfos = state.getStateInfos();	2✔
347
348	final Alphabet<I> oldAlphabet = this.hypothesis.getInputAlphabet();	2✔
349	if (!oldAlphabet.equals(this.alphabet)) {	2✔
350	LOGGER.warn(Category.DATASTRUCTURE,	×
351	"The current alphabet '{}' differs from the resumed alphabet '{}'. Future behavior may be inconsistent",
352	this.alphabet,
353	oldAlphabet);
354	}
355	}	2✔
356
357	public static final class BuilderDefaults {
358
359	private BuilderDefaults() {
360	// prevent instantiation
361	}
362
363	public static boolean repeatedCounterexampleEvaluation() {
364	return true;	2✔
365	}
366
367	public static AcexAnalyzer counterexampleAnalyzer() {
368	return AcexAnalyzers.LINEAR_FWD;	2✔
369	}
370	}
371
372	protected class KVAbstractCounterexample extends AbstractBaseCounterexample<Boolean> {	2✔
373
374	private final Word<I> ceWord;
375	private final MembershipOracle<I, Boolean> oracle;
376	private final StateInfo<I, Boolean>[] states;
377	private final LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>>[] lcas;
378
379	@SuppressWarnings("unchecked")
380	public KVAbstractCounterexample(Word<I> ceWord, boolean output, MembershipOracle<I, Boolean> oracle) {	2✔
381	super(ceWord.length() + 1);	2✔
382	this.ceWord = ceWord;	2✔
383	this.oracle = oracle;	2✔
384
385	int m = ceWord.length();	2✔
386	this.states = new StateInfo[m + 1];	2✔
387	this.lcas = new LCAInfo[m + 1];	2✔
388	int i = 0;	2✔
389
390	int currState = hypothesis.getIntInitialState();	2✔
391	states[i++] = stateInfos.get(currState);	2✔
392	for (I sym : ceWord) {	2✔
393	currState = hypothesis.getSuccessor(currState, sym);	2✔
394	states[i++] = stateInfos.get(currState);	2✔
395	}	2✔
396
397	// Acceptance/Non-acceptance separates hypothesis from target
398	lcas[m] = new LCAInfo<>(discriminationTree.getRoot(), !output, output);	2✔
399	}	2✔
400
401	public StateInfo<I, Boolean> getStateInfo(int idx) {
402	return states[idx];	2✔
403	}
404
405	public LCAInfo<Boolean, AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>>> getLCA(int idx) {
406	return lcas[idx];	2✔
407	}
408
409	@Override
410	protected Boolean computeEffect(int index) {
411	Word<I> prefix = ceWord.prefix(index);	2✔
412	StateInfo<I, Boolean> info = states[index];	2✔
413
414	// Save the expected outcomes on the path from the leaf representing the state
415	// to the root on a stack
416	AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> node = info.dtNode;	2✔
417	Deque<Boolean> expect = new ArrayDeque<>();	2✔
418	while (!node.isRoot()) {	2✔
419	Boolean parentOutcome = node.getParentOutcome();	2✔
420	assert parentOutcome != null;	2✔
421	expect.push(parentOutcome);	2✔
422	node = node.getParent();	2✔
423	}	2✔
424
425	AbstractWordBasedDTNode<I, Boolean, StateInfo<I, Boolean>> currNode = discriminationTree.getRoot();	2✔
426
427	while (!expect.isEmpty()) {	2✔
428	Word<I> suffix = currNode.getDiscriminator();	2✔
429	boolean out = oracle.answerQuery(prefix, suffix);	2✔
430	if (out != expect.pop()) {	2✔
431	lcas[index] = new LCAInfo<>(currNode, !out, out);	2✔
432	return false;	2✔
433	}
434	currNode = currNode.child(out);	2✔
435	}	2✔
436
437	assert currNode.isLeaf() && expect.isEmpty();	2✔
438	return true;	2✔
439	}
440
441	@Override
442	public boolean checkEffects(Boolean eff1, Boolean eff2) {
443	return !eff1 \|\| eff2;	2✔
444	}
445	}
446	}

LearnLib / learnlib / 6605620268

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