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

...
 
Commits (2)
......@@ -18,19 +18,6 @@ namespace owl {
return copy_from_java(env, java_tree);
}
void OwlThread::clearAutomatonCache() const {
jclass clazz = lookup_class(env, "owl/cinterface/DecomposedDPA");
jmethodID clear_cache_method = get_static_methodID(env, clazz, "clearCache", "()V");
env->CallStaticVoidMethod(clazz, clear_cache_method);
if(env->ExceptionCheck()) {
env->ExceptionDescribe();
env->ExceptionClear();
}
deref(env, clazz);
}
Formula OwlThread::adoptFormula(const Formula &formula) const {
return Formula(env, ref(env, formula.handle));
}
......
......@@ -35,7 +35,6 @@ namespace owl {
FormulaFactory createFormulaFactory() const;
DecomposedDPA createAutomaton(const Formula &formula, bool simplify, bool monolithic, int firstOutputVariable) const;
void clearAutomatonCache() const;
};
class OwlJavaVM {
......
......@@ -61,8 +61,6 @@ import owl.util.annotation.CEntryPoint;
// This is a JNI entry point. No touching.
public final class DecomposedDPA {
public static final AutomatonRepository cache = new AutomatonRepository();
public final LabelledTree<Tag, Reference> structure;
private final List<Reference> leaves;
public final List<DeterministicAutomaton<?, ?>> automata;
......@@ -95,16 +93,10 @@ public final class DecomposedDPA {
Builder builder = new Builder(processedFormula.accept(Annotator.INSTANCE));
LabelledTree<Tag, Reference> structure1 = monolithic
? Builder.createLeaf(processedFormula)
? builder.createLeaf(processedFormula)
: processedFormula.accept(builder);
return new DecomposedDPA(structure1, List.copyOf(cache.automata));
}
@CEntryPoint
public static void clearCache() {
cache.automata.clear();
cache.lookup.clear();
return new DecomposedDPA(structure1, List.copyOf(builder.automata));
}
@CEntryPoint
......@@ -151,16 +143,42 @@ public final class DecomposedDPA {
BICONDITIONAL, CONJUNCTION, DISJUNCTION
}
static final class AutomatonRepository {
public static final class Reference {
public final Formula formula;
public final int index;
public final ImmutableIntArray alphabetMapping;
Reference(Formula formula, int index, ImmutableIntArray alphabetMapping) {
this.formula = formula;
this.index = index;
this.alphabetMapping = alphabetMapping;
}
Reference(Formula formula, int index, int[] alphabetMapping) {
this(formula, index, ImmutableIntArray.copyOf(alphabetMapping));
}
@CEntryPoint
public int[] alphabetMapping() {
return alphabetMapping.toArray();
}
}
static final class Builder extends PropositionalVisitor<LabelledTree<Tag, Reference>> {
private final Map<Formula, Acceptance> annotatedTree;
private final List<DeterministicAutomaton<?, ?>> automata = new ArrayList<>();
private final Map<Formula, Reference> lookup = new HashMap<>();
private Reference get(Formula formula) {
Builder(Map<Formula, Acceptance> annotatedTree) {
this.annotatedTree = new HashMap<>(annotatedTree);
}
private LabelledTree<Tag, Reference> createLeaf(Formula formula) {
assert SyntacticFragment.NNF.contains(formula);
Reference reference = lookup.get(formula);
if (reference != null) {
return reference;
return new LabelledTree.Leaf<>(reference);
}
for (Map.Entry<Formula, Reference> entry : lookup.entrySet()) {
......@@ -181,7 +199,7 @@ public final class DecomposedDPA {
}
}
return new Reference(formula, reference.index, newMapping);
return new LabelledTree.Leaf<>(new Reference(formula, reference.index, newMapping));
}
}
......@@ -189,40 +207,7 @@ public final class DecomposedDPA {
Reference newReference = new Reference(formula, automata.size(), shiftedFormula.mapping);
automata.add(DeterministicAutomaton.of(Hacks.attachDummyAlphabet(shiftedFormula.formula)));
lookup.put(formula, newReference);
return newReference;
}
}
public static final class Reference {
public final Formula formula;
public final int index;
public final ImmutableIntArray alphabetMapping;
Reference(Formula formula, int index, ImmutableIntArray alphabetMapping) {
this.formula = formula;
this.index = index;
this.alphabetMapping = alphabetMapping;
}
Reference(Formula formula, int index, int[] alphabetMapping) {
this(formula, index, ImmutableIntArray.copyOf(alphabetMapping));
}
@CEntryPoint
public int[] alphabetMapping() {
return alphabetMapping.toArray();
}
}
static final class Builder extends PropositionalVisitor<LabelledTree<Tag, Reference>> {
private final Map<Formula, Acceptance> annotatedTree;
Builder(Map<Formula, Acceptance> annotatedTree) {
this.annotatedTree = new HashMap<>(annotatedTree);
}
private static LabelledTree<Tag, Reference> createLeaf(Formula formula) {
return new LabelledTree.Leaf<>(cache.get(formula));
return new LabelledTree.Leaf<>(newReference);
}
private List<LabelledTree<Tag, Reference>> createLeaves(PropositionalFormula formula) {
......
......@@ -30,8 +30,6 @@ import static owl.util.Assertions.assertThat;
import com.google.common.primitives.ImmutableIntArray;
import java.util.Collections;
import java.util.List;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;
import owl.collections.LabelledTree.Node;
import owl.ltl.Formula;
......@@ -109,16 +107,6 @@ class DecomposedDPATest {
+ " }\n"
+ "}";
@BeforeEach
void setUp() {
DecomposedDPA.clearCache();
}
@AfterEach()
void tearDown() {
DecomposedDPA.clearCache();
}
@Test
void splitSimpleArbiter() {
of(LtlParser.syntax(SIMPLE_ARBITER), true, false, 0);
......@@ -449,8 +437,6 @@ class DecomposedDPATest {
() -> assertEquals(2, automaton1.size())
);
DecomposedDPA.clearCache();
var automaton2 = of(formula, true, false, 1)
.automata.get(0);
......@@ -460,8 +446,6 @@ class DecomposedDPATest {
() -> assertArrayEquals(new int[]{4, 0, 0, -2, 0, -1, 0, 0}, automaton2.edges(0))
);
DecomposedDPA.clearCache();
var automaton3 = of(formula, true, false, 2)
.automata.get(0);
......