closure? (3b197c42) · Commits · i7 / owl

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

+12 −1

Original line number	Diff line number	Diff line
		@@ -61,6 +61,7 @@ import owl.ltl.Disjunction;
		import owl.ltl.EquivalenceClass;
		import owl.ltl.FOperator;
		import owl.ltl.Formula;
		import owl.ltl.Formulas;
		import owl.ltl.GOperator;
		import owl.ltl.LabelledFormula;
		import owl.ltl.MOperator;
		@@ -513,6 +514,7 @@ public final class DeterministicAutomaton<S, T> {
		}
		}

		indices.sort(Formulas::compare);
		return new AutoValue_DeterministicAutomaton_NormalFormDecomposition(
		type, List.copyOf(indices), smallerClasses);
		}
		@@ -564,7 +566,16 @@ public final class DeterministicAutomaton<S, T> {
		List<Boolean> decomposedState = new ArrayList<>();

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

		if (type() == NormalFormType.DNF) {
		contained = normalform.stream().anyMatch(x -> x.containsAll(index));
		} else {
		assert type() == NormalFormType.CNF;
		contained = normalform.stream().anyMatch(index::containsAll);
		}

		decomposedState.add(contained);
		}

		return decomposedState;

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

+15 −10

Original line number	Diff line number	Diff line
		@@ -24,6 +24,7 @@ import static org.junit.jupiter.api.Assertions.assertEquals;
		import static org.junit.jupiter.api.Assertions.assertTimeout;

		import java.time.Duration;
		import java.util.Arrays;
		import java.util.List;
		import org.junit.jupiter.api.Test;
		import owl.ltl.parser.LtlParser;
		@@ -120,8 +121,8 @@ class DeterministicAutomatonTest {

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

		@SuppressWarnings("PMD")
		@@ -138,10 +139,10 @@ class DeterministicAutomatonTest {

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

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

		@SuppressWarnings("PMD")
		@@ -198,9 +199,13 @@ class DeterministicAutomatonTest {
		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));
		System.out.println(Arrays.toString(automaton.decompose(0)));
		System.out.println(Arrays.toString(automaton.decompose(1)));
		System.out.println(Arrays.toString(automaton.decompose(2)));
		System.out.println(Arrays.toString(automaton.decompose(3)));

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

Admin message