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

87.5

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

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