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

/api/src/main/java/de/learnlib/api/logging/LoggingPropertyOracle.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.api.logging;

import java.util.Collection;

import de.learnlib.api.oracle.PropertyOracle;
import de.learnlib.api.query.DefaultQuery;
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;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * A PropertyOracle that performs logging.
 * <p>
 * This class will log whenever the property is disproved, or when a counterexample to an automaton is found (i.e. a
 * spurious counterexample is found).
 *
 * @param <I> the input type
 * @param <A> the automaton type
 * @param <P> the property type
 * @param <D> the output type
 */
public class LoggingPropertyOracle<I, A extends Output<I, D>, P, D> implements PropertyOracle<I, A, P, D> {

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

    /**
     * The wrapped {@link PropertyOracle}.
     */
    private final PropertyOracle<I, A, P, D> propertyOracle;

    /**
     * Constructs a new LoggingPropertyOracle.
     *
     * @param propertyOracle the {@link PropertyOracle} to wrap around.
     */
    public LoggingPropertyOracle(PropertyOracle<I, A, P, D> propertyOracle) {
        this.propertyOracle = propertyOracle;
    }

    @Override
    public boolean isDisproved() {
        return propertyOracle.isDisproved();
    }

    @Override
    public void setProperty(P property) {
        this.propertyOracle.setProperty(property);
    }

    @Override
    public P getProperty() {
        return propertyOracle.getProperty();
    }

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

    /**
     * Try to disprove this propertyOracle, and log whenever it is disproved.
     *
     * @see PropertyOracle#disprove(Output, Collection)
     */
    @Override
    public @Nullable DefaultQuery<I, D> disprove(A hypothesis, Collection<? extends I> inputs) {
        final DefaultQuery<I, D> result = propertyOracle.disprove(hypothesis, inputs);
        if (result != null) {
            LOGGER.info(Category.EVENT, "Property violated: '{}'", this);
            LOGGER.info(Category.QUERY, "Counter example for property: {}", getCounterExample());
        }

        return result;
    }

    /**
     * Try to find a counterexample to the given hypothesis, and log whenever such a spurious counterexample is found.
     *
     * @see PropertyOracle#findCounterExample(Output, Collection)
     */
    @Override
    public @Nullable DefaultQuery<I, D> doFindCounterExample(A hypothesis, Collection<? extends I> inputs) {
        final DefaultQuery<I, D> result = propertyOracle.findCounterExample(hypothesis, inputs);
        if (result != null) {
            LOGGER.info(Category.EVENT, "Spurious counterexample found for property: '{}'", this);
            LOGGER.info(Category.COUNTEREXAMPLE, "Spurious counterexample: {}", result);
        }
        return result;
    }

    @Override
    public String toString() {
        return String.valueOf(propertyOracle.getProperty());
    }

    public static class DFALoggingPropertyOracle<I, P> extends LoggingPropertyOracle<I, DFA<?, I>, P, Boolean>
            implements DFAPropertyOracle<I, P> {

        public DFALoggingPropertyOracle(DFAPropertyOracle<I, P> property) {
            super(property);
        }
    }

    public static class MealyLoggingPropertyOracle<I, O, P>
            extends LoggingPropertyOracle<I, MealyMachine<?, I, ?, O>, P, Word<O>>
            implements MealyPropertyOracle<I, O, P> {

        public MealyLoggingPropertyOracle(MealyPropertyOracle<I, O, P> property) {
            super(property);
        }
    }
}

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.api.logging;
17
18	import java.util.Collection;
19
20	import de.learnlib.api.oracle.PropertyOracle;
21	import de.learnlib.api.query.DefaultQuery;
22	import net.automatalib.automaton.concept.Output;
23	import net.automatalib.automaton.fsa.DFA;
24	import net.automatalib.automaton.transducer.MealyMachine;
25	import net.automatalib.word.Word;
26	import org.checkerframework.checker.nullness.qual.Nullable;
27	import org.slf4j.Logger;
28	import org.slf4j.LoggerFactory;
29
30	/**
31	* A PropertyOracle that performs logging.
32	* <p>
33	* This class will log whenever the property is disproved, or when a counterexample to an automaton is found (i.e. a
34	* spurious counterexample is found).
35	*
36	* @param <I> the input type
37	* @param <A> the automaton type
38	* @param <P> the property type
39	* @param <D> the output type
40	*/
41	public class LoggingPropertyOracle<I, A extends Output<I, D>, P, D> implements PropertyOracle<I, A, P, D> {
42
43	private static final Logger LOGGER = LoggerFactory.getLogger(LoggingPropertyOracle.class);	×
44
45	/**
46	* The wrapped {@link PropertyOracle}.
47	*/
48	private final PropertyOracle<I, A, P, D> propertyOracle;
49
50	/**
51	* Constructs a new LoggingPropertyOracle.
52	*
53	* @param propertyOracle the {@link PropertyOracle} to wrap around.
54	*/
55	public LoggingPropertyOracle(PropertyOracle<I, A, P, D> propertyOracle) {	×
56	this.propertyOracle = propertyOracle;	×
57	}	×
58
59	@Override
60	public boolean isDisproved() {
61	return propertyOracle.isDisproved();	×
62	}
63
64	@Override
65	public void setProperty(P property) {
66	this.propertyOracle.setProperty(property);	×
67	}	×
68
69	@Override
70	public P getProperty() {
71	return propertyOracle.getProperty();	×
72	}
73
74	@Override
75	public @Nullable DefaultQuery<I, D> getCounterExample() {
76	return propertyOracle.getCounterExample();	×
77	}
78
79	/**
80	* Try to disprove this propertyOracle, and log whenever it is disproved.
81	*
82	* @see PropertyOracle#disprove(Output, Collection)
83	*/
84	@Override
85	public @Nullable DefaultQuery<I, D> disprove(A hypothesis, Collection<? extends I> inputs) {
86	final DefaultQuery<I, D> result = propertyOracle.disprove(hypothesis, inputs);	×
87	if (result != null) {	×
88	LOGGER.info(Category.EVENT, "Property violated: '{}'", this);	×
89	LOGGER.info(Category.QUERY, "Counter example for property: {}", getCounterExample());	×
90	}
91
92	return result;	×
93	}
94
95	/**
96	* Try to find a counterexample to the given hypothesis, and log whenever such a spurious counterexample is found.
97	*
98	* @see PropertyOracle#findCounterExample(Output, Collection)
99	*/
100	@Override
101	public @Nullable DefaultQuery<I, D> doFindCounterExample(A hypothesis, Collection<? extends I> inputs) {
102	final DefaultQuery<I, D> result = propertyOracle.findCounterExample(hypothesis, inputs);	×
103	if (result != null) {	×
104	LOGGER.info(Category.EVENT, "Spurious counterexample found for property: '{}'", this);	×
105	LOGGER.info(Category.COUNTEREXAMPLE, "Spurious counterexample: {}", result);	×
106	}
107	return result;	×
108	}
109
110	@Override
111	public String toString() {
112	return String.valueOf(propertyOracle.getProperty());	×
113	}
114
115	public static class DFALoggingPropertyOracle<I, P> extends LoggingPropertyOracle<I, DFA<?, I>, P, Boolean>
116	implements DFAPropertyOracle<I, P> {
117
118	public DFALoggingPropertyOracle(DFAPropertyOracle<I, P> property) {
119	super(property);	×
120	}	×
121	}
122
123	public static class MealyLoggingPropertyOracle<I, O, P>
124	extends LoggingPropertyOracle<I, MealyMachine<?, I, ?, O>, P, Word<O>>
125	implements MealyPropertyOracle<I, O, P> {
126
127	public MealyLoggingPropertyOracle(MealyPropertyOracle<I, O, P> property) {
128	super(property);	×
129	}	×
130	}
131	}

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