6673301747

Committed 27 Oct 2023 11:46PM UTC coverage: 91.986% (-1.3%) from 93.327%

Build # 6673301747

Build Type

push

github

Committed by

mtf90

Commit Message

merge the release and sign-artifacts profiles

Run Details

10984 of 11941 relevant lines covered (91.99%)

1.72 hits per line

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

0.0

/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.automaton.concept.Output;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.word.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.
 */
@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.automaton.concept.Output;
32	import net.automatalib.automaton.fsa.DFA;
33	import net.automatalib.automaton.transducer.MealyMachine;
34	import net.automatalib.word.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	@GenerateRefinement(name = "DFAPropertyOracleChain",	×
55	generics = {"I", "P"},
56	parentGenerics = {@Generic("I"),
57	@Generic(clazz = DFA.class, generics = {"?", "I"}),
58	@Generic("P"),
59	@Generic(clazz = Boolean.class)},
60	parameterMapping = @Map(from = PropertyOracle.class,
61	to = DFAPropertyOracle.class,
62	withGenerics = {"I", "P"}),
63	interfaces = @Interface(clazz = DFAPropertyOracle.class, generics = {"I", "P"}))
64	@GenerateRefinement(name = "MealyPropertyOracleChain",
65	generics = {"I", "O", "P"},
66	parentGenerics = {@Generic("I"),
67	@Generic(clazz = MealyMachine.class, generics = {"?", "I", "?", "O"}),
68	@Generic("P"),
69	@Generic(clazz = Word.class, generics = "O")},
70	parameterMapping = @Map(from = PropertyOracle.class,
71	to = MealyPropertyOracle.class,
72	withGenerics = {"I", "O", "P"}),
73	interfaces = @Interface(clazz = MealyPropertyOracle.class, generics = {"I", "O", "P"}))
74	public class PropertyOracleChain<I, A extends Output<I, D>, @Nullable P, D> implements PropertyOracle<I, A, P, D> {
75
76	private P property;
77
78	private @Nullable DefaultQuery<I, D> counterExample;
79
80	private final List<PropertyOracle<I, ? super A, P, D>> oracles;
81
82	@SafeVarargs
83	public PropertyOracleChain(PropertyOracle<I, ? super A, P, D>... oracles) {
84	this(Arrays.asList(oracles));	×
85	}	×
86
87	public PropertyOracleChain(Collection<? extends PropertyOracle<I, ? super A, P, D>> oracles) {	×
88	this.oracles = new ArrayList<>(oracles);	×
89	if (!this.oracles.isEmpty()) {	×
90	property = this.oracles.get(0).getProperty();	×
91	} else {
92	property = null;	×
93	}
94	}	×
95
96	public void addOracle(PropertyOracle<I, ? super A, P, D> oracle) {
97	assert oracle.getProperty() == null \|\| oracle.getProperty().equals(property);	×
98	oracle.setProperty(property);	×
99	oracles.add(oracle);	×
100	}	×
101
102	@Override
103	public @Nullable DefaultQuery<I, D> doFindCounterExample(A hypothesis, Collection<? extends I> inputs) {
104	for (PropertyOracle<I, ? super A, P, D> oracle : oracles) {	×
105	DefaultQuery<I, D> ceQry = oracle.findCounterExample(hypothesis, inputs);	×
106	if (ceQry != null) {	×
107	return ceQry;	×
108	}
109	}	×
110
111	return null;	×
112	}
113
114	@Override
115	public @Nullable DefaultQuery<I, D> disprove(A hypothesis, Collection<? extends I> inputs) {
116	for (PropertyOracle<I, ? super A, P, D> oracle : oracles) {	×
117	DefaultQuery<I, D> ceQry = oracle.disprove(hypothesis, inputs);	×
118	if (ceQry != null) {	×
119	counterExample = ceQry;	×
120	return ceQry;	×
121	}
122	}	×
123
124	return null;	×
125	}
126
127	@Override
128	public void setProperty(P property) {
129	oracles.forEach(o -> o.setProperty(property));	×
130	this.property = property;	×
131	}	×
132
133	@Override
134	public P getProperty() {
135	return property;	×
136	}
137
138	@Override
139	public @Nullable DefaultQuery<I, D> getCounterExample() {
140	return counterExample;	×
141	}
142	}

LearnLib / learnlib / 6673301747

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