Restructure C-API and add a transition relation filtering mechanism to DecomposedDPA

parent 0690af57
......@@ -60,6 +60,7 @@ tasks.withType(Javadoc) {
def disablePandoc = project.hasProperty("disable-pandoc")
def disableNative = project.hasProperty("disable-native")
def enableNativeAssertions = project.hasProperty("enable-native-assertions")
apply from: 'gradle/analysis.gradle'
apply from: 'gradle/antlr.gradle'
......@@ -260,6 +261,7 @@ task buildCLibrary(type: Exec, dependsOn: [classes]) {
commandLine command,
"owl.cinterface.CInterface", "libowl",
"-cp", sourceSets.main.runtimeClasspath.asPath,
enableNativeAssertions ? '-ea' : '-da',
"-DowlHeader=${projectDir}/src/main/headers",
'--shared',
'--initialize-at-build-time=owl,it,com,org,jhoafparser',
......
......@@ -19,7 +19,7 @@ typedef enum {
CONSTANT_FALSE,
USED,
UNUSED
} variable_status_t;
} atomic_proposition_status_t;
typedef enum {
BUCHI,
......@@ -36,15 +36,13 @@ typedef enum {
} acceptance_t;
typedef struct {
int *buffer;
int capacity;
int position;
} int_buffer_t;
int *elements;
int length;
} sized_int_array_t;
typedef struct {
double *buffer;
int capacity;
int position;
} double_buffer_t;
double *elements;
int length;
} sized_double_array_t;
#endif
/*
* Copyright (C) 2016 - 2019 (See AUTHORS)
* Copyright (C) 2016 - 2020 (See AUTHORS)
*
* This file is part of Owl.
*
......@@ -190,14 +190,14 @@ public interface Automaton<S, A extends OmegaAcceptance> {
case EDGES:
var edges = new HashSet<Edge<S>>();
for (BitSet valuation : BitSets.powerSet(factory().alphabet().size())) {
for (BitSet valuation : BitSets.powerSet(factory().atomicPropositions().size())) {
edges.addAll(edges(state, valuation));
}
return edges;
case EDGE_TREE:
return edgeTree(state).values();
return edgeTree(state).flatValues();
case EDGE_MAP:
return edgeMap(state).keySet();
......
/*
* Copyright (C) 2016 - 2019 (See AUTHORS)
* Copyright (C) 2016 - 2020 (See AUTHORS)
*
* This file is part of Owl.
*
......@@ -154,7 +154,7 @@ public final class AutomatonUtil {
break;
case EDGE_TREE:
automaton.accept((Automaton.EdgeTreeVisitor<S>) (state, tree) -> tree.values().forEach(
automaton.accept((Automaton.EdgeTreeVisitor<S>) (state, tree) -> tree.flatValues().forEach(
edge -> edge.acceptanceSetIterator().forEachRemaining((IntConsumer) indices::set)));
break;
......
......@@ -20,6 +20,7 @@
package owl.automaton;
import static com.google.common.base.Preconditions.checkArgument;
import static owl.automaton.Automaton.Property.COMPLETE;
import static owl.automaton.Automaton.Property.DETERMINISTIC;
import static owl.automaton.acceptance.OmegaAcceptanceCast.isInstanceOf;
......@@ -121,7 +122,7 @@ public final class BooleanOperations {
Class<A> expectedAcceptance) {
var completeAutomaton = trapState == null ? automaton : Views.complete(automaton, trapState);
checkArgument(completeAutomaton.is(Automaton.Property.COMPLETE), "Automaton is not complete.");
checkArgument(completeAutomaton.is(COMPLETE), "Automaton is not complete.");
checkArgument(!completeAutomaton.initialStates().isEmpty(), "Automaton is empty.");
// Check is too costly.
// checkArgument(completeAutomaton.is(DETERMINISTIC), "Automaton is not deterministic.");
......@@ -246,9 +247,13 @@ public final class BooleanOperations {
throw new IllegalArgumentException("Symbolic factories are incompatible.");
}
if (Collections.indexOfSubList(otherFactory.alphabet(), factory.alphabet()) == 0) {
if (Collections.indexOfSubList(
otherFactory.atomicPropositions(),
factory.atomicPropositions()) == 0) {
factory = otherFactory;
} else if (Collections.indexOfSubList(factory.alphabet(), otherFactory.alphabet()) != 0) {
} else if (Collections.indexOfSubList(
factory.atomicPropositions(),
otherFactory.atomicPropositions()) != 0) {
throw new IllegalArgumentException("Could not find shared alphabet.");
}
}
......@@ -653,5 +658,30 @@ public final class BooleanOperations {
public Set<S> states() {
return backingAutomaton.states();
}
@Override
public void accept(EdgeVisitor<S> visitor) {
backingAutomaton.accept(visitor);
}
@Override
public void accept(EdgeMapVisitor<S> visitor) {
backingAutomaton.accept(visitor);
}
@Override
public void accept(EdgeTreeVisitor<S> visitor) {
backingAutomaton.accept(visitor);
}
@Override
public void accept(Visitor<S> visitor) {
backingAutomaton.accept(visitor);
}
@Override
public boolean is(Property property) {
return backingAutomaton.is(property);
}
}
}
/*
* Copyright (C) 2016 - 2019 (See AUTHORS)
* Copyright (C) 2016 - 2020 (See AUTHORS)
*
* This file is part of Owl.
*
......@@ -35,7 +35,7 @@ final class DefaultImplementations {
static <S> Set<S> visit(Automaton<S, ?> automaton, Automaton.EdgeVisitor<S> visitor) {
Set<S> exploredStates = new HashSet<>(automaton.initialStates());
Deque<S> workQueue = new ArrayDeque<>(exploredStates);
Set<BitSet> powerSet = BitSets.powerSet(automaton.factory().alphabet().size());
Set<BitSet> powerSet = BitSets.powerSet(automaton.factory().atomicPropositions().size());
while (!workQueue.isEmpty()) {
S state = workQueue.remove();
......@@ -91,7 +91,7 @@ final class DefaultImplementations {
S state = workQueue.remove();
var edges = automaton.edgeTree(state);
edges.values().forEach((edge) -> {
edges.flatValues().forEach((edge) -> {
S successor = edge.successor();
if (exploredStates.add(successor)) {
......
/*
* Copyright (C) 2016 - 2019 (See AUTHORS)
* Copyright (C) 2016 - 2020 (See AUTHORS)
*
* This file is part of Owl.
*
......@@ -52,7 +52,7 @@ public interface EdgeTreeAutomatonMixin<S, A extends OmegaAcceptance> extends Au
@Override
default Set<Edge<S>> edges(S state) {
return edgeTree(state).values();
return edgeTree(state).flatValues();
}
@Override
......@@ -62,7 +62,7 @@ public interface EdgeTreeAutomatonMixin<S, A extends OmegaAcceptance> extends Au
@Override
default Set<S> successors(S state) {
return edgeTree(state).values(Edge::successor);
return edgeTree(state).flatValues(Edge::successor);
}
@Override
......
......@@ -54,7 +54,7 @@ public interface EdgesAutomatonMixin<S, A extends OmegaAcceptance> extends Autom
default Set<Edge<S>> edges(S state) {
Set<Edge<S>> edges = new HashSet<>();
for (BitSet valuation : BitSets.powerSet(factory().alphabet().size())) {
for (BitSet valuation : BitSets.powerSet(factory().atomicPropositions().size())) {
edges.addAll(edges(state, valuation));
}
......@@ -66,7 +66,7 @@ public interface EdgesAutomatonMixin<S, A extends OmegaAcceptance> extends Autom
ValuationSetFactory factory = factory();
Map<Edge<S>, ValuationSet> labelledEdges = new HashMap<>();
for (BitSet valuation : BitSets.powerSet(factory.alphabet().size())) {
for (BitSet valuation : BitSets.powerSet(factory.atomicPropositions().size())) {
for (Edge<S> edge : edges(state, valuation)) {
labelledEdges.merge(edge, factory.of(valuation), ValuationSet::union);
}
......
......@@ -460,7 +460,7 @@ public final class HashMapAutomaton<S, A extends OmegaAcceptance> implements
Set<S> exploredStates = new HashSet<>(initialStates);
Deque<S> workQueue = new ArrayDeque<>(exploredStates);
int alphabetSize = vsFactory.alphabet().size();
int alphabetSize = vsFactory.atomicPropositions().size();
while (!workQueue.isEmpty()) {
S state = workQueue.remove();
......
/*
* Copyright (C) 2016 - 2019 (See AUTHORS)
* Copyright (C) 2016 - 2020 (See AUTHORS)
*
* This file is part of Owl.
*
......@@ -183,7 +183,7 @@ public final class Views {
}
return preferredEdgeAccess().get(0) == EDGE_TREE
? edgeTree(state).values()
? edgeTree(state).flatValues()
: edgeMap(state).keySet();
}
......
......@@ -55,10 +55,10 @@ public final class LanguageEmptiness {
x -> hasAcceptingLasso(automaton, x, -1, -1, false));
}
if (acceptance instanceof BuchiAcceptance) {
var casted = OmegaAcceptanceCast.cast(automaton, BuchiAcceptance.class);
return initialStates.stream().noneMatch(x -> Buchi.containsAcceptingLasso(casted, x));
}
//if (acceptance instanceof BuchiAcceptance) {
// var casted = OmegaAcceptanceCast.cast(automaton, BuchiAcceptance.class);
// return initialStates.stream().noneMatch(x -> Buchi.containsAcceptingScc(casted, x));
//}
if (acceptance instanceof GeneralizedBuchiAcceptance) {
var casted = OmegaAcceptanceCast.cast(automaton, GeneralizedBuchiAcceptance.class);
......
......@@ -172,7 +172,7 @@ public final class HoaReader {
this.storedHeader = storedAutomaton.getStoredHeader();
List<String> variables = storedHeader.getAPs();
List<String> alphabet = vsFactory.alphabet();
List<String> alphabet = vsFactory.atomicPropositions();
if (variables.equals(alphabet)) {
remapping = null;
......
......@@ -69,7 +69,7 @@ public final class HoaWriter {
public static <S> void write(Automaton<S, ?> automaton, HOAConsumer consumer,
EnumSet<HoaOption> options) {
Wrapper<S> hoa = new Wrapper<>(consumer, automaton.factory().alphabet(),
Wrapper<S> hoa = new Wrapper<>(consumer, automaton.factory().atomicPropositions(),
automaton.acceptance(), automaton.initialStates(), options,
automaton.is(Automaton.Property.DETERMINISTIC), automaton.name());
automaton.accept((Automaton.Visitor<S>) hoa.visitor);
......
......@@ -38,23 +38,19 @@ public final class CDecomposedDPA {
private CDecomposedDPA() {}
@CEntryPoint(
name = NAMESPACE + "create",
name = NAMESPACE + "of",
documentation = {
"Translate the given formula to a decomposed DPA.",
CInterface.CALL_DESTROY
},
exceptionHandler = CInterface.PrintStackTraceAndExit.ReturnObjectHandle.class
)
public static ObjectHandle create(
public static ObjectHandle of(
IsolateThread thread,
ObjectHandle cLabelledFormula,
boolean simplify,
boolean monolithic,
int firstOutputAtomicProposition) {
var formula = ObjectHandles.getGlobal().<LabelledFormula>get(cLabelledFormula).formula();
var decomposedDPA = DecomposedDPA.of(
formula, simplify, monolithic, firstOutputAtomicProposition);
ObjectHandle cLabelledFormula) {
var formula = ObjectHandles.getGlobal().<LabelledFormula>get(cLabelledFormula);
var decomposedDPA = DecomposedDPA.of(formula);
return ObjectHandles.getGlobal().create(decomposedDPA);
}
......@@ -88,24 +84,6 @@ public final class CDecomposedDPA {
return ObjectHandles.getGlobal().create(get(cDecomposedDPA).automata.get(index));
}
@CEntryPoint(
name = NAMESPACE + "atomic_proposition_status",
exceptionHandler = CInterface.PrintStackTraceAndExit.ReturnVariableStatus.class
)
public static DecomposedDPA.VariableStatus getAtomicPropositionStatus(
IsolateThread thread,
ObjectHandle cDecomposedDPA,
int atomicProposition) {
var decomposedDPA = ObjectHandles.getGlobal().<DecomposedDPA>get(cDecomposedDPA);
if (atomicProposition < decomposedDPA.variableStatuses.size()) {
return decomposedDPA.variableStatuses.get(atomicProposition);
} else {
return DecomposedDPA.VariableStatus.UNUSED;
}
}
@CEntryPoint(
name = NAMESPACE + "declare_realizability_status",
exceptionHandler = CInterface.PrintStackTraceAndExit.ReturnInt.class
......@@ -150,7 +128,6 @@ public final class CDecomposedDPA {
public static native RealizabilityStatus fromCValue(int value);
}
@CContext(CInterface.CDirectives.class)
public static final class Structure {
private static final String NAMESPACE = "decomposed_dpa_structure_";
......@@ -180,7 +157,13 @@ public final class CDecomposedDPA {
IsolateThread thread,
ObjectHandle cLabelledTree) {
return get(cLabelledTree).label;
var node = get(cLabelledTree);
if (node instanceof DecomposedDPA.Tree.Leaf) {
return NodeType.AUTOMATON;
} else {
return ((DecomposedDPA.Tree.Node) node).label;
}
}
@CEntryPoint(
......@@ -217,7 +200,7 @@ public final class CDecomposedDPA {
IsolateThread thread,
ObjectHandle cLabelledTree) {
return getLeaf(cLabelledTree).reference.index;
return getLeaf(cLabelledTree).index;
}
@CEntryPoint(
......@@ -231,7 +214,7 @@ public final class CDecomposedDPA {
IsolateThread thread,
ObjectHandle cLabelledTree) {
return ObjectHandles.getGlobal().create(getLeaf(cLabelledTree).reference.formula);
return ObjectHandles.getGlobal().create(getLeaf(cLabelledTree).formula);
}
@CEntryPoint(
......@@ -243,7 +226,7 @@ public final class CDecomposedDPA {
ObjectHandle cLabelledTree,
int i) {
var mapping = getLeaf(cLabelledTree).reference.alphabetMapping;
var mapping = getLeaf(cLabelledTree).globalToLocalMapping;
if (i < mapping.length()) {
int value = mapping.get(i);
......@@ -256,17 +239,17 @@ public final class CDecomposedDPA {
return -1;
}
private static DecomposedDPA.DecomposedDPAStructure get(
private static DecomposedDPA.Tree get(
ObjectHandle cDeterministicAutomaton) {
return ObjectHandles.getGlobal().get(cDeterministicAutomaton);
}
private static DecomposedDPA.DecomposedDPAStructure.Leaf getLeaf(
private static DecomposedDPA.Tree.Leaf getLeaf(
ObjectHandle cDeterministicAutomaton) {
return ObjectHandles.getGlobal().get(cDeterministicAutomaton);
}
private static DecomposedDPA.DecomposedDPAStructure.Node getNode(
private static DecomposedDPA.Tree.Node getNode(
ObjectHandle cDeterministicAutomaton) {
return ObjectHandles.getGlobal().get(cDeterministicAutomaton);
}
......
......@@ -26,17 +26,17 @@ import org.graalvm.nativeimage.c.type.CDoublePointer;
import org.graalvm.word.PointerBase;
@CContext(CInterface.CDirectives.class)
@CStruct("double_buffer_t")
interface CDoubleBuffer extends PointerBase {
@CStruct("sized_double_array_t")
interface CDoubleArray extends PointerBase {
@CField
CDoublePointer buffer();
CDoublePointer elements();
@CField
int capacity();
void elements(CDoublePointer elements);
@CField
int position();
int length();
@CField
void position(int position);
void length(int length);
}
/*
* Copyright (C) 2016 - 2020 (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.cinterface;
import java.util.Arrays;
import java.util.Objects;
import org.graalvm.nativeimage.ImageInfo;
import org.graalvm.nativeimage.UnmanagedMemory;
import org.graalvm.nativeimage.c.type.CDoublePointer;
import org.graalvm.word.UnsignedWord;
import org.graalvm.word.WordFactory;
import owl.cinterface.emulation.EmulatedCDoublePointer;
import owl.util.ArraysSupport;
public final class CDoubleArrayList {
private CDoublePointer elements;
private int capacity;
private int size;
public CDoubleArrayList() {
if (ImageInfo.inImageCode()) {
this.elements = UnmanagedMemory.malloc(toBytesLength(32));
this.capacity = 32;
} else {
this.elements = new EmulatedCDoublePointer(1);
this.capacity = 1;
}
this.size = 0;
}
public void add(double value) {
grow(size + 1);
elements.write(size, value);
size = size + 1;
}
public double get(int index) {
Objects.checkIndex(index, size);
return elements.read(index);
}
public void set(int index, double value) {
Objects.checkIndex(index, size);
elements.write(index, value);
}
public int size() {
return size;
}
public void moveToArray(CDoubleArray cDoubleArray) {
if (size == Integer.MIN_VALUE) {
throw new IllegalStateException("already moved");
}
cDoubleArray.elements(UnmanagedMemory.realloc(elements, toBytesLength(size)));
cDoubleArray.length(size);
elements = WordFactory.nullPointer();
size = Integer.MIN_VALUE;
}
public double[] toArray() {
int length = size;
double[] array = new double[length];
for (int i = 0; i < length; i++) {
array[i] = get(i);
}
return array;
}
@Override
public String toString() {
return Arrays.toString(toArray());
}
private void grow(int minCapacity) {
if (capacity >= minCapacity) {
return;
}
int newCapacity = ArraysSupport.newLength(capacity,
minCapacity - capacity, /* minimum growth */
capacity >> 1);
if (ImageInfo.inImageCode()) {
this.elements = UnmanagedMemory.realloc(elements, toBytesLength(newCapacity));
} else {
this.elements = new EmulatedCDoublePointer(
(EmulatedCDoublePointer) this.elements, newCapacity);
}
this.capacity = newCapacity;
}
private static UnsignedWord toBytesLength(long length) {
return WordFactory.unsigned(8L * length);
}
}
\ No newline at end of file
......@@ -26,17 +26,17 @@ import org.graalvm.nativeimage.c.type.CIntPointer;
import org.graalvm.word.PointerBase;
@CContext(CInterface.CDirectives.class)
@CStruct("int_buffer_t")
interface CIntBuffer extends PointerBase {
@CStruct("sized_int_array_t")
interface CIntArray extends PointerBase {
@CField
CIntPointer buffer();
CIntPointer elements();
@CField
int capacity();
void elements(CIntPointer elements);
@CField
int position();
int length();
@CField
void position(int position);
void length(int length);
}
/*
* Copyright (C) 2016 - 2020 (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.cinterface;
import java.util.Arrays;
import java.util.Objects;
import org.graalvm.nativeimage.ImageInfo;
import org.graalvm.nativeimage.UnmanagedMemory;
import org.graalvm.nativeimage.c.type.CIntPointer;
import org.graalvm.word.UnsignedWord;
import org.graalvm.word.WordFactory;
import owl.cinterface.emulation.EmulatedCIntPointer;
import owl.util.ArraysSupport;
public final class CIntArrayList {
private CIntPointer elements;
private int capacity;
private int size;
public CIntArrayList() {
if (ImageInfo.inImageCode()) {
this.elements = UnmanagedMemory.malloc(toBytesLength(64));
this.capacity = 64;
} else {
this.elements = new EmulatedCIntPointer(1);
this.capacity = 1;
}
this.size = 0;
}
public void add(int value) {
grow(size + 1);
elements.write(size, value);
size = size + 1;
}
public void add(int value1, int value2) {
grow(size + 2);
elements.write(size, value1);
elements.write(size + 1, value2);
size = size + 2;