19556545386

Committed 21 Nov 2025 01:10AM UTC coverage: 94.471%. First build

Build # 19556545386

Build Type

Pull #155

github

Committed by

web-flow

Commit Message

Merge d1e6e0721 into 7c236fec9

Pull Request Pull Request #155: Bump Java Version to 17/25

Run Details

59 of 83 new or added lines in 25 files covered. (71.08%)

12611 of 13349 relevant lines covered (94.47%)

1.73 hits per line

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

95.65

/examples/src/main/java/de/learnlib/example/aaar/AlternatingBitExampleExplicit.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.example.aaar;

import java.io.IOException;
import java.io.StringWriter;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.List;
import java.util.Map;
import java.util.function.Function;

import de.learnlib.algorithm.LearnerConstructor;
import de.learnlib.algorithm.aaar.ExplicitInitialAbstraction;
import de.learnlib.algorithm.aaar.abstraction.ExplicitAbstractionTree;
import de.learnlib.algorithm.aaar.explicit.ExplicitAAARLearnerMealy;
import de.learnlib.algorithm.lstar.mealy.ExtensibleLStarMealy;
import de.learnlib.algorithm.lstar.mealy.ExtensibleLStarMealyBuilder;
import de.learnlib.datastructure.observationtable.OTLearner.OTLearnerMealy;
import de.learnlib.datastructure.observationtable.writer.ObservationTableASCIIWriter;
import de.learnlib.example.aaar.Event.Msg;
import de.learnlib.example.aaar.Event.Recv;
import de.learnlib.query.DefaultQuery;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.common.util.Pair;
import net.automatalib.graph.Graph;
import net.automatalib.serialization.dot.GraphDOT;
import net.automatalib.visualization.dot.DOT;
import net.automatalib.word.Word;

/**
 * Example from the paper "Automata Learning with Automated Alphabet Abstraction Refinement" by Howar et al., which uses
 * the explicit version of the AAAR learner.
 */
@SuppressWarnings("PMD.SystemPrintln")
public final class AlternatingBitExampleExplicit {

    private static final int ID1 = 72;
    private static final int ID2 = 73;

    private AlternatingBitExampleExplicit() {
        // prevent instantiation
    }

    public static void main(String[] args) throws IOException, InterruptedException {

        final Protocol mqo = new Protocol();

        final LearnerConstructor<ExtensibleLStarMealy<Event, String>, Event, Word<String>> lstar =
                (alph, mq) -> new ExtensibleLStarMealyBuilder<Event, String>().withAlphabet(alph)
                                                                              .withOracle(mq)
                                                                              .create();

        final ExplicitAAARLearnerMealy<ExtensibleLStarMealy<Event, String>, String, Event, String> learner =
                new ExplicitAAARLearnerMealy<>(lstar, mqo, new InitialAbstraction(), new Incrementor());

        learner.startLearning();
        printInfo(learner);

        // Since we directly start with the two concrete symbols, this counterexample does not refine the hypothesis
        learner.refineHypothesis(new DefaultQuery<>(Word.epsilon(),
                                                    Word.fromSymbols(new Msg<>(0, "d"), new Recv()),
                                                    Word.fromSymbols("ind", "ack(0)")));
        printInfo(learner);

        learner.refineHypothesis(new DefaultQuery<>(Word.epsilon(),
                                                    Word.fromSymbols(new Msg<>(ID1, "d'"),
                                                                     new Recv(),
                                                                     new Msg<>(ID2, "d''")),
                                                    Word.fromSymbols("ind", "ack(0)", "ind")));
        printInfo(learner);
    }

    private static <AI, CI, O> void printInfo(ExplicitAAARLearnerMealy<? extends OTLearnerMealy<CI, O>, AI, CI, O> learner)
            throws IOException, InterruptedException {

        System.out.println("-------------------------------------------------------");
        new ObservationTableASCIIWriter<>().write(learner.getLearner().getObservationTable(), System.out);

        if (DOT.checkUsable()) {
            final MealyMachine<?, AI, ?, O> hyp = learner.getHypothesisModel();
            final Map<AI, ExplicitAbstractionTree<AI, CI, Word<O>>> trees = learner.getAbstractionTrees();
            final List<Graph<?, ?>> treesAsGraphs = new ArrayList<>(trees.size());

            for (ExplicitAbstractionTree<AI, CI, Word<O>> t : trees.values()) {
                treesAsGraphs.add(t.graphView());
            }

            try (StringWriter hypWriter = new StringWriter();
                 StringWriter treeWriter = new StringWriter()) {

                GraphDOT.write(hyp.transitionGraphView(learner.getAbstractAlphabet()), hypWriter);
                GraphDOT.write(treesAsGraphs, treeWriter);

                DOT.renderDOTStrings(Arrays.asList(Pair.of("Hypothesis", hypWriter.toString()),
                                                   Pair.of("Abstraction Trees", treeWriter.toString())), true);
            }
        }
    }

    static final class InitialAbstraction implements ExplicitInitialAbstraction<String, Event> {

        @Override
        public String getAbstractSymbol(Event c) {
            if (c instanceof Recv) {
                return "recv";
            } else if (c instanceof Msg) {
                return "msg";
            } else {
                throw new IllegalArgumentException("Unknown event: " + c);
            }
        }

        @Override
        public Event getRepresentative(String a) {
            return switch (a) {
                case "recv" -> new Recv();
                case "msg" -> new Msg<>(0, "d");
                default -> throw new IllegalArgumentException("Unknown abstract: " + a);
            };
        }

        @Override
        public Collection<String> getInitialAbstracts() {
            return Arrays.asList("recv", "msg");
        }
    }

    static final class Incrementor implements Function<String, String> {

        private int cnt;

        @Override
        public String apply(String s) {
            return s + cnt++;
        }
    }
}

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.example.aaar;
17
18	import java.io.IOException;
19	import java.io.StringWriter;
20	import java.util.ArrayList;
21	import java.util.Arrays;
22	import java.util.Collection;
23	import java.util.List;
24	import java.util.Map;
25	import java.util.function.Function;
26
27	import de.learnlib.algorithm.LearnerConstructor;
28	import de.learnlib.algorithm.aaar.ExplicitInitialAbstraction;
29	import de.learnlib.algorithm.aaar.abstraction.ExplicitAbstractionTree;
30	import de.learnlib.algorithm.aaar.explicit.ExplicitAAARLearnerMealy;
31	import de.learnlib.algorithm.lstar.mealy.ExtensibleLStarMealy;
32	import de.learnlib.algorithm.lstar.mealy.ExtensibleLStarMealyBuilder;
33	import de.learnlib.datastructure.observationtable.OTLearner.OTLearnerMealy;
34	import de.learnlib.datastructure.observationtable.writer.ObservationTableASCIIWriter;
35	import de.learnlib.example.aaar.Event.Msg;
36	import de.learnlib.example.aaar.Event.Recv;
37	import de.learnlib.query.DefaultQuery;
38	import net.automatalib.automaton.transducer.MealyMachine;
39	import net.automatalib.common.util.Pair;
40	import net.automatalib.graph.Graph;
41	import net.automatalib.serialization.dot.GraphDOT;
42	import net.automatalib.visualization.dot.DOT;
43	import net.automatalib.word.Word;
44
45	/**
46	* Example from the paper "Automata Learning with Automated Alphabet Abstraction Refinement" by Howar et al., which uses
47	* the explicit version of the AAAR learner.
48	*/
49	@SuppressWarnings("PMD.SystemPrintln")
50	public final class AlternatingBitExampleExplicit {
51
52	private static final int ID1 = 72;
53	private static final int ID2 = 73;
54
55	private AlternatingBitExampleExplicit() {
56	// prevent instantiation
57	}
58
59	public static void main(String[] args) throws IOException, InterruptedException {
60
61	final Protocol mqo = new Protocol();	1✔
62
63	final LearnerConstructor<ExtensibleLStarMealy<Event, String>, Event, Word<String>> lstar =	1✔
64	(alph, mq) -> new ExtensibleLStarMealyBuilder<Event, String>().withAlphabet(alph)	1✔
65	.withOracle(mq)	1✔
66	.create();	1✔
67
68	final ExplicitAAARLearnerMealy<ExtensibleLStarMealy<Event, String>, String, Event, String> learner =	1✔
69	new ExplicitAAARLearnerMealy<>(lstar, mqo, new InitialAbstraction(), new Incrementor());
70
71	learner.startLearning();	1✔
72	printInfo(learner);	1✔
73
74	// Since we directly start with the two concrete symbols, this counterexample does not refine the hypothesis
75	learner.refineHypothesis(new DefaultQuery<>(Word.epsilon(),	1✔
76	Word.fromSymbols(new Msg<>(0, "d"), new Recv()),	1✔
77	Word.fromSymbols("ind", "ack(0)")));	1✔
78	printInfo(learner);	1✔
79
80	learner.refineHypothesis(new DefaultQuery<>(Word.epsilon(),	1✔
81	Word.fromSymbols(new Msg<>(ID1, "d'"),	1✔
82	new Recv(),
83	new Msg<>(ID2, "d''")),
84	Word.fromSymbols("ind", "ack(0)", "ind")));	1✔
85	printInfo(learner);	1✔
86	}	1✔
87
88	private static <AI, CI, O> void printInfo(ExplicitAAARLearnerMealy<? extends OTLearnerMealy<CI, O>, AI, CI, O> learner)
89	throws IOException, InterruptedException {
90
91	System.out.println("-------------------------------------------------------");	1✔
92	new ObservationTableASCIIWriter<>().write(learner.getLearner().getObservationTable(), System.out);	1✔
93
94	if (DOT.checkUsable()) {	1✔
95	final MealyMachine<?, AI, ?, O> hyp = learner.getHypothesisModel();	1✔
96	final Map<AI, ExplicitAbstractionTree<AI, CI, Word<O>>> trees = learner.getAbstractionTrees();	1✔
97	final List<Graph<?, ?>> treesAsGraphs = new ArrayList<>(trees.size());	1✔
98
99	for (ExplicitAbstractionTree<AI, CI, Word<O>> t : trees.values()) {	1✔
100	treesAsGraphs.add(t.graphView());	1✔
101	}	1✔
102
103	try (StringWriter hypWriter = new StringWriter();	1✔
104	StringWriter treeWriter = new StringWriter()) {	1✔
105
106	GraphDOT.write(hyp.transitionGraphView(learner.getAbstractAlphabet()), hypWriter);	1✔
107	GraphDOT.write(treesAsGraphs, treeWriter);	1✔
108
109	DOT.renderDOTStrings(Arrays.asList(Pair.of("Hypothesis", hypWriter.toString()),	1✔
110	Pair.of("Abstraction Trees", treeWriter.toString())), true);	1✔
111	}
112	}
113	}	1✔
114
115	static final class InitialAbstraction implements ExplicitInitialAbstraction<String, Event> {	1✔
116
117	@Override
118	public String getAbstractSymbol(Event c) {
119	if (c instanceof Recv) {	1✔
120	return "recv";	1✔
121	} else if (c instanceof Msg) {	1✔
122	return "msg";	1✔
123	} else {
124	throw new IllegalArgumentException("Unknown event: " + c);	×
125	}
126	}
127
128	@Override
129	public Event getRepresentative(String a) {
130	return switch (a) {	1✔
131	case "recv" -> new Recv();	1✔
132	case "msg" -> new Msg<>(0, "d");	1✔
NEW 133	default -> throw new IllegalArgumentException("Unknown abstract: " + a);	×
134	};
135	}
136
137	@Override
138	public Collection<String> getInitialAbstracts() {
139	return Arrays.asList("recv", "msg");	1✔
140	}
141	}
142
143	static final class Incrementor implements Function<String, String> {	1✔
144
145	private int cnt;
146
147	@Override
148	public String apply(String s) {
149	return s + cnt++;	1✔
150	}
151	}
152	}

LearnLib / learnlib / 19556545386

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