6412002873

Committed 04 Oct 2023 10:05PM UTC coverage: 92.303% (+0.02%) from 92.282%

Build # 6412002873

Build Type

push

github

Committed by

mtf90

Commit Message

further tweak versions

* downgrade maven-javadoc-plugin version because it (for whatever reason) doesn't work on Java 11+
* update previously missed doc skin version

Run Details

11573 of 12538 relevant lines covered (92.3%)

1.67 hits per line

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

48.39

/oracles/property-oracles/src/main/java/de/learnlib/oracle/property/PropertyOracleChain.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.oracle.property;

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

import de.learnlib.api.oracle.PropertyOracle;
import de.learnlib.api.oracle.PropertyOracle.DFAPropertyOracle;
import de.learnlib.api.oracle.PropertyOracle.MealyPropertyOracle;
import de.learnlib.api.query.DefaultQuery;
import de.learnlib.buildtool.refinement.annotation.GenerateRefinement;
import de.learnlib.buildtool.refinement.annotation.Generic;
import de.learnlib.buildtool.refinement.annotation.Interface;
import de.learnlib.buildtool.refinement.annotation.Map;
import net.automatalib.automata.concepts.Output;
import net.automatalib.automata.fsa.DFA;
import net.automatalib.automata.transducers.MealyMachine;
import net.automatalib.words.Word;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A chain of property oracles. Useful when combining multiple model checking strategies to disprove a property, or when
 * finding counter examples to hypotheses.
 * <p>
 * For example, you may want to construct a chain that first uses a model checker for monitors, and next, one that uses
 * a model checker for full LTL. This strategy tends to give shorter counter examples for properties, and these counter
 * examples can be found more quickly (as in smaller hypothesis size and less learning queries).
 *
 * @param <I>
 *         the input type.
 * @param <A>
 *         the automaton type.
 * @param <P>
 *         the property type.
 * @param <D>
 *         the output type.
 *
 * @author Jeroen Meijer
 */
@GenerateRefinement(name = "DFAPropertyOracleChain",
                    generics = {"I", "P"},
                    parentGenerics = {@Generic("I"),
                                      @Generic(clazz = DFA.class, generics = {"?", "I"}),
                                      @Generic("P"),
                                      @Generic(clazz = Boolean.class)},
                    parameterMapping = @Map(from = PropertyOracle.class,
                                            to = DFAPropertyOracle.class,
                                            withGenerics = {"I", "P"}),
                    interfaces = @Interface(clazz = DFAPropertyOracle.class, generics = {"I", "P"}))
@GenerateRefinement(name = "MealyPropertyOracleChain",
                    generics = {"I", "O", "P"},
                    parentGenerics = {@Generic("I"),
                                      @Generic(clazz = MealyMachine.class, generics = {"?", "I", "?", "O"}),
                                      @Generic("P"),
                                      @Generic(clazz = Word.class, generics = "O")},
                    parameterMapping = @Map(from = PropertyOracle.class,
                                            to = MealyPropertyOracle.class,
                                            withGenerics = {"I", "O", "P"}),
                    interfaces = @Interface(clazz = MealyPropertyOracle.class, generics = {"I", "O", "P"}))
public class PropertyOracleChain<I, A extends Output<I, D>, @Nullable P, D> implements PropertyOracle<I, A, P, D> {

    private P property;

    private @Nullable DefaultQuery<I, D> counterExample;

    private final List<PropertyOracle<I, ? super A, P, D>> oracles;

    @SafeVarargs
    public PropertyOracleChain(PropertyOracle<I, ? super A, P, D>... oracles) {
        this(Arrays.asList(oracles));
    }

    public PropertyOracleChain(Collection<? extends PropertyOracle<I, ? super A, P, D>> oracles) {
        this.oracles = new ArrayList<>(oracles);
        if (!this.oracles.isEmpty()) {
            property = this.oracles.get(0).getProperty();
        } else {
            property = null;
        }
    }

    public void addOracle(PropertyOracle<I, ? super A, P, D> oracle) {
        assert oracle.getProperty() == null || oracle.getProperty().equals(property);
        oracle.setProperty(property);
        oracles.add(oracle);
    }

    @Override
    public @Nullable DefaultQuery<I, D> doFindCounterExample(A hypothesis, Collection<? extends I> inputs) {
        for (PropertyOracle<I, ? super A, P, D> oracle : oracles) {
            DefaultQuery<I, D> ceQry = oracle.findCounterExample(hypothesis, inputs);
            if (ceQry != null) {
                return ceQry;
            }
        }

        return null;
    }

    @Override
    public @Nullable DefaultQuery<I, D> disprove(A hypothesis, Collection<? extends I> inputs) {
        for (PropertyOracle<I, ? super A, P, D> oracle : oracles) {
            DefaultQuery<I, D> ceQry = oracle.disprove(hypothesis, inputs);
            if (ceQry != null) {
                counterExample = ceQry;
                return ceQry;
            }
        }

        return null;
    }

    @Override
    public void setProperty(P property) {
        oracles.forEach(o -> o.setProperty(property));
        this.property = property;
    }

    @Override
    public P getProperty() {
        return property;
    }

    @Override
    public @Nullable DefaultQuery<I, D> getCounterExample() {
        return counterExample;
    }
}

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.oracle.property;
17
18	import java.util.ArrayList;
19	import java.util.Arrays;
20	import java.util.Collection;
21	import java.util.List;
22
23	import de.learnlib.api.oracle.PropertyOracle;
24	import de.learnlib.api.oracle.PropertyOracle.DFAPropertyOracle;
25	import de.learnlib.api.oracle.PropertyOracle.MealyPropertyOracle;
26	import de.learnlib.api.query.DefaultQuery;
27	import de.learnlib.buildtool.refinement.annotation.GenerateRefinement;
28	import de.learnlib.buildtool.refinement.annotation.Generic;
29	import de.learnlib.buildtool.refinement.annotation.Interface;
30	import de.learnlib.buildtool.refinement.annotation.Map;
31	import net.automatalib.automata.concepts.Output;
32	import net.automatalib.automata.fsa.DFA;
33	import net.automatalib.automata.transducers.MealyMachine;
34	import net.automatalib.words.Word;
35	import org.checkerframework.checker.nullness.qual.Nullable;
36
37	/**
38	* A chain of property oracles. Useful when combining multiple model checking strategies to disprove a property, or when
39	* finding counter examples to hypotheses.
40	* <p>
41	* For example, you may want to construct a chain that first uses a model checker for monitors, and next, one that uses
42	* a model checker for full LTL. This strategy tends to give shorter counter examples for properties, and these counter
43	* examples can be found more quickly (as in smaller hypothesis size and less learning queries).
44	*
45	* @param <I>
46	* the input type.
47	* @param <A>
48	* the automaton type.
49	* @param <P>
50	* the property type.
51	* @param <D>
52	* the output type.
53	*
54	* @author Jeroen Meijer
55	*/
56	@GenerateRefinement(name = "DFAPropertyOracleChain",	1✔
57	generics = {"I", "P"},
58	parentGenerics = {@Generic("I"),
59	@Generic(clazz = DFA.class, generics = {"?", "I"}),
60	@Generic("P"),
61	@Generic(clazz = Boolean.class)},
62	parameterMapping = @Map(from = PropertyOracle.class,
63	to = DFAPropertyOracle.class,
64	withGenerics = {"I", "P"}),
65	interfaces = @Interface(clazz = DFAPropertyOracle.class, generics = {"I", "P"}))
66	@GenerateRefinement(name = "MealyPropertyOracleChain",
67	generics = {"I", "O", "P"},
68	parentGenerics = {@Generic("I"),
69	@Generic(clazz = MealyMachine.class, generics = {"?", "I", "?", "O"}),
70	@Generic("P"),
71	@Generic(clazz = Word.class, generics = "O")},
72	parameterMapping = @Map(from = PropertyOracle.class,
73	to = MealyPropertyOracle.class,
74	withGenerics = {"I", "O", "P"}),
75	interfaces = @Interface(clazz = MealyPropertyOracle.class, generics = {"I", "O", "P"}))
76	public class PropertyOracleChain<I, A extends Output<I, D>, @Nullable P, D> implements PropertyOracle<I, A, P, D> {
77
78	private P property;
79
80	private @Nullable DefaultQuery<I, D> counterExample;
81
82	private final List<PropertyOracle<I, ? super A, P, D>> oracles;
83
84	@SafeVarargs
85	public PropertyOracleChain(PropertyOracle<I, ? super A, P, D>... oracles) {
86	this(Arrays.asList(oracles));	1✔
87	}	1✔
88
89	public PropertyOracleChain(Collection<? extends PropertyOracle<I, ? super A, P, D>> oracles) {	1✔
90	this.oracles = new ArrayList<>(oracles);	1✔
91	if (!this.oracles.isEmpty()) {	1✔
92	property = this.oracles.get(0).getProperty();	1✔
93	} else {
94	property = null;	×
95	}
96	}	1✔
97
98	public void addOracle(PropertyOracle<I, ? super A, P, D> oracle) {
99	assert oracle.getProperty() == null \|\| oracle.getProperty().equals(property);	×
100	oracle.setProperty(property);	×
101	oracles.add(oracle);	×
102	}	×
103
104	@Override
105	public @Nullable DefaultQuery<I, D> doFindCounterExample(A hypothesis, Collection<? extends I> inputs) {
106	for (PropertyOracle<I, ? super A, P, D> oracle : oracles) {	×
107	DefaultQuery<I, D> ceQry = oracle.findCounterExample(hypothesis, inputs);	×
108	if (ceQry != null) {	×
109	return ceQry;	×
110	}
111	}	×
112
113	return null;	×
114	}
115
116	@Override
117	public @Nullable DefaultQuery<I, D> disprove(A hypothesis, Collection<? extends I> inputs) {
118	for (PropertyOracle<I, ? super A, P, D> oracle : oracles) {	1✔
119	DefaultQuery<I, D> ceQry = oracle.disprove(hypothesis, inputs);	1✔
120	if (ceQry != null) {	1✔
121	counterExample = ceQry;	1✔
122	return ceQry;	1✔
123	}
124	}	×
125
126	return null;	×
127	}
128
129	@Override
130	public void setProperty(P property) {
131	oracles.forEach(o -> o.setProperty(property));	×
132	this.property = property;	×
133	}	×
134
135	@Override
136	public P getProperty() {
137	return property;	1✔
138	}
139
140	@Override
141	public @Nullable DefaultQuery<I, D> getCounterExample() {
142	return counterExample;	1✔
143	}
144	}

LearnLib / learnlib / 6412002873

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