Skip to content

Commit

Permalink
Minor changes.
Browse files Browse the repository at this point in the history
  • Loading branch information
@pfg666
pfg666 committed Jun 26, 2024
1 parent f5ee896 commit 39661b3
Show file tree
Hide file tree
Showing 6 changed files with 24 additions and 21 deletions.
1 change: 0 additions & 1 deletion src/main/java/de/learnlib/ralib/learning/SymbolicSuffix.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,6 @@ public SymbolicSuffix(Word<ParameterizedSymbol> actions) {
this.restrictions = new LinkedHashMap<>();

SuffixValueGenerator valgen = new SuffixValueGenerator();
int idx = 1;
for (ParameterizedSymbol ps : actions) {
for (DataType t : ps.getPtypes()) {
SuffixValue sv = valgen.next(t);
Expand Down
8 changes: 4 additions & 4 deletions src/main/java/de/learnlib/ralib/oracles/mto/SymbolicSuffixRestrictionBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ public SymbolicSuffixRestrictionBuilder() {


public Map<SuffixValue, SuffixValueRestriction> restrictSuffix(Word<PSymbolInstance> prefix, Word<PSymbolInstance> suffix) {
DataType[] types = DataWords.typesOf(DataWords.actsOf(suffix));
DataType[] types = DataWords.typesOf(DataWords.actsOf(suffix));
Map<SuffixValue, SuffixValueRestriction> restrictions = new LinkedHashMap<>();
SuffixValueGenerator svgen = new SuffixValueGenerator();
for (DataType t : types) {
Expand All @@ -55,7 +55,7 @@ public Map<SuffixValue, SuffixValueRestriction> restrictSuffix(Word<PSymbolInsta
restr = SuffixValueRestriction.genericRestriction(sv, prefix, suffix, consts);
} else {
// theory-specific restrictions
Theory<?> theory = teachers.get(t);
Theory<?> theory = teachers.get(t);
restr = theory.restrictSuffixValue(sv, prefix, suffix, consts);
}
restrictions.put(sv, restr);
Expand All @@ -66,7 +66,7 @@ public Map<SuffixValue, SuffixValueRestriction> restrictSuffix(Word<PSymbolInsta
public SuffixValueRestriction restrictSuffixValue(SDTGuard guard, Map<SuffixValue, SuffixValueRestriction> prior) {
if (teachers == null)
return SuffixValueRestriction.genericRestriction(guard, prior);
Theory theory = teachers.get(guard.getParameter().getType());
Theory<?> theory = teachers.get(guard.getParameter().getType());
return theory.restrictSuffixValue(guard, prior);
}

Expand All @@ -75,7 +75,7 @@ public boolean sdtPathRevealsRegister(List<SDTGuard> path, SymbolicDataValue[] r
return false;
Set<SymbolicDataValue> revealedRegisters = new LinkedHashSet<>();
for (SDTGuard guard : path) {
Theory theory = teachers.get(guard.getParameter().getType());
Theory<?> theory = teachers.get(guard.getParameter().getType());
for (SymbolicDataValue r : registers) {
if (theory.guardRevealsRegister(guard, r)) {
revealedRegisters.add(r);
Expand Down
8 changes: 5 additions & 3 deletions src/main/java/de/learnlib/ralib/theory/EquivalenceClassFilter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,9 @@ public EquivalenceClassFilter(List<DataValue<T>> equivClasses, boolean useOptimi
public List<DataValue<T>> toList(SuffixValueRestriction restr,
Word<PSymbolInstance> prefix, Word<ParameterizedSymbol> suffix, WordValuation valuation) {

if (!useOptimization)
if (!useOptimization) {
return equivClasses;
}

List<DataValue<T>> filtered = new ArrayList<>();

Expand All @@ -51,14 +52,15 @@ public List<DataValue<T>> toList(SuffixValueRestriction restr,
for (int i = 0; i < dts.length; i++) {
SuffixValue sv = svgen.next(dts[i]);
DataValue<?> val = valuation.get(sv.getId());
if (val != null)
if (val != null) {
mapping.put(sv, val);
}
}
}

GuardExpression expr = restr.toGuardExpression(mapping.keySet());
for (DataValue<T> ec : equivClasses) {
Mapping<SymbolicDataValue, DataValue<?>> ecMapping = new Mapping<SymbolicDataValue, DataValue<?>>();
Mapping<SymbolicDataValue, DataValue<?>> ecMapping = new Mapping<>();
ecMapping.putAll(mapping);
ecMapping.put(restr.getParameter(), ec);
if (expr.isSatisfied(ecMapping)) {
Expand Down
13 changes: 7 additions & 6 deletions src/main/java/de/learnlib/ralib/theory/SuffixValueRestriction.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,19 +54,20 @@ public SuffixValue getParameter() {
* @return
*/
public static SuffixValueRestriction genericRestriction(SuffixValue sv, Word<PSymbolInstance> prefix, Word<PSymbolInstance> suffix, Constants consts) {
DataValue[] prefixVals = DataWords.valsOf(prefix);
DataValue[] suffixVals = DataWords.valsOf(suffix);
DataValue<?>[] prefixVals = DataWords.valsOf(prefix);
DataValue<?>[] suffixVals = DataWords.valsOf(suffix);
DataType[] prefixTypes = DataWords.typesOf(DataWords.actsOf(prefix));
DataType[] suffixTypes = DataWords.typesOf(DataWords.actsOf(suffix));
DataValue val = suffixVals[sv.getId()-1];
int arityFirst = suffix.length() > 0 ? suffix.getSymbol(0).getBaseSymbol().getArity() : 0;
DataValue<?> val = suffixVals[sv.getId()-1];
int firstSymbolArity = suffix.length() > 0 ? suffix.getSymbol(0).getBaseSymbol().getArity() : 0;

boolean unrestricted = false;
for (int i = 0; i < prefixVals.length; i++) {
DataValue<?> dv = prefixVals[i];
DataType dt = prefixTypes[i];
if (dt.equals(sv.getType()) && dv.equals(val))
if (dt.equals(sv.getType()) && dv.equals(val)) {
unrestricted = true;
}
}
if (consts.containsValue(val)) {
unrestricted = true;
Expand All @@ -76,7 +77,7 @@ public static SuffixValueRestriction genericRestriction(SuffixValue sv, Word<PSy
for (int i = 0; i < sv.getId()-1 && !equalsSuffixValue; i++) {
DataType dt = suffixTypes[i];
if (dt.equals(sv.getType()) && suffixVals[i].equals(val)) {
if (sv.getId() <= arityFirst) {
if (sv.getId() <= firstSymbolArity) {
unrestricted = true;
} else {
equalsSuffixValue = true;
Expand Down
12 changes: 6 additions & 6 deletions src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ private Map<SDTGuard, SDT> mergeGuards(Map<EqualityGuard, SDT> eqs, SDTAndGuard
EqualityGuard eqGuard = e.getKey();
LOGGER.trace("comparing guards: " + eqGuard.toString() + " to " + deqGuard.toString()
+ "\nSDT : " + eqSdt.toString() + "\nto SDT : " + deqSdt.toString());
List<SDTIfGuard> ds = new ArrayList();
List<SDTIfGuard> ds = new ArrayList<>();
ds.add(eqGuard);
LOGGER.trace("remapping: " + ds.toString());
if (!(eqSdt.isEquivalentUnder(deqSdt, ds))) {
Expand Down Expand Up @@ -172,7 +172,7 @@ public SDT treeQuery(Word<PSymbolInstance> prefix, SymbolicSuffix suffix, WordVa
List<DataValue<T>> potList = new ArrayList<>(potSet);
List<DataValue<T>> potential = getPotential(potList);

DataValue fresh = getFreshValue(potential);
DataValue<T> fresh = getFreshValue(potential);

List<DataValue<T>> equivClasses = new ArrayList<>(potSet);
equivClasses.add(fresh);
Expand Down Expand Up @@ -342,7 +342,7 @@ private EqualityGuard pickupDataValue(DataValue<T> newDv, List<DataValue> prefix
public DataValue instantiate(Word<PSymbolInstance> prefix, ParameterizedSymbol ps, PIV piv, ParValuation pval,
Constants constants, SDTGuard guard, Parameter param, Set<DataValue<T>> oldDvs) {

List<DataValue> prefixValues = Arrays.asList(DataWords.valsOf(prefix));
List<DataValue<?>> prefixValues = Arrays.asList(DataWords.valsOf(prefix));
LOGGER.trace("prefix values : " + prefixValues.toString());
DataType type = param.getType();
Deque<SDTGuard> guards = new LinkedList<>();
Expand Down Expand Up @@ -372,15 +372,15 @@ public DataValue instantiate(Word<PSymbolInstance> prefix, ParameterizedSymbol p
}
}

Collection potSet = DataWords.<T>joinValsToSet(constants.<T>values(type), DataWords.<T>valSet(prefix, type),
Collection<DataValue<T>> potSet = DataWords.<T>joinValsToSet(constants.<T>values(type), DataWords.<T>valSet(prefix, type),
pval.<T>values(type));

if (!potSet.isEmpty()) {
LOGGER.trace("potSet = " + potSet.toString());
} else {
LOGGER.trace("potSet is empty");
}
DataValue fresh = this.getFreshValue(new ArrayList<DataValue<T>>(potSet));
DataValue<T> fresh = this.getFreshValue(new ArrayList<DataValue<T>>(potSet));
LOGGER.trace("fresh = " + fresh.toString());
return fresh;

Expand Down Expand Up @@ -417,7 +417,7 @@ private Word<PSymbolInstance> buildQuery(Word<PSymbolInstance> prefix, SymbolicS
if (base + a.getArity() > values.size()) {
break;
}
DataValue[] vals = new DataValue[a.getArity()];
DataValue<?>[] vals = new DataValue[a.getArity()];
for (int i = 0; i < a.getArity(); i++) {
vals[i] = values.get(base + i + 1);
}
Expand Down
3 changes: 2 additions & 1 deletion src/main/java/de/learnlib/ralib/words/DataWords.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,8 @@ public static <T> Set<DataValue<T>> valSet(Word<PSymbolInstance> word, DataType
* @param in
* @return
*/
public static <T> Set<DataValue<T>> joinValsToSet(Collection<DataValue<T>> ... in) {
@SafeVarargs
public static <T> Set<DataValue<T>> joinValsToSet(Collection<DataValue<T>> ... in) {
Set<DataValue<T>> vals = new LinkedHashSet<>();
for (Collection<DataValue<T>> s : in) {
vals.addAll(s);
Expand Down

0 comments on commit 39661b3

Please sign in to comment.