From 149aad9f67f706a5c50fa07b043fa01e2777dd23 Mon Sep 17 00:00:00 2001 From: Markus Frohme Date: Tue, 9 Jul 2024 16:31:10 +0200 Subject: [PATCH] make symbolic values type-aware including some cleanups --- .../automatalib/automaton/ra/Assignment.java | 16 +-- .../automaton/ra/GuardExpression.java | 7 +- .../automaton/ra/RegisterAutomaton.java | 5 +- .../automaton/ra/RegisterMealyMachine.java | 4 +- .../java/net/automatalib/data/Constants.java | 4 +- .../java/net/automatalib/data/DataType.java | 2 +- .../java/net/automatalib/data/DataValue.java | 18 ++-- .../net/automatalib/data/ParValuation.java | 2 +- .../automatalib/data/SymbolicDataValue.java | 44 ++++---- .../data/SymbolicDataValueGenerator.java | 18 ++-- .../java/net/automatalib/data/Valuation.java | 15 ++- .../java/net/automatalib/data/VarMapping.java | 26 ++++- .../net/automatalib/data/VarValuation.java | 4 +- .../automatalib/symbol/PSymbolInstance.java | 13 +++ .../ra/guard/impl/AtomicGuardExpression.java | 18 ++-- .../automaton/ra/guard/impl/Conjunction.java | 9 +- .../automaton/ra/guard/impl/Disjunction.java | 9 +- .../ra/guard/impl/EqualityGuard.java | 52 +++++++++ .../ra/guard/impl/FalseGuardExpression.java | 11 +- .../automaton/ra/guard/impl/Negation.java | 9 +- .../automaton/ra/guard/impl/SmallerGuard.java | 52 +++++++++ .../ra/guard/impl/TrueGuardExpression.java | 9 +- .../automaton/ra/impl/OutputMapping.java | 27 ++--- .../automaton/ra/impl/OutputTransition.java | 10 +- .../automaton/ra/impl/RegisterAutomaton.java | 4 +- .../automaton/ra/impl/TransitionGuard.java | 5 +- .../xml/ra/ExpressionParser.java | 10 +- .../xml/ra/RegisterAutomatonExporter.java | 38 +++---- .../xml/ra/RegisterAutomatonImporter.java | 101 +++++++++--------- 29 files changed, 347 insertions(+), 195 deletions(-) create mode 100644 core/src/main/java/net/automatalib/automaton/ra/guard/impl/EqualityGuard.java create mode 100644 core/src/main/java/net/automatalib/automaton/ra/guard/impl/SmallerGuard.java diff --git a/api/src/main/java/net/automatalib/automaton/ra/Assignment.java b/api/src/main/java/net/automatalib/automaton/ra/Assignment.java index d412e3a52..e9adfd2dd 100644 --- a/api/src/main/java/net/automatalib/automaton/ra/Assignment.java +++ b/api/src/main/java/net/automatalib/automaton/ra/Assignment.java @@ -34,25 +34,25 @@ */ public class Assignment { - private final VarMapping assignment; + private final VarMapping, ? extends SymbolicDataValue> assignment; - public Assignment(VarMapping assignment) { + public Assignment(VarMapping, ? extends SymbolicDataValue> assignment) { this.assignment = assignment; } public VarValuation compute(VarValuation registers, ParValuation parameters, Constants consts) { VarValuation val = new VarValuation(registers); - for (Entry e : assignment) { - SymbolicDataValue valp = e.getValue(); + for (Entry, ? 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: " + @@ -67,7 +67,7 @@ public String toString() { return assignment.toString(":="); } - public VarMapping getAssignment() { + public VarMapping, ? extends SymbolicDataValue> getAssignment() { return assignment; } diff --git a/api/src/main/java/net/automatalib/automaton/ra/GuardExpression.java b/api/src/main/java/net/automatalib/automaton/ra/GuardExpression.java index d0a80ec5d..53e7e52ce 100644 --- a/api/src/main/java/net/automatalib/automaton/ra/GuardExpression.java +++ b/api/src/main/java/net/automatalib/automaton/ra/GuardExpression.java @@ -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; /** @@ -32,7 +31,7 @@ public interface GuardExpression { GuardExpression relabel(VarMapping relabelling); - boolean isSatisfied(Mapping> val); + boolean isSatisfied(Valuation val); - Set getSymbolicDataValues(); + Set> getSymbolicDataValues(); } diff --git a/api/src/main/java/net/automatalib/automaton/ra/RegisterAutomaton.java b/api/src/main/java/net/automatalib/automaton/ra/RegisterAutomaton.java index a8ceba09d..288b3f554 100644 --- a/api/src/main/java/net/automatalib/automaton/ra/RegisterAutomaton.java +++ b/api/src/main/java/net/automatalib/automaton/ra/RegisterAutomaton.java @@ -17,10 +17,8 @@ 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; @@ -28,7 +26,6 @@ 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; /** @@ -39,7 +36,7 @@ public interface RegisterAutomaton extends Unive Constants getConstants(); - Collection getRegisters(); + Collection> getRegisters(); VarValuation getInitialRegisters(); diff --git a/api/src/main/java/net/automatalib/automaton/ra/RegisterMealyMachine.java b/api/src/main/java/net/automatalib/automaton/ra/RegisterMealyMachine.java index 00b347394..c3f8aca7c 100644 --- a/api/src/main/java/net/automatalib/automaton/ra/RegisterMealyMachine.java +++ b/api/src/main/java/net/automatalib/automaton/ra/RegisterMealyMachine.java @@ -33,10 +33,10 @@ */ public interface RegisterMealyMachine extends UniversalAutomaton { - Collection getRegisters(); - Constants getConstants(); + Collection> getRegisters(); + VarValuation getInitialRegisters(); default @Nullable L getInitialState() { diff --git a/api/src/main/java/net/automatalib/data/Constants.java b/api/src/main/java/net/automatalib/data/Constants.java index c45f3c269..31e410372 100644 --- a/api/src/main/java/net/automatalib/data/Constants.java +++ b/api/src/main/java/net/automatalib/data/Constants.java @@ -16,11 +16,13 @@ */ package net.automatalib.data; +import net.automatalib.data.SymbolicDataValue.Constant; + /** * Named constants. * * @author falk */ -public class Constants extends Valuation> { +public class Constants extends Valuation, DataValue> { } diff --git a/api/src/main/java/net/automatalib/data/DataType.java b/api/src/main/java/net/automatalib/data/DataType.java index 6ac4e6973..49099409d 100644 --- a/api/src/main/java/net/automatalib/data/DataType.java +++ b/api/src/main/java/net/automatalib/data/DataType.java @@ -61,7 +61,7 @@ public String getName() { return name; } - public Class getBase() { + public Class getBase() { return base; } } diff --git a/api/src/main/java/net/automatalib/data/DataValue.java b/api/src/main/java/net/automatalib/data/DataValue.java index c0e4b4233..43a90eac4 100644 --- a/api/src/main/java/net/automatalib/data/DataValue.java +++ b/api/src/main/java/net/automatalib/data/DataValue.java @@ -27,23 +27,23 @@ public class DataValue { protected final DataType type; - protected final T id; + protected final T value; - public DataValue(DataType type, T id) { + public DataValue(DataType 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; } @@ -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 getType() { return type; } diff --git a/api/src/main/java/net/automatalib/data/ParValuation.java b/api/src/main/java/net/automatalib/data/ParValuation.java index 6a5bdbfa8..943b4b77a 100644 --- a/api/src/main/java/net/automatalib/data/ParValuation.java +++ b/api/src/main/java/net/automatalib/data/ParValuation.java @@ -28,7 +28,7 @@ * * @author falk */ -public class ParValuation extends Valuation> { +public class ParValuation extends Valuation, DataValue> { public ParValuation() { diff --git a/api/src/main/java/net/automatalib/data/SymbolicDataValue.java b/api/src/main/java/net/automatalib/data/SymbolicDataValue.java index 4c642f2bf..3fb4ff8ef 100644 --- a/api/src/main/java/net/automatalib/data/SymbolicDataValue.java +++ b/api/src/main/java/net/automatalib/data/SymbolicDataValue.java @@ -23,17 +23,17 @@ * * @author falk */ -public abstract class SymbolicDataValue { +public abstract class SymbolicDataValue { - protected final DataType type; + protected final DataType type; protected final int id; - private SymbolicDataValue(DataType dataType, int id) { + private SymbolicDataValue(DataType dataType, int id) { this.type = dataType; this.id = id; } - public DataType getType() { + public DataType getType() { return type; } @@ -41,15 +41,15 @@ public int getId() { return id; } - public static final class Parameter extends SymbolicDataValue { + public static final class Parameter extends SymbolicDataValue { - public Parameter(DataType dataType, int id) { + public Parameter(DataType dataType, int id) { super(dataType, id); } @Override - public SymbolicDataValue.Parameter copy() { - return new SymbolicDataValue.Parameter(type, id); + public SymbolicDataValue.Parameter copy() { + return new SymbolicDataValue.Parameter<>(type, id); } @Override @@ -58,15 +58,15 @@ public String toString() { } }; - public static final class Register extends SymbolicDataValue { + public static final class Register extends SymbolicDataValue { - public Register(DataType dataType, int id) { + public Register(DataType dataType, int id) { super(dataType, id); } @Override - public SymbolicDataValue.Register copy() { - return new SymbolicDataValue.Register(type, id); + public SymbolicDataValue.Register copy() { + return new SymbolicDataValue.Register<>(type, id); } @Override @@ -75,15 +75,15 @@ public String toString() { } }; - public static final class Constant extends SymbolicDataValue { + public static final class Constant extends SymbolicDataValue { - public Constant(DataType dataType, int id) { + public Constant(DataType dataType, int id) { super(dataType, id); } @Override - public SymbolicDataValue.Constant copy() { - return new SymbolicDataValue.Constant(type, id); + public SymbolicDataValue.Constant copy() { + return new SymbolicDataValue.Constant<>(type, id); } @Override @@ -92,15 +92,15 @@ public String toString() { } }; - public static final class SuffixValue extends SymbolicDataValue { + public static final class SuffixValue extends SymbolicDataValue { - public SuffixValue(DataType dataType, int id) { + public SuffixValue(DataType dataType, int id) { super(dataType, id); } @Override - public SymbolicDataValue.SuffixValue copy() { - return new SymbolicDataValue.SuffixValue(type, id); + public SymbolicDataValue.SuffixValue copy() { + return new SymbolicDataValue.SuffixValue<>(type, id); } @Override @@ -109,7 +109,7 @@ public String toString() { } }; - public abstract SymbolicDataValue copy(); + public abstract SymbolicDataValue copy(); @Override public boolean equals(Object obj) { @@ -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); } diff --git a/api/src/main/java/net/automatalib/data/SymbolicDataValueGenerator.java b/api/src/main/java/net/automatalib/data/SymbolicDataValueGenerator.java index c60bcaec6..7d13f9982 100644 --- a/api/src/main/java/net/automatalib/data/SymbolicDataValueGenerator.java +++ b/api/src/main/java/net/automatalib/data/SymbolicDataValueGenerator.java @@ -32,33 +32,33 @@ public void set(SymbolicDataValueGenerator g) { id = g.id; } - public abstract SymbolicDataValue next(DataType type); + public abstract SymbolicDataValue next(DataType type); public static final class ParameterGenerator extends SymbolicDataValueGenerator { @Override - public SymbolicDataValue.Parameter next(DataType type) { - return new SymbolicDataValue.Parameter(type, id++); + public SymbolicDataValue.Parameter next(DataType 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 SymbolicDataValue.Register next(DataType 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 SymbolicDataValue.SuffixValue next(DataType 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 SymbolicDataValue.Constant next(DataType type) { + return new SymbolicDataValue.Constant<>(type, id++); } }; } diff --git a/api/src/main/java/net/automatalib/data/Valuation.java b/api/src/main/java/net/automatalib/data/Valuation.java index fd61a7c2e..868a15178 100644 --- a/api/src/main/java/net/automatalib/data/Valuation.java +++ b/api/src/main/java/net/automatalib/data/Valuation.java @@ -31,7 +31,7 @@ * @param * @param */ -public class Valuation> extends Mapping { +public class Valuation, V extends DataValue> extends Mapping { /** * returns the contained values of some type. @@ -50,4 +50,17 @@ public Collection> values(DataType 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 DataValue get(SymbolicDataValue key) { + return (DataValue) super.get(key); + } + } diff --git a/api/src/main/java/net/automatalib/data/VarMapping.java b/api/src/main/java/net/automatalib/data/VarMapping.java index 55f7fdda6..8ed29b010 100644 --- a/api/src/main/java/net/automatalib/data/VarMapping.java +++ b/api/src/main/java/net/automatalib/data/VarMapping.java @@ -16,6 +16,8 @@ */ package net.automatalib.data; +import net.automatalib.data.SymbolicDataValue.Register; + /** * maps symbolic data values to symbolic data values. * @@ -24,11 +26,33 @@ * * @author falk */ -public class VarMapping extends Mapping { +public class VarMapping, V extends SymbolicDataValue> extends Mapping { public VarMapping() {} public VarMapping(K k1, V v1) { put(k1, v1); } + + @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 SymbolicDataValue get(SymbolicDataValue key) { + return (SymbolicDataValue) super.get(key); + } + + public static class RegMapping> extends VarMapping> { + + @Override + public Register get(SymbolicDataValue key) { + return (Register) super.get(key); + } + } + } diff --git a/api/src/main/java/net/automatalib/data/VarValuation.java b/api/src/main/java/net/automatalib/data/VarValuation.java index 9a053c584..8fe4f1a42 100644 --- a/api/src/main/java/net/automatalib/data/VarValuation.java +++ b/api/src/main/java/net/automatalib/data/VarValuation.java @@ -16,12 +16,14 @@ */ package net.automatalib.data; +import net.automatalib.data.SymbolicDataValue.Register; + /** * A valuation of registers. * * @author falk */ -public class VarValuation extends Valuation> { +public class VarValuation extends Valuation, DataValue> { public VarValuation(VarValuation other) { if (other != null) { diff --git a/api/src/main/java/net/automatalib/symbol/PSymbolInstance.java b/api/src/main/java/net/automatalib/symbol/PSymbolInstance.java index 2ba109dbb..a8fdeeeeb 100644 --- a/api/src/main/java/net/automatalib/symbol/PSymbolInstance.java +++ b/api/src/main/java/net/automatalib/symbol/PSymbolInstance.java @@ -19,6 +19,7 @@ import java.util.Arrays; import java.util.Objects; +import net.automatalib.data.DataType; import net.automatalib.data.DataValue; /** @@ -40,6 +41,18 @@ public class PSymbolInstance { public PSymbolInstance(ParameterizedSymbol baseSymbol, DataValue ... parameterValues) { + + if (baseSymbol.getArity() == parameterValues.length) { + final DataType[] types = baseSymbol.getPtypes(); + for (int i = 0; i < parameterValues.length; i++) { + if (!types[i].equals(parameterValues[i].getType())) { + throw new IllegalArgumentException("Type of parameter '" + parameterValues[i] + "' does not match expected type"); + } + } + } else { + throw new IllegalArgumentException("The numbers of parameters and values do not match"); + } + this.baseSymbol = baseSymbol; this.parameterValues = parameterValues; } diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/AtomicGuardExpression.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/AtomicGuardExpression.java index 98b9165b5..d3c1e0f68 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/AtomicGuardExpression.java +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/AtomicGuardExpression.java @@ -20,11 +20,11 @@ import java.util.LinkedHashSet; import java.util.Set; +import net.automatalib.automaton.ra.GuardExpression; 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; -import net.automatalib.automaton.ra.GuardExpression; /** * @@ -32,7 +32,7 @@ * @param * @param */ -public class AtomicGuardExpression implements +public class AtomicGuardExpression, Right extends SymbolicDataValue> implements GuardExpression { private final Left left; @@ -48,7 +48,7 @@ public AtomicGuardExpression(Left left, Relation relation, Right right) { } @Override - public boolean isSatisfied(Mapping> val) { + public boolean isSatisfied(Valuation val) { DataValue lv = val.get(left); DataValue rv = val.get(right); @@ -75,11 +75,11 @@ public boolean isSatisfied(Mapping> val) { @Override public GuardExpression relabel(VarMapping relabelling) { - SymbolicDataValue newLeft = relabelling.get(left); + SymbolicDataValue newLeft = relabelling.get(left); if (newLeft == null) { newLeft = left; } - SymbolicDataValue newRight = relabelling.get(right); + SymbolicDataValue newRight = relabelling.get(right); if (newRight == null) { newRight = right; } @@ -101,7 +101,7 @@ public Right getRight() { } @Override - public Set getSymbolicDataValues() { + public Set> getSymbolicDataValues() { return new LinkedHashSet<>(Arrays.asList(left, right)); } @@ -114,8 +114,8 @@ private boolean numCompare(DataValue l, DataValue r, Relation relation) { return false; } - Comparable lc = (Comparable) l.getId(); - int result = lc.compareTo(r.getId()); + Comparable lc = (Comparable) l.getValue(); + int result = lc.compareTo(r.getValue()); switch (relation) { case SMALLER: return result < 0; diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Conjunction.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Conjunction.java index e2a333810..9a61f9add 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Conjunction.java +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Conjunction.java @@ -21,9 +21,8 @@ import net.automatalib.automaton.ra.GuardExpression; import net.automatalib.common.util.string.StringUtil; -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; /** @@ -49,7 +48,7 @@ public GuardExpression relabel(VarMapping relabelling) { } @Override - public boolean isSatisfied(Mapping> val) { + public boolean isSatisfied(Valuation val) { for (GuardExpression ge : conjuncts) { if (!ge.isSatisfied(val)) { return false; @@ -64,8 +63,8 @@ public String toString() { } @Override - public Set getSymbolicDataValues() { - final Set result = new LinkedHashSet<>(); + public Set> getSymbolicDataValues() { + final Set> result = new LinkedHashSet<>(); for (GuardExpression ge : conjuncts) { result.addAll(ge.getSymbolicDataValues()); } diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Disjunction.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Disjunction.java index 5e3fcf018..377ed0e80 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Disjunction.java +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Disjunction.java @@ -21,9 +21,8 @@ import net.automatalib.automaton.ra.GuardExpression; import net.automatalib.common.util.string.StringUtil; -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; /** @@ -49,7 +48,7 @@ public GuardExpression relabel(VarMapping relabelling) { } @Override - public boolean isSatisfied(Mapping> val) { + public boolean isSatisfied(Valuation val) { for (GuardExpression ge : disjuncts) { if (ge.isSatisfied(val)) { return true; @@ -64,8 +63,8 @@ public String toString() { } @Override - public Set getSymbolicDataValues() { - final Set result = new LinkedHashSet<>(); + public Set> getSymbolicDataValues() { + final Set> result = new LinkedHashSet<>(); for (GuardExpression ge : disjuncts) { result.addAll(ge.getSymbolicDataValues()); } diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/EqualityGuard.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/EqualityGuard.java new file mode 100644 index 000000000..db82a973f --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/EqualityGuard.java @@ -0,0 +1,52 @@ +package net.automatalib.automaton.ra.guard.impl; + +import java.util.Arrays; +import java.util.LinkedHashSet; +import java.util.Set; + +import net.automatalib.automaton.ra.GuardExpression; +import net.automatalib.data.DataValue; +import net.automatalib.data.SymbolicDataValue; +import net.automatalib.data.Valuation; +import net.automatalib.data.VarMapping; + +public class EqualityGuard implements GuardExpression { + + private final SymbolicDataValue left; + private final SymbolicDataValue right; + + public EqualityGuard(SymbolicDataValue left, SymbolicDataValue right) { + this.left = left; + this.right = right; + } + + @Override + public boolean isSatisfied(Valuation val) { + DataValue lv = val.get(left); + DataValue rv = val.get(right); + + assert lv != null && rv != null; + + return lv.equals(rv); + } + + @Override + public GuardExpression relabel(VarMapping relabelling) { + SymbolicDataValue newLeft = relabelling.get(left); + if (newLeft == null) { + newLeft = left; + } + SymbolicDataValue newRight = relabelling.get(right); + if (newRight == null) { + newRight = right; + } + + return new EqualityGuard(newLeft, newRight); + } + + @Override + public Set> getSymbolicDataValues() { + return new LinkedHashSet<>(Arrays.asList(left, right)); + } + +} diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/FalseGuardExpression.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/FalseGuardExpression.java index 72bb9e1a1..aaa539a94 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/FalseGuardExpression.java +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/FalseGuardExpression.java @@ -19,11 +19,10 @@ import java.util.Collections; import java.util.Set; -import net.automatalib.data.DataValue; -import net.automatalib.data.Mapping; +import net.automatalib.automaton.ra.GuardExpression; import net.automatalib.data.SymbolicDataValue; +import net.automatalib.data.Valuation; import net.automatalib.data.VarMapping; -import net.automatalib.automaton.ra.GuardExpression; /** * @@ -39,8 +38,8 @@ public GuardExpression relabel(VarMapping relabelling) { } @Override - public boolean isSatisfied(Mapping> val) { - return true; + public boolean isSatisfied(Valuation val) { + return false; } @Override @@ -49,7 +48,7 @@ public String toString() { } @Override - public Set getSymbolicDataValues() { + public Set> getSymbolicDataValues() { return Collections.emptySet(); } } diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Negation.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Negation.java index 6ccac4b24..76abb615b 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Negation.java +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/Negation.java @@ -18,11 +18,10 @@ import java.util.Set; -import net.automatalib.data.DataValue; -import net.automatalib.data.Mapping; +import net.automatalib.automaton.ra.GuardExpression; import net.automatalib.data.SymbolicDataValue; +import net.automatalib.data.Valuation; import net.automatalib.data.VarMapping; -import net.automatalib.automaton.ra.GuardExpression; /** * @@ -47,7 +46,7 @@ public GuardExpression relabel(VarMapping relabelling) { } @Override - public boolean isSatisfied(Mapping> val) { + public boolean isSatisfied(Valuation val) { return !negated.isSatisfied(val); } @@ -57,7 +56,7 @@ public String toString() { } @Override - public Set getSymbolicDataValues() { + public Set> getSymbolicDataValues() { return this.negated.getSymbolicDataValues(); } diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/SmallerGuard.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/SmallerGuard.java new file mode 100644 index 000000000..1e8fcdb44 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/SmallerGuard.java @@ -0,0 +1,52 @@ +package net.automatalib.automaton.ra.guard.impl; + +import java.util.Arrays; +import java.util.LinkedHashSet; +import java.util.Set; + +import net.automatalib.automaton.ra.GuardExpression; +import net.automatalib.data.DataValue; +import net.automatalib.data.SymbolicDataValue; +import net.automatalib.data.Valuation; +import net.automatalib.data.VarMapping; + +public class SmallerGuard, L extends SymbolicDataValue, R extends SymbolicDataValue> implements GuardExpression { + + private final L left; + private final R right; + + public SmallerGuard(L left, R right) { + this.left = left; + this.right = right; + } + + @Override + public boolean isSatisfied(Valuation val) { + DataValue lv = val.get(left); + DataValue rv = val.get(right); + + assert lv != null && rv != null; + + return lv.getValue().compareTo(rv.getValue()) < 0; + } + + @Override + public GuardExpression relabel(VarMapping relabelling) { + SymbolicDataValue newLeft = relabelling.get(left); + if (newLeft == null) { + newLeft = left; + } + SymbolicDataValue newRight = relabelling.get(right); + if (newRight == null) { + newRight = right; + } + + return new SmallerGuard<>(newLeft, newRight); + } + + @Override + public Set> getSymbolicDataValues() { + return new LinkedHashSet<>(Arrays.asList(left, right)); + } + +} diff --git a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/TrueGuardExpression.java b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/TrueGuardExpression.java index e76b534ad..a82a0f6f7 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/guard/impl/TrueGuardExpression.java +++ b/core/src/main/java/net/automatalib/automaton/ra/guard/impl/TrueGuardExpression.java @@ -19,11 +19,10 @@ import java.util.Collections; import java.util.Set; -import net.automatalib.data.DataValue; -import net.automatalib.data.Mapping; +import net.automatalib.automaton.ra.GuardExpression; import net.automatalib.data.SymbolicDataValue; +import net.automatalib.data.Valuation; import net.automatalib.data.VarMapping; -import net.automatalib.automaton.ra.GuardExpression; /** * @@ -39,7 +38,7 @@ public GuardExpression relabel(VarMapping relabelling) { } @Override - public boolean isSatisfied(Mapping> val) { + public boolean isSatisfied(Valuation val) { return true; } @@ -49,7 +48,7 @@ public String toString() { } @Override - public Set getSymbolicDataValues() { + public Set> getSymbolicDataValues() { return Collections.emptySet(); } } diff --git a/core/src/main/java/net/automatalib/automaton/ra/impl/OutputMapping.java b/core/src/main/java/net/automatalib/automaton/ra/impl/OutputMapping.java index dc73481ef..4920a6cd0 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/impl/OutputMapping.java +++ b/core/src/main/java/net/automatalib/automaton/ra/impl/OutputMapping.java @@ -37,37 +37,38 @@ */ public class OutputMapping { - private final Collection fresh; + private final Collection> fresh; - private final VarMapping piv; + private final VarMapping, SymbolicDataValue> piv; - public OutputMapping(Collection fresh, - VarMapping piv) { + public OutputMapping(Collection> fresh, + VarMapping, SymbolicDataValue> piv) { this.fresh = fresh; this.piv = piv; } public OutputMapping() { - this(new ArrayList(), new VarMapping()); + this(new ArrayList<>(), new VarMapping<>()); } - public OutputMapping(Parameter fresh) { - this(Collections.singleton(fresh), new VarMapping()); + public OutputMapping(Parameter fresh) { + this(Collections.singleton(fresh), new VarMapping<>()); } - public OutputMapping(Parameter key, Register value) { - this(new ArrayList(), new VarMapping(key, value)); + public OutputMapping(Parameter key, Register value) { + this(new ArrayList<>(), new VarMapping<>()); + this.piv.put(key, value); } - public OutputMapping(VarMapping outputs) { - this(new ArrayList(), outputs); + public OutputMapping(VarMapping, SymbolicDataValue> outputs) { + this(new ArrayList<>(), outputs); } - public Collection getFreshParameters() { + public Collection> getFreshParameters() { return fresh; } - public VarMapping getOutput() { + public VarMapping, SymbolicDataValue> getOutput() { return piv; } diff --git a/core/src/main/java/net/automatalib/automaton/ra/impl/OutputTransition.java b/core/src/main/java/net/automatalib/automaton/ra/impl/OutputTransition.java index 15a86cf24..a9935fc9e 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/impl/OutputTransition.java +++ b/core/src/main/java/net/automatalib/automaton/ra/impl/OutputTransition.java @@ -59,12 +59,12 @@ public boolean canBeEnabled(VarValuation registers, Constants consts) { public boolean isEnabled(VarValuation registers, ParValuation parameters, Constants consts) { // check freshness of parameters ... - for (Parameter p : output.getFreshParameters()) { + for (Parameter p : output.getFreshParameters()) { DataValue pval = parameters.get(p); if (registers.containsValue(pval) || consts.containsValue(pval)) { return false; } - for (Entry> e : parameters) { + for (Entry, DataValue> e : parameters) { if (!p.equals(e.getKey()) && pval.equals(e.getValue())) { return false; } @@ -72,15 +72,15 @@ public boolean isEnabled(VarValuation registers, ParValuation parameters, Consta } // check other parameters - for (Entry e : output.getOutput()) { + for (Entry, SymbolicDataValue> e : output.getOutput()) { if (e.getValue() instanceof Register) { if (!parameters.get(e.getKey()).equals( - registers.get( (Register) e.getValue()))) { + registers.get( (Register) e.getValue()))) { return false; } } else if (e.getValue() instanceof Constant) { if (!parameters.get(e.getKey()).equals( - consts.get( (Constant) e.getValue()))) { + consts.get( (Constant) e.getValue()))) { return false; } } else { diff --git a/core/src/main/java/net/automatalib/automaton/ra/impl/RegisterAutomaton.java b/core/src/main/java/net/automatalib/automaton/ra/impl/RegisterAutomaton.java index ca717fd4f..60ec6b62b 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/impl/RegisterAutomaton.java +++ b/core/src/main/java/net/automatalib/automaton/ra/impl/RegisterAutomaton.java @@ -103,8 +103,8 @@ public Collection getInputStates() { return ret; } - public Collection getRegisters() { - Set regs = new HashSet<>(); + public Collection> getRegisters() { + Set> regs = new HashSet<>(); for (Transition t : getTransitions()) { regs.addAll(t.getAssignment().getAssignment().keySet()); } diff --git a/core/src/main/java/net/automatalib/automaton/ra/impl/TransitionGuard.java b/core/src/main/java/net/automatalib/automaton/ra/impl/TransitionGuard.java index d61204c2f..3766fc1d1 100644 --- a/core/src/main/java/net/automatalib/automaton/ra/impl/TransitionGuard.java +++ b/core/src/main/java/net/automatalib/automaton/ra/impl/TransitionGuard.java @@ -20,10 +20,9 @@ import net.automatalib.automaton.ra.guard.impl.TrueGuardExpression; import net.automatalib.data.Constants; import net.automatalib.data.DataValue; -import net.automatalib.data.Mapping; import net.automatalib.data.ParValuation; import net.automatalib.data.SymbolicDataValue; -import net.automatalib.data.VarMapping; +import net.automatalib.data.Valuation; import net.automatalib.data.VarValuation; /** @@ -54,7 +53,7 @@ public TransitionGuard(GuardExpression condition) { * @return */ public boolean isSatisfied(VarValuation registers, ParValuation parameters, Constants consts) { - Mapping> val = new Mapping<>(); + Valuation, DataValue> val = new Valuation<>(); val.putAll(registers); val.putAll(parameters); val.putAll(consts); diff --git a/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/ExpressionParser.java b/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/ExpressionParser.java index f7e0ef261..87f5bc477 100644 --- a/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/ExpressionParser.java +++ b/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/ExpressionParser.java @@ -37,11 +37,11 @@ public class ExpressionParser { private final String expLine; - private final Map pMap; + private final Map> pMap; private GuardExpression predicate; - public ExpressionParser(String exp, Map pMap) { + public ExpressionParser(String exp, Map> pMap) { expLine = exp.trim(); this.pMap = pMap; @@ -110,9 +110,9 @@ else if (pred.contains(">")) { "this should not happen!!! " + pred + " in " + expLine); } - SymbolicDataValue left = pMap.get(related[0].trim()); - SymbolicDataValue right = pMap.get(related[1].trim()); - return new AtomicGuardExpression(left, relation, right); + SymbolicDataValue left = pMap.get(related[0].trim()); + SymbolicDataValue right = pMap.get(related[1].trim()); + return new AtomicGuardExpression<>(left, relation, right); } /** diff --git a/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonExporter.java b/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonExporter.java index d436d3fb9..1f02eed6a 100644 --- a/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonExporter.java +++ b/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonExporter.java @@ -23,14 +23,14 @@ import java.util.Map; import java.util.Map.Entry; import java.util.Set; -import jakarta.xml.bind.JAXB; +import jakarta.xml.bind.JAXB; import net.automatalib.automaton.ra.Assignment; -import net.automatalib.automaton.ra.impl.RALocation; -import net.automatalib.automaton.ra.impl.Transition; import net.automatalib.automaton.ra.TransitionGuard; import net.automatalib.automaton.ra.impl.OutputMapping; import net.automatalib.automaton.ra.impl.OutputTransition; +import net.automatalib.automaton.ra.impl.RALocation; +import net.automatalib.automaton.ra.impl.Transition; import net.automatalib.data.Constants; import net.automatalib.data.DataType; import net.automatalib.data.DataValue; @@ -39,9 +39,9 @@ import net.automatalib.data.SymbolicDataValue.Parameter; import net.automatalib.data.SymbolicDataValue.Register; import net.automatalib.data.SymbolicDataValueGenerator.ParameterGenerator; +import net.automatalib.symbol.ParameterizedSymbol; import net.automatalib.symbol.impl.InputSymbol; import net.automatalib.symbol.impl.OutputSymbol; -import net.automatalib.symbol.ParameterizedSymbol; /** * @@ -53,26 +53,26 @@ public class RegisterAutomatonExporter { private static RegisterAutomaton.Constants exportConstants(Constants consts) { RegisterAutomaton.Constants ret = factory.createRegisterAutomatonConstants(); - for (Entry> e : consts) { + for (Entry, DataValue> e : consts) { RegisterAutomaton.Constants.Constant c = factory.createRegisterAutomatonConstantsConstant(); c.setName(e.getKey().toString()); c.setType(e.getKey().getType().getName()); - c.setValue(e.getValue().getId().toString()); + c.setValue(e.getValue().getValue().toString()); ret.getConstant().add(c); } return ret; } - private static RegisterAutomaton.Globals exportRegisters(Collection reg, Map extra) { + private static RegisterAutomaton.Globals exportRegisters(Collection> reg, Map> extra) { RegisterAutomaton.Globals ret = factory.createRegisterAutomatonGlobals(); - for (Register r : reg) { + for (Register r : reg) { RegisterAutomaton.Globals.Variable v = factory.createRegisterAutomatonGlobalsVariable(); v.setName(r.toString()); v.setType(r.getType().getName()); v.setValue("0"); ret.getVariable().add(v); } - for (Entry e : extra.entrySet()) { + for (Entry> e : extra.entrySet()) { RegisterAutomaton.Globals.Variable v = factory.createRegisterAutomatonGlobalsVariable(); v.setName(e.getKey()); v.setType(e.getValue().getName()); @@ -88,7 +88,7 @@ private static RegisterAutomaton.Alphabet.Inputs exportInputs(Collection t : input.getPtypes()) { RegisterAutomaton.Alphabet.Inputs.Symbol.Param param = factory.createRegisterAutomatonAlphabetInputsSymbolParam(); param.setName("p" + (idx++)); @@ -106,7 +106,7 @@ private static RegisterAutomaton.Alphabet.Outputs exportOutputs(Collection t : output.getPtypes()) { RegisterAutomaton.Alphabet.Outputs.Symbol.Param param = factory.createRegisterAutomatonAlphabetOutputsSymbolParam(); param.setName("p" + (idx++)); @@ -127,7 +127,7 @@ private static RegisterAutomaton.Locations exportLocations( factory.createRegisterAutomatonLocationsLocation(); l.setName(loc.getName()); - if (ra.getInitialState().equals(loc)) { + if (loc.equals(ra.getInitialState())) { l.setInitial("true"); } ret.getLocation() .add(l); @@ -135,7 +135,7 @@ private static RegisterAutomaton.Locations exportLocations( return ret; } - private static RegisterAutomaton.Transitions exportTransitions(Collection trans, Map tmp) { + private static RegisterAutomaton.Transitions exportTransitions(Collection trans, Map> tmp) { RegisterAutomaton.Transitions ret = factory.createRegisterAutomatonTransitions(); @@ -166,7 +166,7 @@ private static RegisterAutomaton.Transitions.Transition exportInputTransition(Tr } private static RegisterAutomaton.Transitions.Transition exportOutputTransition( - OutputTransition t, Map tmp) { + OutputTransition t, Map> tmp) { RegisterAutomaton.Transitions.Transition ret = factory.createRegisterAutomatonTransitionsTransition(); @@ -183,8 +183,8 @@ private static RegisterAutomaton.Transitions.Transition exportOutputTransition( OutputMapping outMap = t.getOutput(); ParameterGenerator pgen = new ParameterGenerator(); int idx=1; - for (DataType type : t.getLabel().getPtypes()) { - Parameter p = pgen.next(type); + for (DataType type : t.getLabel().getPtypes()) { + Parameter p = pgen.next(type); if (outMap.getFreshParameters().contains(p)) { // find out register that stores parameter @@ -202,7 +202,7 @@ private static RegisterAutomaton.Transitions.Transition exportOutputTransition( } } else { - SymbolicDataValue out = outMap.getOutput().get(p); + SymbolicDataValue out = outMap.getOutput().get(p); // assignments are assumed to happen before // output by the parser if (out instanceof Register) { @@ -247,7 +247,7 @@ private static String exportGuard(TransitionGuard guard) { private static RegisterAutomaton.Transitions.Transition.Assignments exportAssignments(Assignment as) { RegisterAutomaton.Transitions.Transition.Assignments ret = factory.createRegisterAutomatonTransitionsTransitionAssignments(); - for (Entry e : as.getAssignment()) { + for (Entry, ? extends SymbolicDataValue> e : as.getAssignment()) { RegisterAutomaton.Transitions.Transition.Assignments.Assign a = factory.createRegisterAutomatonTransitionsTransitionAssignmentsAssign(); @@ -283,7 +283,7 @@ public static void write(net.automatalib.automaton.ra.impl.RegisterAutomaton ra, RegisterAutomaton.Alphabet acts = factory.createRegisterAutomatonAlphabet(); acts.setInputs(exportInputs(inputs)); acts.setOutputs(exportOutputs(outputs)); - Map tmp = new HashMap<>(); + Map> tmp = new HashMap<>(); ret.setAlphabet(acts); ret.setConstants(exportConstants(c)); ret.setLocations(exportLocations(ra, ra.getStates())); diff --git a/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonImporter.java b/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonImporter.java index 9350716a3..ac8bb1d39 100644 --- a/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonImporter.java +++ b/serialization/xml/src/main/java/net/automatalib/serialization/xml/ra/RegisterAutomatonImporter.java @@ -27,19 +27,17 @@ import java.util.ListIterator; import java.util.Map; import java.util.Set; -import jakarta.xml.bind.JAXB; - -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; +import jakarta.xml.bind.JAXB; +import net.automatalib.alphabet.Alphabet; +import net.automatalib.alphabet.impl.GrowingMapAlphabet; import net.automatalib.automaton.ra.Assignment; import net.automatalib.automaton.ra.impl.InputTransition; import net.automatalib.automaton.ra.impl.MutableRegisterAutomaton; -import net.automatalib.automaton.ra.impl.RALocation; -import net.automatalib.automaton.ra.impl.TransitionGuard; import net.automatalib.automaton.ra.impl.OutputMapping; import net.automatalib.automaton.ra.impl.OutputTransition; -import net.automatalib.serialization.xml.ra.RegisterAutomaton.Transitions.Transition; +import net.automatalib.automaton.ra.impl.RALocation; +import net.automatalib.automaton.ra.impl.TransitionGuard; import net.automatalib.data.Constants; import net.automatalib.data.DataType; import net.automatalib.data.DataValue; @@ -47,16 +45,17 @@ import net.automatalib.data.SymbolicDataValue.Constant; import net.automatalib.data.SymbolicDataValue.Parameter; import net.automatalib.data.SymbolicDataValue.Register; -import net.automatalib.data.VarMapping; -import net.automatalib.data.VarValuation; import net.automatalib.data.SymbolicDataValueGenerator.ConstantGenerator; import net.automatalib.data.SymbolicDataValueGenerator.ParameterGenerator; import net.automatalib.data.SymbolicDataValueGenerator.RegisterGenerator; +import net.automatalib.data.VarMapping; +import net.automatalib.data.VarValuation; +import net.automatalib.serialization.xml.ra.RegisterAutomaton.Transitions.Transition; +import net.automatalib.symbol.ParameterizedSymbol; import net.automatalib.symbol.impl.InputSymbol; import net.automatalib.symbol.impl.OutputSymbol; -import net.automatalib.symbol.ParameterizedSymbol; -import net.automatalib.alphabet.Alphabet; -import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; /** * @@ -68,9 +67,9 @@ public class RegisterAutomatonImporter { private final Map outputSigmaMap = new LinkedHashMap<>(); private final Map paramNames = new LinkedHashMap<>(); private final Map stateMap = new LinkedHashMap<>(); - private final Map constMap = new LinkedHashMap<>(); - private final Map regMap = new LinkedHashMap<>(); - private final Map typeMap = new LinkedHashMap<>(); + private final Map> constMap = new LinkedHashMap<>(); + private final Map> regMap = new LinkedHashMap<>(); + private final Map> typeMap = new LinkedHashMap<>(); // TRUE input locations, FALSE output locations private final Map locationTypeMap = new LinkedHashMap<>(); @@ -83,7 +82,7 @@ public class RegisterAutomatonImporter { private static final Logger LOGGER = LoggerFactory.getLogger(RegisterAutomatonImporter.class); - public Collection getDataTypes() { + public Collection> getDataTypes() { return typeMap.values(); } @@ -144,26 +143,26 @@ private void loadModel(InputStream is) { if (t.getParams() != null) { pnames = t.getParams().split(","); } - Map paramMap = paramMap(ps, pnames); + Map> paramMap = paramMap(ps, pnames); // guard String gstring = t.getGuard(); TransitionGuard p = new TransitionGuard(); if (gstring != null) { - Map map = buildValueMap( - constMap, regMap, (ps instanceof OutputSymbol) ? new LinkedHashMap() : paramMap); + Map> map = buildValueMap( + constMap, regMap, (ps instanceof OutputSymbol) ? new LinkedHashMap>() : paramMap); ExpressionParser parser = new ExpressionParser(gstring, map); p = new TransitionGuard(parser.getPredicate()); } // assignment - Set freshRegs = new HashSet<>(); - VarMapping assignments = new VarMapping<>(); + Set> freshRegs = new HashSet<>(); + VarMapping, SymbolicDataValue> assignments = new VarMapping<>(); if (t.getAssignments() != null) { for (RegisterAutomaton.Transitions.Transition.Assignments.Assign ass : t.getAssignments().getAssign()) { - Register left = regMap.get(ass.to); - SymbolicDataValue right; + Register left = regMap.get(ass.to); + SymbolicDataValue right; if ( ("__fresh__").equals(ass.value)) { freshRegs.add(left); continue; @@ -185,15 +184,15 @@ else if (constMap.containsKey(ass.value)) { // output if (ps instanceof OutputSymbol) { - Parameter[] pList = paramList(ps); + Parameter[] pList = paramList(ps); int idx = 0; - VarMapping outputs = new VarMapping<>(); + VarMapping, SymbolicDataValue> outputs = new VarMapping<>(); for (String s : pnames) { //Parameter param = paramMap.get(s); - Parameter param = pList[idx++]; - SymbolicDataValue source = null; + Parameter param = pList[idx++]; + SymbolicDataValue source = null; if (regMap.containsKey(s)) { - Register r = regMap.get(s); + Register r = regMap.get(s); if (freshRegs.contains(r)) { // add assignment to store fresh value assignments.put(r, param); @@ -216,7 +215,7 @@ else if (constMap.containsKey(ass.value)) { // all unassigned parameters have to be fresh by convention, // we do not allow "don't care" in outputs - Set fresh = new LinkedHashSet<>(paramMap.values()); + Set> fresh = new LinkedHashSet<>(paramMap.values()); fresh.removeAll(outputs.keySet()); OutputMapping outMap = new OutputMapping(fresh, outputs); @@ -243,7 +242,7 @@ private void getAlphabet(RegisterAutomaton.Alphabet a) { for (RegisterAutomaton.Alphabet.Inputs.Symbol s : a.getInputs().getSymbol()) { int pcount = s.getParam().size(); String[] pNames = new String[pcount]; - DataType[] pTypes = new DataType[pcount]; + DataType[] pTypes = new DataType[pcount]; int idx = 0; for (RegisterAutomaton.Alphabet.Inputs.Symbol.Param p : s.getParam()) { pNames[idx] = p.name; @@ -261,7 +260,7 @@ private void getAlphabet(RegisterAutomaton.Alphabet a) { for (RegisterAutomaton.Alphabet.Outputs.Symbol s : a.getOutputs().getSymbol()) { int pcount = s.getParam().size(); String[] pNames = new String[pcount]; - DataType[] pTypes = new DataType[pcount]; + DataType[] pTypes = new DataType[pcount]; int idx = 0; for (RegisterAutomaton.Alphabet.Outputs.Symbol.Param p : s.getParam()) { pNames[idx] = p.name; @@ -280,12 +279,12 @@ private void getAlphabet(RegisterAutomaton.Alphabet a) { private void getConstants(RegisterAutomaton.Constants xml) { ConstantGenerator cgen = new ConstantGenerator(); for (RegisterAutomaton.Constants.Constant def : xml.getConstant()) { - DataType type = getOrCreateType(def.type); - Constant c = cgen.next(type); + DataType type = getOrCreateType(def.type); + Constant c = cgen.next(type); constMap.put(def.value, c); constMap.put(def.name, c); LOGGER.trace("{} ->{}", def.name, c); - DataValue dv = new DataValue(type, Integer.parseInt(def.value)); + DataValue dv = new DataValue(type, Integer.parseInt(def.value)); consts.put(c, dv); } LOGGER.trace("Loading: {}", consts); @@ -294,8 +293,8 @@ private void getConstants(RegisterAutomaton.Constants xml) { private void getRegisters(RegisterAutomaton.Globals g) { RegisterGenerator rgen = new RegisterGenerator(); for (RegisterAutomaton.Globals.Variable def : g.getVariable()) { - DataType type = getOrCreateType(def.type); - Register r = rgen.next(type); + DataType type = getOrCreateType(def.type); + Register r = rgen.next(type); regMap.put(def.name, r); LOGGER.trace("{} ->{}", def.name, r); Object o = null; @@ -311,7 +310,7 @@ private void getRegisters(RegisterAutomaton.Globals g) { "Unsupported Register Type: " + type.getBase().getName()); } - DataValue dv = new DataValue(type, o); + DataValue dv = new DataValue(type, o); initialRegs.put(r, dv); } LOGGER.trace("Loading: {}", initialRegs); @@ -321,11 +320,15 @@ private RegisterAutomaton unmarschall(InputStream is) { return JAXB.unmarshal(is, RegisterAutomaton.class); } - private DataType getOrCreateType(String name) { - DataType t = typeMap.get(name); + private DataType getOrCreateType(String name) { + DataType t = typeMap.get(name); if (t == null) { // TODO: there should be a proper way of specifying java types to be bound - t = new DataType(name, isDoubleTempCheck(name) ? Double.class : Integer.class); + if (isDoubleTempCheck(name)) { + t = new DataType<>(name, Double.class); + } else { + t = new DataType<>(name, Integer.class); + } typeMap.put(name, t); } return t; @@ -335,23 +338,23 @@ private boolean isDoubleTempCheck(String name) { return name.equals("DOUBLE") || name.equals("double"); } - private Map buildValueMap( - Map ... maps) { - Map ret = new LinkedHashMap<>(); - for (Map m : maps) { + private Map> buildValueMap( + Map> ... maps) { + Map> ret = new LinkedHashMap<>(); + for (Map> m : maps) { ret.putAll(m); } return ret; } - private Map paramMap( + private Map> paramMap( ParameterizedSymbol ps, String ... pNames) { if (pNames == null) { pNames = paramNames.get(ps); } - Map ret = new LinkedHashMap<>(); + Map> ret = new LinkedHashMap<>(); ParameterGenerator pgen = new ParameterGenerator(); int idx = 0; for (String name : pNames) { @@ -361,13 +364,13 @@ private Map paramMap( return ret; } - private Parameter[] paramList(ParameterizedSymbol ps) { + private Parameter[] paramList(ParameterizedSymbol ps) { - Parameter[] ret = new Parameter[ps.getArity()]; + Parameter[] ret = new Parameter[ps.getArity()]; ParameterGenerator pgen = new ParameterGenerator(); int idx = 0; - for (DataType t : ps.getPtypes()) { + for (DataType t : ps.getPtypes()) { ret[idx] = pgen.next(t); idx++; }