Skip to content

Commit

Permalink
make symbolic values type-aware
Browse files Browse the repository at this point in the history
including some cleanups
  • Loading branch information
mtf90 committed Jul 9, 2024
1 parent 398e863 commit 149aad9
Show file tree
Hide file tree
Showing 29 changed files with 347 additions and 195 deletions.
16 changes: 8 additions & 8 deletions api/src/main/java/net/automatalib/automaton/ra/Assignment.java
Original file line number Diff line number Diff line change
Expand Up @@ -34,25 +34,25 @@
*/
public class Assignment {

private final VarMapping<Register, ? extends SymbolicDataValue> assignment;
private final VarMapping<Register<?>, ? extends SymbolicDataValue<?>> assignment;

public Assignment(VarMapping<Register, ? extends SymbolicDataValue> assignment) {
public Assignment(VarMapping<Register<?>, ? extends SymbolicDataValue<?>> assignment) {
this.assignment = assignment;
}

public VarValuation compute(VarValuation registers, ParValuation parameters, Constants consts) {
VarValuation val = new VarValuation(registers);
for (Entry<Register, ? extends SymbolicDataValue> e : assignment) {
SymbolicDataValue valp = e.getValue();
for (Entry<Register<?>, ? extends SymbolicDataValue<?>> e : assignment) {
SymbolicDataValue<?> valp = e.getValue();
if (valp.isRegister()) {
val.put(e.getKey(), registers.get( (Register) valp));
val.put(e.getKey(), registers.get( (Register<?>) valp));
}
else if (valp.isParameter()) {
val.put(e.getKey(), parameters.get( (Parameter) valp));
val.put(e.getKey(), parameters.get( (Parameter<?>) valp));
}
//TODO: check if we want to copy constant values into vars
else if (valp.isConstant()) {
val.put(e.getKey(), consts.get( (Constant) valp));
val.put(e.getKey(), consts.get( (Constant<?>) valp));
}
else {
throw new IllegalStateException("Illegal assignment: " +
Expand All @@ -67,7 +67,7 @@ public String toString() {
return assignment.toString(":=");
}

public VarMapping<Register, ? extends SymbolicDataValue> getAssignment() {
public VarMapping<Register<?>, ? extends SymbolicDataValue<?>> getAssignment() {
return assignment;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,8 @@

import java.util.Set;

import net.automatalib.data.DataValue;
import net.automatalib.data.Mapping;
import net.automatalib.data.SymbolicDataValue;
import net.automatalib.data.Valuation;
import net.automatalib.data.VarMapping;

/**
Expand All @@ -32,7 +31,7 @@ public interface GuardExpression {

GuardExpression relabel(VarMapping<?, ?> relabelling);

boolean isSatisfied(Mapping<SymbolicDataValue, DataValue<?>> val);
boolean isSatisfied(Valuation<?, ?> val);

Set<SymbolicDataValue> getSymbolicDataValues();
Set<SymbolicDataValue<?>> getSymbolicDataValues();
}
Original file line number Diff line number Diff line change
Expand Up @@ -17,18 +17,15 @@
package net.automatalib.automaton.ra;

import java.util.Collection;
import java.util.List;
import java.util.Set;

import net.automatalib.automaton.DeterministicAutomaton;
import net.automatalib.automaton.UniversalAutomaton;
import net.automatalib.data.Constants;
import net.automatalib.data.SymbolicDataValue.Register;
import net.automatalib.data.VarValuation;
import net.automatalib.symbol.PSymbolInstance;
import net.automatalib.symbol.ParameterizedSymbol;
import net.automatalib.ts.acceptor.AcceptorTS;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
Expand All @@ -39,7 +36,7 @@ public interface RegisterAutomaton<L, T extends GuardedTransition> extends Unive

Constants getConstants();

Collection<Register> getRegisters();
Collection<Register<?>> getRegisters();

VarValuation getInitialRegisters();

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@
*/
public interface RegisterMealyMachine<L, T extends GuardedOutputTransition> extends UniversalAutomaton<L, ParameterizedSymbol, T, Void, ParameterizedSymbol> {

Collection<Register> getRegisters();

Constants getConstants();

Collection<Register<?>> getRegisters();

VarValuation getInitialRegisters();

default @Nullable L getInitialState() {
Expand Down
4 changes: 3 additions & 1 deletion api/src/main/java/net/automatalib/data/Constants.java
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,13 @@
*/
package net.automatalib.data;

import net.automatalib.data.SymbolicDataValue.Constant;

/**
* Named constants.
*
* @author falk
*/
public class Constants extends Valuation<SymbolicDataValue.Constant, DataValue<?>> {
public class Constants extends Valuation<Constant<?>, DataValue<?>> {

}
2 changes: 1 addition & 1 deletion api/src/main/java/net/automatalib/data/DataType.java
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ public String getName() {
return name;
}

public Class<?> getBase() {
public Class<T> getBase() {
return base;
}
}
18 changes: 9 additions & 9 deletions api/src/main/java/net/automatalib/data/DataValue.java
Original file line number Diff line number Diff line change
Expand Up @@ -27,23 +27,23 @@ public class DataValue<T> {

protected final DataType<T> type;

protected final T id;
protected final T value;

public DataValue(DataType<T> type, T id) {
public DataValue(DataType<T> type, T value) {
this.type = type;
this.id = id;
this.value = value;
}

@Override
public String toString() {
return id.toString() + "[" + this.type.getName() + "]";
return value.toString() + "[" + this.type.getName() + "]";
}

@Override
public int hashCode() {
int hash = 7;
hash = 97 * hash + Objects.hashCode(this.type);
hash = 97 * hash + Objects.hashCode(this.id);
hash = 97 * hash + Objects.hashCode(this.value);
return hash;
}

Expand All @@ -57,14 +57,14 @@ public boolean equals(Object obj) {
}
final DataValue<?> other = (DataValue<?>) obj;

return Objects.equals(this.type, other.type) && Objects.equals(this.id, other.id);
return Objects.equals(this.type, other.type) && Objects.equals(this.value, other.value);
}

public T getId() {
return id;
public T getValue() {
return value;
}

public DataType<?> getType() {
public DataType<T> getType() {
return type;
}

Expand Down
2 changes: 1 addition & 1 deletion api/src/main/java/net/automatalib/data/ParValuation.java
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
*
* @author falk
*/
public class ParValuation extends Valuation<Parameter, DataValue<?>> {
public class ParValuation extends Valuation<Parameter<?>, DataValue<?>> {

public ParValuation() {

Expand Down
44 changes: 22 additions & 22 deletions api/src/main/java/net/automatalib/data/SymbolicDataValue.java
Original file line number Diff line number Diff line change
Expand Up @@ -23,33 +23,33 @@
*
* @author falk
*/
public abstract class SymbolicDataValue {
public abstract class SymbolicDataValue<T> {

protected final DataType<?> type;
protected final DataType<T> type;
protected final int id;

private SymbolicDataValue(DataType<?> dataType, int id) {
private SymbolicDataValue(DataType<T> dataType, int id) {
this.type = dataType;
this.id = id;
}

public DataType<?> getType() {
public DataType<T> getType() {
return type;
}

public int getId() {
return id;
}

public static final class Parameter extends SymbolicDataValue {
public static final class Parameter<T> extends SymbolicDataValue<T> {

public Parameter(DataType<?> dataType, int id) {
public Parameter(DataType<T> dataType, int id) {
super(dataType, id);
}

@Override
public SymbolicDataValue.Parameter copy() {
return new SymbolicDataValue.Parameter(type, id);
public SymbolicDataValue.Parameter<T> copy() {
return new SymbolicDataValue.Parameter<>(type, id);
}

@Override
Expand All @@ -58,15 +58,15 @@ public String toString() {
}
};

public static final class Register extends SymbolicDataValue {
public static final class Register<T> extends SymbolicDataValue<T> {

public Register(DataType<?> dataType, int id) {
public Register(DataType<T> dataType, int id) {
super(dataType, id);
}

@Override
public SymbolicDataValue.Register copy() {
return new SymbolicDataValue.Register(type, id);
public SymbolicDataValue.Register<T> copy() {
return new SymbolicDataValue.Register<>(type, id);
}

@Override
Expand All @@ -75,15 +75,15 @@ public String toString() {
}
};

public static final class Constant extends SymbolicDataValue {
public static final class Constant<T> extends SymbolicDataValue<T> {

public Constant(DataType<?> dataType, int id) {
public Constant(DataType<T> dataType, int id) {
super(dataType, id);
}

@Override
public SymbolicDataValue.Constant copy() {
return new SymbolicDataValue.Constant(type, id);
public SymbolicDataValue.Constant<T> copy() {
return new SymbolicDataValue.Constant<>(type, id);
}

@Override
Expand All @@ -92,15 +92,15 @@ public String toString() {
}
};

public static final class SuffixValue extends SymbolicDataValue {
public static final class SuffixValue<T> extends SymbolicDataValue<T> {

public SuffixValue(DataType<?> dataType, int id) {
public SuffixValue(DataType<T> dataType, int id) {
super(dataType, id);
}

@Override
public SymbolicDataValue.SuffixValue copy() {
return new SymbolicDataValue.SuffixValue(type, id);
public SymbolicDataValue.SuffixValue<T> copy() {
return new SymbolicDataValue.SuffixValue<>(type, id);
}

@Override
Expand All @@ -109,7 +109,7 @@ public String toString() {
}
};

public abstract SymbolicDataValue copy();
public abstract SymbolicDataValue<T> copy();

@Override
public boolean equals(Object obj) {
Expand All @@ -120,7 +120,7 @@ public boolean equals(Object obj) {
return false;
}

final SymbolicDataValue other = (SymbolicDataValue) obj;
final SymbolicDataValue<?> other = (SymbolicDataValue<?>) obj;

return this.id == other.id && Objects.equals(this.type, other.type);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,33 +32,33 @@ public void set(SymbolicDataValueGenerator g) {
id = g.id;
}

public abstract SymbolicDataValue next(DataType<?> type);
public abstract <T> SymbolicDataValue<T> next(DataType<T> type);

public static final class ParameterGenerator extends SymbolicDataValueGenerator {
@Override
public SymbolicDataValue.Parameter next(DataType<?> type) {
return new SymbolicDataValue.Parameter(type, id++);
public <T> SymbolicDataValue.Parameter<T> next(DataType<T> type) {
return new SymbolicDataValue.Parameter<>(type, id++);
}
};

public static final class RegisterGenerator extends SymbolicDataValueGenerator {
@Override
public SymbolicDataValue.Register next(DataType<?> type) {
return new SymbolicDataValue.Register(type, id++);
public <T> SymbolicDataValue.Register<T> next(DataType<T> type) {
return new SymbolicDataValue.Register<>(type, id++);
}
};

public static final class SuffixValueGenerator extends SymbolicDataValueGenerator {
@Override
public SymbolicDataValue.SuffixValue next(DataType<?> type) {
return new SymbolicDataValue.SuffixValue(type, id++);
public <T> SymbolicDataValue.SuffixValue<T> next(DataType<T> type) {
return new SymbolicDataValue.SuffixValue<>(type, id++);
}
};

public static final class ConstantGenerator extends SymbolicDataValueGenerator {
@Override
public SymbolicDataValue.Constant next(DataType<?> type) {
return new SymbolicDataValue.Constant(type, id++);
public <T> SymbolicDataValue.Constant<T> next(DataType<T> type) {
return new SymbolicDataValue.Constant<>(type, id++);
}
};
}
15 changes: 14 additions & 1 deletion api/src/main/java/net/automatalib/data/Valuation.java
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@
* @param <K>
* @param <V>
*/
public class Valuation<K, V extends DataValue<?>> extends Mapping<K, V> {
public class Valuation<K extends SymbolicDataValue<?>, V extends DataValue<?>> extends Mapping<K, V> {

/**
* returns the contained values of some type.
Expand All @@ -50,4 +50,17 @@ public <T> Collection<DataValue<T>> values(DataType<T> type) {
return list;
}

@Override
public V put(K key, V value) {
if (!key.getType().equals(value.getType())) {
throw new IllegalArgumentException("Types of key and value do not match");
}
return super.put(key, value);
}

@SuppressWarnings("unchecked")
public <T> DataValue<T> get(SymbolicDataValue<T> key) {
return (DataValue<T>) super.get(key);
}

}
Loading

0 comments on commit 149aad9

Please sign in to comment.