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

95.65

/examples/src/main/java/de/learnlib/examples/bbc/Example4.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.examples.bbc;

import java.util.function.Function;

import de.learnlib.acex.analyzers.AcexAnalyzers;
import de.learnlib.algorithms.ttt.dfa.TTTLearnerDFA;
import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner;
import de.learnlib.api.logging.LoggingPropertyOracle.DFALoggingPropertyOracle;
import de.learnlib.api.oracle.EmptinessOracle.DFAEmptinessOracle;
import de.learnlib.api.oracle.EquivalenceOracle.DFAEquivalenceOracle;
import de.learnlib.api.oracle.InclusionOracle.DFAInclusionOracle;
import de.learnlib.api.oracle.LassoEmptinessOracle.DFALassoEmptinessOracle;
import de.learnlib.api.oracle.MembershipOracle.DFAMembershipOracle;
import de.learnlib.api.oracle.OmegaMembershipOracle.DFAOmegaMembershipOracle;
import de.learnlib.api.oracle.PropertyOracle.DFAPropertyOracle;
import de.learnlib.examples.LearningExample.DFALearningExample;
import de.learnlib.examples.dfa.ExampleTinyDFA;
import de.learnlib.oracle.emptiness.DFABFEmptinessOracle;
import de.learnlib.oracle.emptiness.DFALassoEmptinessOracleImpl;
import de.learnlib.oracle.equivalence.DFABFInclusionOracle;
import de.learnlib.oracle.equivalence.DFACExFirstOracle;
import de.learnlib.oracle.equivalence.DFAEQOracleChain;
import de.learnlib.oracle.equivalence.DFAWpMethodEQOracle;
import de.learnlib.oracle.membership.SimulatorOmegaOracle.DFASimulatorOmegaOracle;
import de.learnlib.oracle.property.DFAFinitePropertyOracle;
import de.learnlib.oracle.property.DFALassoPropertyOracle;
import de.learnlib.oracle.property.DFAPropertyOracleChain;
import de.learnlib.util.Experiment.DFAExperiment;
import net.automatalib.automata.fsa.DFA;
import net.automatalib.modelcheckers.ltsmin.LTSminUtil;
import net.automatalib.modelcheckers.ltsmin.LTSminVersion;
import net.automatalib.modelcheckers.ltsmin.ltl.LTSminLTLDFABuilder;
import net.automatalib.modelcheckers.ltsmin.monitor.LTSminMonitorDFABuilder;
import net.automatalib.modelchecking.ModelChecker.DFAModelChecker;
import net.automatalib.modelchecking.ModelCheckerLasso.DFAModelCheckerLasso;
import net.automatalib.util.automata.equivalence.DeterministicEquivalenceTest;
import net.automatalib.words.Alphabet;

/**
 * Runs a black-box checking experiment for a DFA.
 * <p>
 * This example is similar to {@link Example1}, except that is also uses a monitor to disprove properties for the
 * learned DFA.
 */
public final class Example4 {

    /**
     * A function that transforms edges in an FSM source to actual input for a DFA.
     */
    public static final Function<String, Character> EDGE_PARSER = s -> s.charAt(0);

    private Example4() {}

    public static void main(String[] args) {

        // This code requires v3.1.0
        if (!LTSminUtil.supports(LTSminVersion.of(3, 1, 0))) {
            return;
        }

        DFALearningExample<Character> le = ExampleTinyDFA.createExample();

        // define the alphabet
        Alphabet<Character> sigma = le.getAlphabet();

        // create the DFA to be verified/learned
        DFA<?, Character> dfa = le.getReferenceAutomaton();

        // create an omega membership oracle
        DFAOmegaMembershipOracle<?, Character> omqOracle = new DFASimulatorOmegaOracle<>(dfa);

        // create a regular membership oracle
        DFAMembershipOracle<Character> mqOracle = omqOracle.getMembershipOracle();

        // create a learner
        DFALearner<Character> learner = new TTTLearnerDFA<>(sigma, mqOracle, AcexAnalyzers.LINEAR_FWD);

        // create a model checker that uses a Buchi automaton
        DFAModelCheckerLasso<Character, String> modelCheckerBuchi =
                new LTSminLTLDFABuilder<Character>().withString2Input(EDGE_PARSER).create();

        // create a lasso emptiness oracle, that is used to disprove properties
        DFALassoEmptinessOracle<Character> lassoEmptinessOracle = new DFALassoEmptinessOracleImpl<>(omqOracle);

        // create a model checker that uses monitors
        DFAModelChecker<Character, String, DFA<?, Character>> modelCheckerMonitor =
                new LTSminMonitorDFABuilder<Character>().withString2Input(EDGE_PARSER).create();

        // create an emptiness oracle, that is used to disprove properties.
        DFAEmptinessOracle<Character> emptinessOracle = new DFABFEmptinessOracle<>(mqOracle, 1.0);

        // create an inclusion oracle, that is used to find counterexamples to hypotheses
        DFAInclusionOracle<Character> inclusionOracle = new DFABFInclusionOracle<>(mqOracle, 1.0);

        // create an LTL property oracle, that also logs stuff
        // also it chains the property oracle that uses monitors and Buchi automata
        DFAPropertyOracle<Character, String> ltl = new DFALoggingPropertyOracle<>(
                new DFAPropertyOracleChain<>(
                        new DFAFinitePropertyOracle<>("letter==\"b\"", inclusionOracle, emptinessOracle, modelCheckerMonitor),
                        new DFALassoPropertyOracle<>("letter==\"b\"", inclusionOracle, lassoEmptinessOracle, modelCheckerBuchi)));

        // create an equivalence oracle, that first searches for a counter example using the ltl properties, and next
        // with the W-method.
        DFAEquivalenceOracle<Character> eqOracle =
                new DFAEQOracleChain<>(new DFACExFirstOracle<>(ltl), new DFAWpMethodEQOracle<>(mqOracle, 3));

        // create an experiment
        DFAExperiment<Character> experiment = new DFAExperiment<>(learner, eqOracle, sigma);

        // run the experiment
        experiment.run();

        // get the result
        final DFA<?, Character> result = experiment.getFinalHypothesis();

        // assert we have the correct result
        assert DeterministicEquivalenceTest.findSeparatingWord(dfa, result, sigma) == null;
    }
}

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.examples.bbc;
17
18	import java.util.function.Function;
19
20	import de.learnlib.acex.analyzers.AcexAnalyzers;
21	import de.learnlib.algorithms.ttt.dfa.TTTLearnerDFA;
22	import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner;
23	import de.learnlib.api.logging.LoggingPropertyOracle.DFALoggingPropertyOracle;
24	import de.learnlib.api.oracle.EmptinessOracle.DFAEmptinessOracle;
25	import de.learnlib.api.oracle.EquivalenceOracle.DFAEquivalenceOracle;
26	import de.learnlib.api.oracle.InclusionOracle.DFAInclusionOracle;
27	import de.learnlib.api.oracle.LassoEmptinessOracle.DFALassoEmptinessOracle;
28	import de.learnlib.api.oracle.MembershipOracle.DFAMembershipOracle;
29	import de.learnlib.api.oracle.OmegaMembershipOracle.DFAOmegaMembershipOracle;
30	import de.learnlib.api.oracle.PropertyOracle.DFAPropertyOracle;
31	import de.learnlib.examples.LearningExample.DFALearningExample;
32	import de.learnlib.examples.dfa.ExampleTinyDFA;
33	import de.learnlib.oracle.emptiness.DFABFEmptinessOracle;
34	import de.learnlib.oracle.emptiness.DFALassoEmptinessOracleImpl;
35	import de.learnlib.oracle.equivalence.DFABFInclusionOracle;
36	import de.learnlib.oracle.equivalence.DFACExFirstOracle;
37	import de.learnlib.oracle.equivalence.DFAEQOracleChain;
38	import de.learnlib.oracle.equivalence.DFAWpMethodEQOracle;
39	import de.learnlib.oracle.membership.SimulatorOmegaOracle.DFASimulatorOmegaOracle;
40	import de.learnlib.oracle.property.DFAFinitePropertyOracle;
41	import de.learnlib.oracle.property.DFALassoPropertyOracle;
42	import de.learnlib.oracle.property.DFAPropertyOracleChain;
43	import de.learnlib.util.Experiment.DFAExperiment;
44	import net.automatalib.automata.fsa.DFA;
45	import net.automatalib.modelcheckers.ltsmin.LTSminUtil;
46	import net.automatalib.modelcheckers.ltsmin.LTSminVersion;
47	import net.automatalib.modelcheckers.ltsmin.ltl.LTSminLTLDFABuilder;
48	import net.automatalib.modelcheckers.ltsmin.monitor.LTSminMonitorDFABuilder;
49	import net.automatalib.modelchecking.ModelChecker.DFAModelChecker;
50	import net.automatalib.modelchecking.ModelCheckerLasso.DFAModelCheckerLasso;
51	import net.automatalib.util.automata.equivalence.DeterministicEquivalenceTest;
52	import net.automatalib.words.Alphabet;
53
54	/**
55	* Runs a black-box checking experiment for a DFA.
56	* <p>
57	* This example is similar to {@link Example1}, except that is also uses a monitor to disprove properties for the
58	* learned DFA.
59	*/
60	public final class Example4 {
61
62	/**
63	* A function that transforms edges in an FSM source to actual input for a DFA.
64	*/
65	public static final Function<String, Character> EDGE_PARSER = s -> s.charAt(0);	1✔
66
67	private Example4() {}
68
69	public static void main(String[] args) {
70
71	// This code requires v3.1.0
72	if (!LTSminUtil.supports(LTSminVersion.of(3, 1, 0))) {	1✔
73	return;	×
74	}
75
76	DFALearningExample<Character> le = ExampleTinyDFA.createExample();	1✔
77
78	// define the alphabet
79	Alphabet<Character> sigma = le.getAlphabet();	1✔
80
81	// create the DFA to be verified/learned
82	DFA<?, Character> dfa = le.getReferenceAutomaton();	1✔
83
84	// create an omega membership oracle
85	DFAOmegaMembershipOracle<?, Character> omqOracle = new DFASimulatorOmegaOracle<>(dfa);	1✔
86
87	// create a regular membership oracle
88	DFAMembershipOracle<Character> mqOracle = omqOracle.getMembershipOracle();	1✔
89
90	// create a learner
91	DFALearner<Character> learner = new TTTLearnerDFA<>(sigma, mqOracle, AcexAnalyzers.LINEAR_FWD);	1✔
92
93	// create a model checker that uses a Buchi automaton
94	DFAModelCheckerLasso<Character, String> modelCheckerBuchi =	1✔
95	new LTSminLTLDFABuilder<Character>().withString2Input(EDGE_PARSER).create();	1✔
96
97	// create a lasso emptiness oracle, that is used to disprove properties
98	DFALassoEmptinessOracle<Character> lassoEmptinessOracle = new DFALassoEmptinessOracleImpl<>(omqOracle);	1✔
99
100	// create a model checker that uses monitors
101	DFAModelChecker<Character, String, DFA<?, Character>> modelCheckerMonitor =	1✔
102	new LTSminMonitorDFABuilder<Character>().withString2Input(EDGE_PARSER).create();	1✔
103
104	// create an emptiness oracle, that is used to disprove properties.
105	DFAEmptinessOracle<Character> emptinessOracle = new DFABFEmptinessOracle<>(mqOracle, 1.0);	1✔
106
107	// create an inclusion oracle, that is used to find counterexamples to hypotheses
108	DFAInclusionOracle<Character> inclusionOracle = new DFABFInclusionOracle<>(mqOracle, 1.0);	1✔
109
110	// create an LTL property oracle, that also logs stuff
111	// also it chains the property oracle that uses monitors and Buchi automata
112	DFAPropertyOracle<Character, String> ltl = new DFALoggingPropertyOracle<>(	1✔
113	new DFAPropertyOracleChain<>(
114	new DFAFinitePropertyOracle<>("letter==\"b\"", inclusionOracle, emptinessOracle, modelCheckerMonitor),
115	new DFALassoPropertyOracle<>("letter==\"b\"", inclusionOracle, lassoEmptinessOracle, modelCheckerBuchi)));
116
117	// create an equivalence oracle, that first searches for a counter example using the ltl properties, and next
118	// with the W-method.
119	DFAEquivalenceOracle<Character> eqOracle =	1✔
120	new DFAEQOracleChain<>(new DFACExFirstOracle<>(ltl), new DFAWpMethodEQOracle<>(mqOracle, 3));
121
122	// create an experiment
123	DFAExperiment<Character> experiment = new DFAExperiment<>(learner, eqOracle, sigma);	1✔
124
125	// run the experiment
126	experiment.run();	1✔
127
128	// get the result
129	final DFA<?, Character> result = experiment.getFinalHypothesis();	1✔
130
131	// assert we have the correct result
132	assert DeterministicEquivalenceTest.findSeparatingWord(dfa, result, sigma) == null;	1✔
133	}	1✔
134	}

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