add dnf/cnf encoding. (ef604d1d) · Commits · i7 / owl

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

+64 −31

Original line number	Diff line number	Diff line
		@@ -27,6 +27,7 @@ import static owl.cinterface.Acceptance.PARITY_MIN_ODD;
		import static owl.cinterface.Acceptance.SAFETY;
		import static owl.translations.ltl2dpa.LTL2DPAFunction.Configuration.COMPLEMENT_CONSTRUCTION_HEURISTIC;

		import com.google.auto.value.AutoValue;
		import com.google.common.collect.Iterables;
		import it.unimi.dsi.fastutil.ints.IntArrayList;
		import it.unimi.dsi.fastutil.objects.Object2IntMap;
		@@ -63,8 +64,8 @@ import owl.ltl.SyntacticFragments;
		import owl.ltl.XOperator;
		import owl.ltl.rewriter.NormalForms;
		import owl.run.Environment;
		import owl.translations.canonical.DeterministicConstructionsPortfolio;
		import owl.translations.canonical.BreakpointState;
		import owl.translations.canonical.DeterministicConstructionsPortfolio;
		import owl.translations.canonical.GenericConstructions;
		import owl.translations.ltl2dpa.AsymmetricRankingState;
		import owl.translations.ltl2dpa.LTL2DPAFunction;
		@@ -291,7 +292,8 @@ public final class DeterministicAutomaton<S, T> {
		allClasses.add((EquivalenceClass) decomposer.apply(x).get(i));
		}

		stateComponent2indexMap.add(decomposeInit(allClasses));
		stateComponent2indexMap.add(
		NormalFormDecomposition.of((EquivalenceClass) object, allClasses));
		} else if (object instanceof Integer) {
		stateComponent2indexMap.add(null);
		} else {
		@@ -306,14 +308,18 @@ public final class DeterministicAutomaton<S, T> {
		@CEntryPoint
		public String describeDecompose() {
		decomposeInit();
		assert stateComponent2indexMap != null;

		StringBuilder stringBuilder = new StringBuilder();

		int index = 0;

		for (Object foo : stateComponent2indexMap) {
		if (foo instanceof List) {
		for (var clause : (List) foo) {
		if (foo instanceof NormalFormDecomposition) {
		stringBuilder.append(String.format("-: %s decomposition\n",
		((NormalFormDecomposition) foo).type()));

		for (var clause : ((NormalFormDecomposition) foo).decomposition()) {
		stringBuilder.append(String.format("%d: %s\n", index, clause.toString()));
		index++;
		}
		@@ -332,6 +338,7 @@ public final class DeterministicAutomaton<S, T> {
		@CEntryPoint
		public int[] decompose(int stateIndex) {
		decomposeInit();
		assert stateComponent2indexMap != null;

		S state = index2StateMap.get(stateIndex);
		var decomposedState = decomposer.apply(state);
		@@ -339,12 +346,12 @@ public final class DeterministicAutomaton<S, T> {

		for (int i = 0; i < decomposedState.size(); i++) {
		var component = decomposedState.get(i);

		var helper = stateComponent2indexMap.get(i);

		if (helper instanceof List) {
		if (helper instanceof NormalFormDecomposition) {
		var clazz = (EquivalenceClass) component;
		decompose((List) helper, clazz).forEach(x -> indexList.add(((Boolean) x) ? 1 : 0));
		var decomposition = (NormalFormDecomposition) helper;
		decomposition.decompose(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());
		@@ -358,31 +365,7 @@ public final class DeterministicAutomaton<S, T> {
		return indexList.toIntArray();
		}

		private List<Set<Formula>> decomposeInit(Set<EquivalenceClass> classes) {
		Set<Set<Formula>> seenElements = new HashSet<>();
		List<Set<Formula>> indices = new ArrayList<>();

		for (var clazz : classes) {
		for (var clause : NormalForms.toDnf(clazz.representative())) {
		if (seenElements.add(clause)) {
		indices.add(clause);
		}
		}
		}

		return indices;
		}

		private List<Boolean> decompose(List<Set<Formula>> indices, EquivalenceClass clazz) {
		var dnf = NormalForms.toDnf(clazz.representative());
		List<Boolean> decomposedState = new ArrayList<>();

		for (var index : indices) {
		decomposedState.add(dnf.contains(index));
		}

		return decomposedState;
		}

		@CEntryPoint
		public int[] edges(int stateIndex) {
		@@ -470,4 +453,54 @@ public final class DeterministicAutomaton<S, T> {
		cache.put(tree, index);
		return index;
		}

		@AutoValue
		abstract static class NormalFormDecomposition {

		abstract NormalFormType type();

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

		static NormalFormDecomposition of(EquivalenceClass initialState,
		Set<EquivalenceClass> classes) {
		var type = initialState.representative() instanceof Conjunction
		? NormalFormType.CNF
		: NormalFormType.DNF;

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

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

		if (seenElements.add(clause)) {
		indices.add(clause);
		}
		}
		}

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

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

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

		for (var index : decomposition()) {
		decomposedState.add(normalform.contains(index));
		}

		return decomposedState;
		}
		}

		enum NormalFormType {
		CNF, DNF
		}
		}

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

+6 −5

Original line number	Diff line number	Diff line
		@@ -118,10 +118,10 @@ class DeterministicAutomatonTest {

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

		assertArrayEquals(new int[]{0, 0, 0, 1, 1, 0, 0}, automaton.decompose(0));
		assertArrayEquals(new int[]{0, 0, 0, 0, 0, 1, 1}, automaton.decompose(1));
		assertArrayEquals(new int[]{0, 0, 1, 0, 0, 0, 0}, automaton.decompose(2));
		assertArrayEquals(new int[]{1, 1, 0, 0, 0, 0, 0}, automaton.decompose(3));
		assertArrayEquals(new int[]{1, 0, 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));
		}

		@SuppressWarnings("PMD")
		@@ -165,7 +165,8 @@ class DeterministicAutomatonTest {
		@SuppressWarnings("PMD")
		@Test
		void testDecomposeCoSafetyRegression() {
		var automaton = DeterministicAutomaton.of(LtlParser.parse("F (a & b & X (a & X a) & X (b & X b))"));
		var automaton = DeterministicAutomaton.of(
		LtlParser.parse("F (a & b & X (a & X a) & X (b & X b))"));

		assertEquals(4, automaton.size());