evil hacks. (ba62b8d3) · Commits · i7 / owl

src/main/java/owl/cinterface/DeterministicAutomaton.java

+82 −11

Original line number	Diff line number	Diff line
		@@ -33,6 +33,7 @@ import it.unimi.dsi.fastutil.ints.IntArrayList;
		import it.unimi.dsi.fastutil.objects.Object2IntMap;
		import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap;
		import java.util.ArrayList;
		import java.util.BitSet;
		import java.util.EnumSet;
		import java.util.HashMap;
		import java.util.HashSet;
		@@ -58,13 +59,20 @@ import owl.ltl.BooleanConstant;
		import owl.ltl.Conjunction;
		import owl.ltl.Disjunction;
		import owl.ltl.EquivalenceClass;
		import owl.ltl.FOperator;
		import owl.ltl.Formula;
		import owl.ltl.GOperator;
		import owl.ltl.LabelledFormula;
		import owl.ltl.MOperator;
		import owl.ltl.ROperator;
		import owl.ltl.SyntacticFragments;
		import owl.ltl.UOperator;
		import owl.ltl.WOperator;
		import owl.ltl.XOperator;
		import owl.ltl.rewriter.NormalForms;
		import owl.run.Environment;
		import owl.translations.canonical.BreakpointState;
		import owl.translations.canonical.DeterministicConstructions;
		import owl.translations.canonical.DeterministicConstructionsPortfolio;
		import owl.translations.canonical.GenericConstructions;
		import owl.translations.ltl2dpa.AsymmetricRankingState;
		@@ -286,14 +294,23 @@ public final class DeterministicAutomaton<S, T> {
		var object = decomposedInitialState.get(i);

		if (object instanceof EquivalenceClass) {
		var initialClazz = (EquivalenceClass) object;
		Set<EquivalenceClass> allClasses = new HashSet<>();

		Map<EquivalenceClass, EquivalenceClass> preMap = Map.of();

		if (automaton instanceof DeterministicConstructions.Base) {
		preMap = ((DeterministicConstructions.Base<S, ?>) automaton).unfoldPre();
		}

		for (S x : index2StateMap) {
		allClasses.add((EquivalenceClass) decomposer.apply(x).get(i));
		var clazz = (EquivalenceClass) decomposer.apply(x).get(i);
		allClasses.add(preMap.getOrDefault(clazz, clazz));
		}

		stateComponent2indexMap.add(
		NormalFormDecomposition.of((EquivalenceClass) object, allClasses));
		NormalFormDecomposition.of(
		preMap.getOrDefault(initialClazz, initialClazz), allClasses));
		} else if (object instanceof Integer) {
		stateComponent2indexMap.add(null);
		} else {
		@@ -351,7 +368,15 @@ public final class DeterministicAutomaton<S, T> {
		if (helper instanceof NormalFormDecomposition) {
		var clazz = (EquivalenceClass) component;
		var decomposition = (NormalFormDecomposition) helper;
		decomposition.decompose(clazz).forEach(x -> indexList.add(x ? 1 : 0));

		Map<EquivalenceClass, EquivalenceClass> preMap = Map.of();

		if (automaton instanceof DeterministicConstructions.Base) {
		preMap = ((DeterministicConstructions.Base<S, ?>) automaton).unfoldPre();
		}

		decomposition.decompose(preMap.getOrDefault(clazz, clazz))
		.forEach(x -> indexList.add(x ? 1 : 0));
		} else if (helper instanceof Map) {
		Map<Object, Integer> map = ((Object2IntOpenHashMap) helper);
		int index = map.computeIfAbsent(component, (x) -> map.size());
		@@ -461,19 +486,26 @@ public final class DeterministicAutomaton<S, T> {

		abstract List<Set<Formula>> decomposition();

		abstract Map<EquivalenceClass, EquivalenceClass> smallerCache();

		static NormalFormDecomposition of(EquivalenceClass initialState,
		Set<EquivalenceClass> classes) {
		var type = initialState.representative() instanceof Conjunction
		? NormalFormType.CNF
		: NormalFormType.DNF;
		Map<EquivalenceClass, EquivalenceClass> smallerClasses = new HashMap<>();
		var initialStateSmall = smallerClasses.computeIfAbsent(
		initialState, NormalFormDecomposition::smaller);

		var type = determine(initialStateSmall.representative());

		Set<Set<Formula>> seenElements = new HashSet<>();
		List<Set<Formula>> indices = new ArrayList<>();

		for (var clazz : classes) {
		var smallerClazz = smallerClasses.computeIfAbsent(
		clazz, NormalFormDecomposition::smaller);

		for (var clause : type == NormalFormType.DNF
		? NormalForms.toDnf(clazz.representative())
		: NormalForms.toCnf(clazz.representative())) {
		? NormalForms.toDnf(smallerClazz.representative())
		: NormalForms.toCnf(smallerClazz.representative())) {

		if (seenElements.add(clause)) {
		indices.add(clause);
		@@ -482,13 +514,52 @@ public final class DeterministicAutomaton<S, T> {
		}

		return new AutoValue_DeterministicAutomaton_NormalFormDecomposition(
		type, List.copyOf(indices));
		type, List.copyOf(indices), smallerClasses);
		}

		static NormalFormType determine(Formula formula) {
		if (formula instanceof XOperator) {
		return determine(((XOperator) formula).operand);
		}

		if (formula instanceof GOperator
		\|\| formula instanceof ROperator
		\|\| formula instanceof MOperator
		\|\| formula instanceof Conjunction) {
		return NormalFormType.CNF;
		}

		if (formula instanceof FOperator
		\|\| formula instanceof UOperator
		\|\| formula instanceof WOperator
		\|\| formula instanceof Disjunction) {
		return NormalFormType.DNF;
		}

		return NormalFormType.DNF;
		}

		static EquivalenceClass smaller(EquivalenceClass clazz) {
		for (var smallerClazz : clazz.substitute(x -> {
		if (x instanceof XOperator) {
		return XOperator.of(x);
		}

		return x;
		}).temporalStepTree().values()) {
		if (smallerClazz.unfold().equals(clazz)) {
		return smallerClazz;
		}
		}

		return clazz;
		}

		private List<Boolean> decompose(EquivalenceClass clazz) {
		var smallerClazz = smallerCache().get(clazz);
		var normalform = type() == NormalFormType.DNF
		? NormalForms.toDnf(clazz.representative())
		: NormalForms.toCnf(clazz.representative());
		? NormalForms.toDnf(smallerClazz.representative())
		: NormalForms.toCnf(smallerClazz.representative());

		List<Boolean> decomposedState = new ArrayList<>();

src/main/java/owl/translations/canonical/DeterministicConstructions.java

+19 −3

Original line number	Diff line number	Diff line
		@@ -24,8 +24,11 @@ import static owl.collections.ValuationTrees.cartesianProduct;
		import com.google.common.base.Preconditions;
		import java.util.ArrayList;
		import java.util.BitSet;
		import java.util.Collections;
		import java.util.Comparator;
		import java.util.HashMap;
		import java.util.List;
		import java.util.Map;
		import java.util.Set;
		import java.util.function.Function;
		import java.util.stream.Collectors;
		@@ -62,7 +65,7 @@ public final class DeterministicConstructions {
		private DeterministicConstructions() {
		}

		abstract static class Base<S, A extends OmegaAcceptance>
		public abstract static class Base<S, A extends OmegaAcceptance>
		extends AbstractCachedStatesAutomaton<S, A>
		implements EdgeTreeAutomatonMixin<S, A> {

		@@ -113,6 +116,7 @@ public final class DeterministicConstructions {
		}

		EquivalenceClass initialStateInternal(EquivalenceClass clazz) {
		pre.putIfAbsent(clazz.unfold(), clazz);
		return eagerUnfold ? clazz.unfold() : clazz;
		}

		@@ -131,9 +135,18 @@ public final class DeterministicConstructions {
		<T> ValuationTree<T> successorTreeInternal(EquivalenceClass clazz,
		Function<EquivalenceClass, Set<T>> edgeFunction) {
		return eagerUnfold
		? clazz.temporalStepTree(x -> edgeFunction.apply(x.unfold()))
		? clazz.temporalStepTree(x -> {
		pre.putIfAbsent(x.unfold(), x);
		return edgeFunction.apply(x.unfold());
		})
		: clazz.unfold().temporalStepTree(edgeFunction);
		}

		Map<EquivalenceClass, EquivalenceClass> pre = new HashMap<>();

		public Map<EquivalenceClass, EquivalenceClass> unfoldPre() {
		return Collections.unmodifiableMap(pre);
		}
		}

		private abstract static class Terminal<A extends OmegaAcceptance>
		@@ -141,7 +154,10 @@ public final class DeterministicConstructions {
		private final EquivalenceClass initialState;

		private final Function<EquivalenceClass, Set<Edge<EquivalenceClass>>>
		edgeMapper = x -> Collections3.ofNullable(this.buildEdge(x.unfold()));
		edgeMapper = x -> {
		pre.putIfAbsent(x.unfold(), x);
		return Collections3.ofNullable(this.buildEdge(x.unfold()));
		};

		private Terminal(Factories factories, boolean eagerUnfold, Formula formula) {
		super(factories, eagerUnfold);

src/test/java/owl/cinterface/DeterministicAutomatonTest.java

+26 −3

Original line number	Diff line number	Diff line
		@@ -100,8 +100,8 @@ class DeterministicAutomatonTest {
		System.out.println(automaton.describeDecompose());

		assertArrayEquals(new int[]{1, 1}, automaton.decompose(0));
		assertArrayEquals(new int[]{1, 0}, automaton.decompose(1));
		assertArrayEquals(new int[]{0, 1}, automaton.decompose(2));
		assertArrayEquals(new int[]{0, 1}, automaton.decompose(1));
		assertArrayEquals(new int[]{1, 0}, automaton.decompose(2));
		}

		@SuppressWarnings("PMD")
		@@ -118,7 +118,7 @@ class DeterministicAutomatonTest {

		System.out.println(automaton.describeDecompose());

		assertArrayEquals(new int[]{1, 0, 1}, automaton.decompose(0));
		assertArrayEquals(new int[]{0, 1, 1}, automaton.decompose(0));
		assertArrayEquals(new int[]{1, 1, 0}, automaton.decompose(1));
		assertArrayEquals(new int[]{0, 1, 0}, automaton.decompose(2));
		assertArrayEquals(new int[]{1, 0, 0}, automaton.decompose(3));
		@@ -180,4 +180,27 @@ class DeterministicAutomatonTest {
		assertArrayEquals(new int[]{1, 0, 1, 1}, automaton.decompose(1));
		assertArrayEquals(new int[]{1, 1, 0, 0}, automaton.decompose(2));
		}

		@SuppressWarnings("PMD")
		@Test
		void testDecomposeCoSafetyRegression2() {
		var automaton = DeterministicAutomaton.of(
		LtlParser.parse("((a U b) U c) U d"));

		assertEquals(8, automaton.size());

		automaton.edges(0);
		automaton.edges(1);
		automaton.edges(2);
		automaton.edges(3);
		automaton.edges(4);
		automaton.edges(5);
		automaton.edges(6);

		System.out.println(automaton.describeDecompose());

		assertArrayEquals(new int[]{1, 0, 1, 0}, automaton.decompose(0));
		assertArrayEquals(new int[]{1, 0, 1, 1}, automaton.decompose(1));
		assertArrayEquals(new int[]{1, 1, 0, 0}, automaton.decompose(2));
		}
		}

Admin message