-
Notifications
You must be signed in to change notification settings - Fork 44
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add ProtectedIndependenceRelation, instantiate to protect against qua…
…ntifiers
- Loading branch information
Showing
2 changed files
with
123 additions
and
0 deletions.
There are no files selected for viewing
112 changes: 112 additions & 0 deletions
112
...informatik/ultimate/automata/partialorder/independence/ProtectedIndependenceRelation.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,112 @@ | ||
| /* | ||
| * Copyright (C) 2022 Dominik Klumpp ([email protected]) | ||
| * Copyright (C) 2022 University of Freiburg | ||
| * | ||
| * This file is part of the ULTIMATE Automata Library. | ||
| * | ||
| * The ULTIMATE Automata Library is free software: you can redistribute it and/or modify | ||
| * it under the terms of the GNU Lesser General Public License as published | ||
| * by the Free Software Foundation, either version 3 of the License, or | ||
| * (at your option) any later version. | ||
| * | ||
| * The ULTIMATE Automata Library is distributed in the hope that it will be useful, | ||
| * but WITHOUT ANY WARRANTY; without even the implied warranty of | ||
| * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | ||
| * GNU Lesser General Public License for more details. | ||
| * | ||
| * You should have received a copy of the GNU Lesser General Public License | ||
| * along with the ULTIMATE Automata Library. If not, see <http://www.gnu.org/licenses/>. | ||
| * | ||
| * Additional permission under GNU GPL version 3 section 7: | ||
| * If you modify the ULTIMATE Automata Library, or any covered work, by linking | ||
| * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), | ||
| * containing parts covered by the terms of the Eclipse Public License, the | ||
| * licensors of the ULTIMATE Automata Library grant you additional permission | ||
| * to convey the resulting work. | ||
| */ | ||
| package de.uni_freiburg.informatik.ultimate.automata.partialorder.independence; | ||
|
|
||
| /** | ||
| * An independence relation that protects an underlying relation from certain queries (e.g. queries that are expected to | ||
| * be expensive) and returns {@code Dependence.UNKNOWN} instead. | ||
| * | ||
| * @author Dominik Klumpp ([email protected]) | ||
| * | ||
| * @param <S> | ||
| * The type of states (i.e. conditions) of the relation | ||
| * @param <L> | ||
| * The type of letters that are checked for independence | ||
| */ | ||
| public class ProtectedIndependenceRelation<S, L> implements IIndependenceRelation<S, L> { | ||
| private final IIndependenceRelation<S, L> mUnderlying; | ||
| private final IFilter<L> mFilter; | ||
|
|
||
| /** | ||
| * Create a new protecting wrapper around a given relation. | ||
| * | ||
| * @param underlying | ||
| * The underlying relation to protect | ||
| * @param filter | ||
| * A filter that determines which queries are allowed and which simply return {@code UNKNOWN} | ||
| */ | ||
| public ProtectedIndependenceRelation(final IIndependenceRelation<S, L> underlying, final IFilter<L> filter) { | ||
| mUnderlying = underlying; | ||
| mFilter = filter; | ||
| } | ||
|
|
||
| @Override | ||
| public boolean isSymmetric() { | ||
| return mUnderlying.isSymmetric(); | ||
| } | ||
|
|
||
| @Override | ||
| public boolean isConditional() { | ||
| return mUnderlying.isConditional(); | ||
| } | ||
|
|
||
| @Override | ||
| public Dependence isIndependent(final S state, final L a, final L b) { | ||
| if (mFilter.test(a) && mFilter.test(b)) { | ||
| final var result = mUnderlying.isIndependent(state, a, b); | ||
| mFilter.update(a, b, result); | ||
| return result; | ||
| } | ||
| return Dependence.UNKNOWN; | ||
| } | ||
|
|
||
| /** | ||
| * A filter predicate for independence relations. The filter can also learn from past queries and therefore change | ||
| * over time. | ||
| * | ||
| * @author Dominik Klumpp ([email protected]) | ||
| * | ||
| * @param <L> | ||
| * The type of letters being filtered | ||
| */ | ||
| @FunctionalInterface | ||
| public interface IFilter<L> { | ||
| /** | ||
| * Determines if a given letter passes the filter. | ||
| * | ||
| * @param a | ||
| * The letter to test | ||
| * @return true if the letter passes the filter, i.e., a query involving this letter can be performed; false if | ||
| * queries involving this letter should not be performed. | ||
| */ | ||
| boolean test(L a); | ||
|
|
||
| /** | ||
| * Called whenever a query was performed, to allow the filter to update its internal state. | ||
| * | ||
| * @param a | ||
| * The first letter | ||
| * @param b | ||
| * The second letter | ||
| * @param result | ||
| * The result of the independence query | ||
| */ | ||
| default void update(final L a, final L b, final Dependence result) { | ||
| // by default, do nothing | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters