04.07., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

...
 
Commits (2)
......@@ -49,6 +49,8 @@ API:
* Overhaul of the C++-API. Most notably there is an API for approximative realisability checks for a
state in the decomposed DPA.
* Add basic support for ultimately periodic words and add language membership tests.
Bugfixes:
* Throw an exception on malformed LTL input such as `FF`, `Fa!` and `F+`. Thanks
......
......@@ -34,7 +34,7 @@ import java.util.function.IntConsumer;
import owl.automaton.Automaton.EdgeMapVisitor;
import owl.automaton.acceptance.GeneralizedBuchiAcceptance;
import owl.automaton.acceptance.OmegaAcceptance;
import owl.automaton.algorithms.EmptinessCheck;
import owl.automaton.algorithms.LanguageEmptiness;
import owl.automaton.algorithms.SccDecomposition;
import owl.automaton.edge.Edge;
import owl.collections.ValuationSet;
......@@ -192,7 +192,7 @@ public final class AutomatonUtil {
.stateFilter(scc::contains)
.build();
if (!EmptinessCheck.isEmpty(Views.createView(automaton, viewSettings))) {
if (!LanguageEmptiness.isEmpty(Views.createView(automaton, viewSettings))) {
acceptingSccs.addAll(scc);
}
}
......
/*
* Copyright (C) 2016 - 2018 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program 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 General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.automaton;
import static java.util.stream.Collectors.toUnmodifiableList;
import com.google.common.base.Preconditions;
import de.tum.in.naturals.bitset.ImmutableBitSet;
import java.util.BitSet;
import java.util.List;
import java.util.Objects;
public final class UltimatelyPeriodicWord {
public final List<BitSet> prefix;
public final List<BitSet> period;
public UltimatelyPeriodicWord(List<BitSet> prefix, List<BitSet> period) {
this.prefix = prefix.stream().map(ImmutableBitSet::copyOf).collect(toUnmodifiableList());
this.period = period.stream().map(ImmutableBitSet::copyOf).collect(toUnmodifiableList());
Preconditions.checkArgument(!this.period.isEmpty());
}
@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (!(o instanceof UltimatelyPeriodicWord)) {
return false;
}
UltimatelyPeriodicWord that = (UltimatelyPeriodicWord) o;
return prefix.equals(that.prefix) && period.equals(that.period);
}
@Override
public int hashCode() {
return Objects.hash(prefix, period);
}
}
......@@ -29,9 +29,9 @@ import owl.automaton.Views;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.CoBuchiAcceptance;
public final class LanguageAnalysis {
public final class LanguageContainment {
private LanguageAnalysis() {}
private LanguageContainment() {}
/**
* Checks if the first the language of the first automaton is included in the language of the
......@@ -54,7 +54,7 @@ public final class LanguageAnalysis {
var casted1 = AutomatonUtil.cast(automaton1, Object.class, BuchiAcceptance.class);
var casted2 = AutomatonUtil.cast(automaton2, Object.class, BuchiAcceptance.class);
return EmptinessCheck.isEmpty(AutomatonOperations.intersection(List.of(casted1,
return LanguageEmptiness.isEmpty(AutomatonOperations.intersection(List.of(casted1,
AutomatonUtil.cast(Views.complement(casted2, new Object()), CoBuchiAcceptance.class))));
}
}
......@@ -38,8 +38,8 @@ import owl.automaton.acceptance.RabinAcceptance;
import owl.automaton.edge.Edge;
import owl.automaton.transformations.RabinDegeneralization;
public final class EmptinessCheck {
private EmptinessCheck() {}
public final class LanguageEmptiness {
private LanguageEmptiness() {}
public static <S> boolean isEmpty(Automaton<S, ?> automaton) {
return automaton.initialStates().stream().allMatch(state -> isEmpty(automaton, state));
......@@ -157,7 +157,7 @@ public final class EmptinessCheck {
/* assert Parity.containsAcceptingLasso(casted, initialState)
== Parity.containsAcceptingScc(casted, initialState); */
return !EmptinessCheck.Parity.containsAcceptingLasso(casted, initialState);
return !LanguageEmptiness.Parity.containsAcceptingLasso(casted, initialState);
}
if (acceptance instanceof RabinAcceptance) {
......@@ -176,7 +176,7 @@ public final class EmptinessCheck {
}
throw new UnsupportedOperationException(
String.format("Emptiness check for %s not yet implemented.", acceptance.name()));
String.format("Emptiness check for %s not yet implemented.", acceptance.getClass()));
}
private static final class Buchi {
......
/*
* Copyright (C) 2016 - 2018 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program 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 General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.automaton.algorithms;
import java.util.BitSet;
import java.util.Set;
import java.util.stream.Collectors;
import org.immutables.value.Value;
import owl.automaton.AbstractCachedStatesAutomaton;
import owl.automaton.Automaton;
import owl.automaton.EdgesAutomatonMixin;
import owl.automaton.UltimatelyPeriodicWord;
import owl.automaton.acceptance.OmegaAcceptance;
import owl.automaton.edge.Edge;
import owl.automaton.util.AnnotatedState;
import owl.factories.ValuationSetFactory;
import owl.util.annotation.HashedTuple;
public final class LanguageMembership {
private LanguageMembership() {
}
public static <S, A extends OmegaAcceptance> boolean contains(Automaton<S, A> automaton,
UltimatelyPeriodicWord word) {
return !LanguageEmptiness.isEmpty(new IndexedAutomaton<>(automaton, word));
}
@Value.Immutable
@HashedTuple
abstract static class IndexedState<S> implements AnnotatedState<S> {
abstract int index();
static <S> IndexedState<S> of(int index, S state) {
return IndexedStateTuple.create(index, state);
}
}
private static class IndexedAutomaton<S, A extends OmegaAcceptance>
extends AbstractCachedStatesAutomaton<IndexedState<S>, A>
implements EdgesAutomatonMixin<IndexedState<S>, A> {
private final Automaton<S, A> automaton;
private final UltimatelyPeriodicWord word;
private IndexedAutomaton(Automaton<S, A> automaton,
UltimatelyPeriodicWord word) {
this.automaton = automaton;
this.word = word;
}
@Override
public A acceptance() {
return automaton.acceptance();
}
@Override
public ValuationSetFactory factory() {
return automaton.factory();
}
@Override
public Set<IndexedState<S>> initialStates() {
return automaton.initialStates().stream()
.map(x -> IndexedStateTuple.create(-word.prefix.size(), x))
.collect(Collectors.toUnmodifiableSet());
}
@Override
public Set<Edge<IndexedState<S>>> edges(IndexedState<S> state, BitSet valuation) {
BitSet allowedValuation;
if (state.index() < 0) {
allowedValuation = word.prefix.get(-state.index() - 1);
} else {
allowedValuation = word.period.get(state.index());
}
if (!allowedValuation.equals(valuation)) {
return Set.of();
}
Set<Edge<S>> edges = automaton.edges(state.state(), valuation);
int nextIndex;
if (state.index() + 1 >= word.period.size()) {
nextIndex = (state.index() + 1) % word.period.size();
} else {
nextIndex = state.index() + 1;
}
return edges.stream()
.map(x -> x.withSuccessor(IndexedState.of(nextIndex, x.successor())))
.collect(Collectors.toUnmodifiableSet());
}
}
}
......@@ -33,7 +33,7 @@ import owl.automaton.acceptance.GeneralizedRabinAcceptance;
import owl.automaton.acceptance.OmegaAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.acceptance.RabinAcceptance;
import owl.automaton.algorithms.EmptinessCheck;
import owl.automaton.algorithms.LanguageEmptiness;
import owl.automaton.algorithms.SccDecomposition;
import owl.automaton.output.HoaPrinter;
import owl.automaton.transformations.ParityUtil;
......@@ -190,7 +190,7 @@ public final class MinimizationUtil {
}
// There are no accepting runs.
if (EmptinessCheck.isEmpty(automaton, scc.iterator().next())) {
if (LanguageEmptiness.isEmpty(automaton, scc.iterator().next())) {
logger.log(Level.FINER, "Removing scc {0}", scc);
automaton.removeStateIf(scc::contains);
// Ensure readable automaton.
......
......@@ -50,7 +50,7 @@ import owl.automaton.acceptance.CoBuchiAcceptance;
import owl.automaton.acceptance.GeneralizedBuchiAcceptance;
import owl.automaton.acceptance.OmegaAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.algorithms.EmptinessCheck;
import owl.automaton.algorithms.LanguageEmptiness;
import owl.automaton.edge.Edge;
import owl.automaton.transformations.ParityUtil;
import owl.automaton.util.AnnotatedState;
......@@ -241,12 +241,12 @@ public final class DeterministicAutomaton<S, T> {
acceptanceFlag = PARITY_MIN_EVEN;
}
if (EmptinessCheck.isEmpty(automaton)) {
if (LanguageEmptiness.isEmpty(automaton)) {
return new DeterministicAutomaton<>(automaton,
acceptanceFlag, ParityAcceptance.class, x -> false, x -> REJECTING, x -> 0d
);
} else {
assert EmptinessCheck.isEmpty(
assert LanguageEmptiness.isEmpty(
ParityUtil.complement((MutableAutomaton) automaton, MutableAutomatonUtil.Sink.INSTANCE));
return new DeterministicAutomaton<>(automaton,
acceptanceFlag, ParityAcceptance.class, x -> true, x -> ACCEPTING, x -> 1d
......
......@@ -28,7 +28,7 @@ import static owl.translations.LTL2DAFunction.Constructions.SAFETY;
import java.util.EnumSet;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import owl.automaton.algorithms.EmptinessCheck;
import owl.automaton.algorithms.LanguageEmptiness;
import owl.ltl.Disjunction;
import owl.ltl.Formula;
import owl.ltl.LabelledFormula;
......@@ -47,7 +47,7 @@ public final class LanguageAnalysis {
var labelledFormula = attachDummyAlphabet(formula);
var translation = new LTL2DAFunction(DefaultEnvironment.of(false, false), true,
EnumSet.of(SAFETY, CO_SAFETY, BUCHI, CO_BUCHI, GENERALIZED_RABIN));
return !EmptinessCheck.isEmpty(translation.apply(labelledFormula));
return !LanguageEmptiness.isEmpty(translation.apply(labelledFormula));
}
public static boolean isUnsatisfiable(Formula formula) {
......
......@@ -55,6 +55,10 @@ public final class LTL2DAFunction implements Function<LabelledFormula, Automaton
private final EnumSet<Constructions> allowedConstructions;
private final Function<LabelledFormula, ? extends Automaton<?, ?>> fallback;
public LTL2DAFunction(Environment environment) {
this(environment, false, EnumSet.allOf(Constructions.class));
}
public LTL2DAFunction(Environment environment, boolean onTheFly,
EnumSet<Constructions> allowedConstructions) {
this.allowedConstructions = EnumSet.copyOf(allowedConstructions);
......
......@@ -42,7 +42,7 @@ import owl.automaton.EdgesAutomatonMixin;
import owl.automaton.Views;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.algorithms.LanguageAnalysis;
import owl.automaton.algorithms.LanguageContainment;
import owl.automaton.edge.Edge;
import owl.factories.ValuationSetFactory;
import owl.run.modules.ImmutableTransformerParser;
......@@ -97,7 +97,7 @@ public final class NBA2DPA implements Function<Automaton<?, ?>, Automaton<?, Par
.build(new CacheLoader<>() {
@Override
public Boolean load(Map.Entry<Set<S>, S> entry) {
return LanguageAnalysis.contains(
return LanguageContainment.contains(
Views.replaceInitialState(nba, Set.of(entry.getValue())),
AutomatonUtil.cast(AutomatonOperations.union(entry.getKey().stream()
.map(x -> Views.replaceInitialState(nba, Set.of(x)))
......
......@@ -31,7 +31,7 @@ import owl.ltl.parser.LtlParser;
import owl.run.DefaultEnvironment;
import owl.translations.LTL2DAFunction;
class LanguageAnalysisTest {
class LanguageContainmentTest {
@Test
void contains() {
......@@ -48,13 +48,13 @@ class LanguageAnalysisTest {
var infOftComplex
= AutomatonUtil.cast(translation.apply(formula3), Object.class, BuchiAcceptance.class);
assertTrue(LanguageAnalysis.contains(infOftAandB, infOftA));
assertFalse(LanguageAnalysis.contains(infOftA, infOftAandB));
assertTrue(LanguageContainment.contains(infOftAandB, infOftA));
assertFalse(LanguageContainment.contains(infOftA, infOftAandB));
assertTrue(LanguageAnalysis.contains(infOftComplex, infOftA));
assertFalse(LanguageAnalysis.contains(infOftA, infOftComplex));
assertTrue(LanguageContainment.contains(infOftComplex, infOftA));
assertFalse(LanguageContainment.contains(infOftA, infOftComplex));
assertTrue(LanguageAnalysis.contains(infOftAandB, infOftComplex));
assertFalse(LanguageAnalysis.contains(infOftComplex, infOftAandB));
assertTrue(LanguageContainment.contains(infOftAandB, infOftComplex));
assertFalse(LanguageContainment.contains(infOftComplex, infOftAandB));
}
}
/*
* Copyright (C) 2016 - 2018 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program 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 General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.automaton.algorithms;
import static org.junit.jupiter.api.Assertions.assertFalse;
import static org.junit.jupiter.api.Assertions.assertTrue;
import de.tum.in.naturals.bitset.BitSets;
import java.util.BitSet;
import java.util.EnumSet;
import java.util.List;
import java.util.function.Function;
import org.junit.jupiter.api.Test;
import owl.automaton.Automaton;
import owl.automaton.UltimatelyPeriodicWord;
import owl.ltl.LabelledFormula;
import owl.ltl.parser.LtlParser;
import owl.run.DefaultEnvironment;
import owl.translations.LTL2DAFunction;
import owl.translations.LTL2NAFunction;
class LanguageMembershipTest {
private static final Function<LabelledFormula, Automaton<?, ?>> deterministicTranslation
= new LTL2DAFunction(DefaultEnvironment.standard(), false, EnumSet.of(
LTL2DAFunction.Constructions.SAFETY,
LTL2DAFunction.Constructions.CO_SAFETY,
LTL2DAFunction.Constructions.BUCHI,
LTL2DAFunction.Constructions.CO_BUCHI,
LTL2DAFunction.Constructions.PARITY,
LTL2DAFunction.Constructions.RABIN));
private static final Function<LabelledFormula, Automaton<?, ?>> nondeterministicTranslation
= new LTL2NAFunction(DefaultEnvironment.standard());
@Test
void containsDeterministic() {
var automaton = deterministicTranslation.apply(LtlParser.parse("F G a | G F b | X X c"));
var wordA = new UltimatelyPeriodicWord(List.of(new BitSet()), List.of(BitSets.of(0)));
var wordAandB = new UltimatelyPeriodicWord(List.of(), List.of(BitSets.of(0), BitSets.of(1)));
var wordC = new UltimatelyPeriodicWord(List.of(), List.of(BitSets.of(2)));
var wordEmpty = new UltimatelyPeriodicWord(List.of(), List.of(new BitSet()));
assertTrue(LanguageMembership.contains(automaton, wordA));
assertTrue(LanguageMembership.contains(automaton, wordAandB));
assertTrue(LanguageMembership.contains(automaton, wordC));
assertFalse(LanguageMembership.contains(automaton, wordEmpty));
}
@Test
void containsNondeterministic() {
var automaton = nondeterministicTranslation.apply(LtlParser.parse("F G a | G F b | X X c"));
var wordA = new UltimatelyPeriodicWord(List.of(new BitSet()), List.of(BitSets.of(0)));
var wordAandB = new UltimatelyPeriodicWord(List.of(), List.of(BitSets.of(0), BitSets.of(1)));
var wordC = new UltimatelyPeriodicWord(List.of(), List.of(BitSets.of(2)));
var wordEmpty = new UltimatelyPeriodicWord(List.of(), List.of(new BitSet()));
assertTrue(LanguageMembership.contains(automaton, wordA));
assertTrue(LanguageMembership.contains(automaton, wordAandB));
assertTrue(LanguageMembership.contains(automaton, wordC));
assertFalse(LanguageMembership.contains(automaton, wordEmpty));
}
}
\ No newline at end of file
......@@ -24,7 +24,7 @@ import static org.junit.jupiter.api.Assertions.assertTrue;
import org.junit.jupiter.api.Test;
import owl.ltl.parser.LtlParser;
class LanguageAnalysisTest {
class LanguageContainmentTest {
@Test
void isSatisfiable() {
......
......@@ -29,7 +29,7 @@ import java.util.EnumSet;
import java.util.Map;
import org.junit.jupiter.api.Test;
import owl.automaton.Automaton;
import owl.automaton.algorithms.EmptinessCheck;
import owl.automaton.algorithms.LanguageEmptiness;
import owl.automaton.edge.Edge;
import owl.ltl.EquivalenceClass;
import owl.ltl.parser.LtlParser;
......@@ -55,8 +55,8 @@ class LTL2DAModuleFunctionTest {
var complementAutomaton = translator.apply(formula.not());
assertEquals(automaton.size(), complementAutomaton.size());
assertFalse(EmptinessCheck.isEmpty(automaton));
assertFalse(EmptinessCheck.isEmpty(complementAutomaton));
assertFalse(LanguageEmptiness.isEmpty(automaton));
assertFalse(LanguageEmptiness.isEmpty(complementAutomaton));
}
@Test
......
......@@ -29,7 +29,7 @@ import owl.automaton.AutomatonReader;
import owl.automaton.AutomatonUtil;
import owl.automaton.Views;
import owl.automaton.acceptance.GeneralizedBuchiAcceptance;
import owl.automaton.algorithms.EmptinessCheck;
import owl.automaton.algorithms.LanguageEmptiness;
import owl.automaton.output.HoaPrinter;
import owl.run.DefaultEnvironment;
......@@ -106,10 +106,10 @@ class TestHasAcceptingRun {
var dpa = new NBA2DPA().apply(nba);
HoaPrinter.feedTo(dpa, new HOAIntermediateCheckValidity(new HOAConsumerNull()));
assertEquals(EmptinessCheck.isEmpty(dpa), !hasAcceptingRun);
assertEquals(LanguageEmptiness.isEmpty(dpa), !hasAcceptingRun);
var complement = Views.complement(AutomatonUtil.cast(dpa), new Object());
HoaPrinter.feedTo(complement, new HOAIntermediateCheckValidity(new HOAConsumerNull()));
assertEquals(EmptinessCheck.isEmpty(complement), !complementHasAcceptingRun);
assertEquals(LanguageEmptiness.isEmpty(complement), !complementHasAcceptingRun);
}
}