Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Overhaul of Inequality Theory #99

Merged
merged 9 commits into from
Apr 2, 2025
+1,972 −1,519
Merged

Overhaul of Inequality Theory #99

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
cf753f2
overhaul of inequality theory
FredrikTaquist Mar 20, 2025
d89603b
add test cases for branch merging
FredrikTaquist Mar 20, 2025
e2a16cd
inequality theory suffix optimization
FredrikTaquist Mar 20, 2025
b3a2f5b
remove commented out code
FredrikTaquist Mar 21, 2025
6531ae2
greater and lesser suffix value restrictions
FredrikTaquist Mar 21, 2025
ddcf9ed
sdt equivalence with via register equality in guard merging
FredrikTaquist Mar 26, 2025
a5a3833
fix indentation and other small fixes
FredrikTaquist Mar 26, 2025
fcbda35
remove commented out code
FredrikTaquist Mar 26, 2025
0650bf6
documentation of guard merging and some small fixes
FredrikTaquist Mar 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions src/main/java/de/learnlib/ralib/automata/guards/AtomicGuardExpression.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,8 @@ public boolean isSatisfied(Mapping<SymbolicDataValue, DataValue<?>> val) {
return !lv.equals(rv);
case BIGGER:
case SMALLER:
case BIGGER_OR_EQUAL:
case SMALLER_OR_EQUAL:
return numCompare(lv, rv, relation);

default:
Expand Down Expand Up @@ -116,8 +118,12 @@ private boolean numCompare(DataValue l, DataValue r, Relation relation) {
switch (relation) {
case SMALLER:
return result < 0;
case SMALLER_OR_EQUAL:
return result <= 0;
case BIGGER:
return result > 0;
case BIGGER_OR_EQUAL:
return result >= 0;

default:
throw new UnsupportedOperationException(
Expand Down
2 changes: 2 additions & 0 deletions src/main/java/de/learnlib/ralib/automata/guards/Relation.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,9 @@
public enum Relation {

SMALLER("<"),
SMALLER_OR_EQUAL("<="),
BIGGER(">"),
BIGGER_OR_EQUAL(">="),
EQUALS("=="),
NOT_EQUALS("!=");

Expand Down
8 changes: 8 additions & 0 deletions src/main/java/de/learnlib/ralib/automata/xml/ExpressionParser.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,10 +96,18 @@ else if (pred.contains("!!")) {
related = pred.split("!!");
relation = Relation.NOT_EQUALS;
}
else if (pred.contains("<=")) {
related = pred.split("<=");
relation = Relation.SMALLER_OR_EQUAL;
}
else if (pred.contains("<")) {
related = pred.split("<");
relation = Relation.SMALLER;
}
else if (pred.contains(">=")) {
related = pred.split(">=");
relation = Relation.BIGGER_OR_EQUAL;
}
else if (pred.contains(">")) {
related = pred.split(">");
relation = Relation.BIGGER;
Expand Down
43 changes: 43 additions & 0 deletions src/main/java/de/learnlib/ralib/oracles/mto/SDT.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@
*/
package de.learnlib.ralib.oracles.mto;

import static de.learnlib.ralib.solver.jconstraints.JContraintsUtil.toExpression;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.LinkedHashMap;
Expand All @@ -42,6 +44,10 @@
import de.learnlib.ralib.theory.SDTMultiGuard;
import de.learnlib.ralib.theory.SDTTrueGuard;
import de.learnlib.ralib.theory.inequality.IntervalGuard;
import gov.nasa.jpf.constraints.api.ConstraintSolver.Result;
import gov.nasa.jpf.constraints.api.Expression;
import gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver;
import gov.nasa.jpf.constraints.util.ExpressionUtil;

/**
* Implementation of Symbolic Decision Trees.
Expand Down Expand Up @@ -168,6 +174,17 @@ public Set<SymbolicDataValue> getVariables() {
return variables;
}

public Set<SuffixValue> getSuffixValues() {
Set<SuffixValue> values = new LinkedHashSet<>();
if (this instanceof SDTLeaf)
return values;
for (Entry<SDTGuard, SDT> e : children.entrySet()) {
values.add(e.getKey().getParameter());
values.addAll(e.getValue().getSuffixValues());
}
return values;
}

@Override
public boolean isAccepting() {
if (this instanceof SDTLeaf) {
Expand Down Expand Up @@ -538,4 +555,30 @@ public SDT copy() {
return new SDT(cc);
}

/**
* Check if a SDT is semantically equivalent to another, given some conditions on the other SDT
*
* @param other - the SDT to compare to
* @param condition - the conditions to apply to other
* @param solver - a constraint solver
*/
public boolean isEquivalentUnderCondition(SDT other, Expression<Boolean> condition, NativeZ3Solver solver) {
Map<GuardExpression, Boolean> expressions = this.getGuardExpressions(new Constants());
Map<GuardExpression, Boolean> otherExpressions = other.getGuardExpressions(new Constants());
for (Map.Entry<GuardExpression, Boolean> entry : expressions.entrySet()) {
Expression<Boolean> x = toExpression(entry.getKey());
Boolean outcome = entry.getValue();
for (Map.Entry<GuardExpression, Boolean> otherEntry : otherExpressions.entrySet()) {
if (outcome != otherEntry.getValue()) {
Expression<Boolean> otherX = toExpression(otherEntry.getKey());
Expression<Boolean> renamed = ExpressionUtil.and(otherX, condition);
Expression<Boolean> con = ExpressionUtil.and(x, renamed);
if (solver.isSatisfiable(con) == Result.SAT) {
return false;
}
}
}
}
return true;
}
}
4 changes: 4 additions & 0 deletions src/main/java/de/learnlib/ralib/solver/jconstraints/JContraintsUtil.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,8 +136,12 @@ public static Expression<Boolean> toExpression(AtomicGuardExpression expr,
return new NumericBooleanExpression(lv, NumericComparator.NE, rv);
case SMALLER:
return new NumericBooleanExpression(lv, NumericComparator.LT, rv);
case SMALLER_OR_EQUAL:
return new NumericBooleanExpression(lv, NumericComparator.LE, rv);
case BIGGER:
return new NumericBooleanExpression(lv, NumericComparator.GT, rv);
case BIGGER_OR_EQUAL:
return new NumericBooleanExpression(lv, NumericComparator.GE, rv);

default:
throw new UnsupportedOperationException(
Expand Down
6 changes: 0 additions & 6 deletions src/main/java/de/learnlib/ralib/theory/SDTAndGuard.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
import java.util.ArrayList;
import java.util.List;
import java.util.Objects;
import java.util.Set;

import de.learnlib.ralib.automata.guards.Conjunction;
import de.learnlib.ralib.automata.guards.GuardExpression;
Expand Down Expand Up @@ -99,11 +98,6 @@ public SDTGuard relabel(VarMapping relabelling) {
return new SDTAndGuard(sv, gg.toArray(new SDTIfGuard[]{}));
}

@Override
public Set<SDTGuard> mergeWith(SDTGuard other, List<SymbolicDataValue> regPotential) {
throw new UnsupportedOperationException("Not supported yet."); //To change body of generated methods, choose Tools | Templates.
}

@Override
public SDTAndGuard copy() {
return new SDTAndGuard(this);
Expand Down
80 changes: 0 additions & 80 deletions src/main/java/de/learnlib/ralib/theory/SDTGuard.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,86 +60,6 @@ public TransitionGuard toTG() {

public abstract SDTGuard relabel(VarMapping relabelling);

public abstract Set<SDTGuard> mergeWith(SDTGuard other, List<SymbolicDataValue> regPotential);

public abstract SDTGuard copy();

// private Set<SDTGuard> mergeIfWith(SDTIfGuard thisIf, SDTIfGuard otherIf) {
// Set<SDTGuard> ifGuard = new LinkedHashSet<>();
// ifGuard.add(otherIf);
// return mergeIfWith(thisIf, ifGuard);
// }
//
// private Set<SDTGuard> mergeIfWith(SDTIfGuard thisIf, Set<SDTGuard> otherOr) {
//// System.out.println("mergeIfWith Set: thisIf " + thisIf + ", otherOr " + otherOr);
// Set<SDTGuard> otherGuards = new LinkedHashSet<>();
// otherGuards.addAll(otherOr);
// if (otherGuards.contains(thisIf.toDeqGuard())) {
//// System.out.println("contradiction");
// otherGuards.remove(thisIf.toDeqGuard());
// // disequality + equality = true
// if (!((thisIf instanceof EqualityGuard) || thisIf instanceof DisequalityGuard)) {
//// System.out.println("neither is eq or deq");
// otherGuards.add(new DisequalityGuard(
// thisIf.getParameter(), thisIf.getRegister()));
// }
// } else {
// otherGuards.add(thisIf);
// }
//// System.out.println("otherGuards " + otherGuards);
// return otherGuards;
// }
//
// private Set<SDTGuard> mergeIfWith(SDTIfGuard thisIf, SDTAndGuard otherAnd) {
// Set<SDTGuard> ifGuard = new LinkedHashSet<>();
// ifGuard.add(thisIf);
// return mergeAndWith(otherAnd, ifGuard);
// }
//
//// private Set<SDTGuard> mergeAndWith(SDTAndGuard thisAnd, SDTAndGuard otherAnd) {
//// Set<SDTGuard> andGuard = new LinkedHashSet<>();
//// andGuard.add(otherAnd);
//// return mergeAndWith(thisAnd, andGuard);
//// }
////
//// private Set<SDTGuard> mergeAndWith(SDTAndGuard thisAnd, SDTIfGuard otherIf) {
//// return mergeIfWith(otherIf, thisAnd);
//// }
// private Set<SDTGuard> mergeAndWith(SDTAndGuard thisAnd, Set<SDTGuard> _merged) {
// //System.out.println(thisAnd + " merges with " + _merged);
// Set<SDTIfGuard> ifs = new LinkedHashSet<>();
// List<SDTGuard> thisGuards = thisAnd.getGuards();
// Set<SDTGuard> merged = new LinkedHashSet<>();
// merged.addAll(_merged);
// for (SDTGuard x : thisGuards) {
// assert x instanceof SDTIfGuard;
// SDTIfGuard ifX = (SDTIfGuard) x;
// if (merged.contains(ifX.toDeqGuard())) {
// merged.remove(ifX.toDeqGuard());
// if (!((ifX instanceof EqualityGuard) || ifX instanceof DisequalityGuard)) {
// merged.add(new DisequalityGuard(ifX.getParameter(), ifX.getRegister()));
// }
// } else {
// ifs.add(ifX);
// }
// }
// if (ifs.size() == 1) {
// merged.addAll(ifs);
// } else if (ifs.size() > 1) {
// merged.add(new SDTAndGuard(thisAnd.parameter, ifs.toArray(new SDTIfGuard[]{})));
//
// }
// //System.out.println("result: " + merged);
// return merged;
// }

// private Set<SDTGuard> mergeOrWith(SDTOrGuard thisOr, SDTIfGuard otherIf) {
// return mergeIfWith(otherIf, thisOr.guardSet);
// }
//
// private Set<SDTGuard> mergeOrWith(SDTOrGuard thisOr, SDTAndGuard otherAnd) {
// return mergeAndWith(otherAnd, thisOr.guardSet);
// }
//public abstract SDTGuard mergeWith(Set<SDTGuard> others);

}
31 changes: 0 additions & 31 deletions src/main/java/de/learnlib/ralib/theory/SDTOrGuard.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
import java.util.ArrayList;
import java.util.List;
import java.util.Objects;
import java.util.Set;

import de.learnlib.ralib.automata.guards.Disjunction;
import de.learnlib.ralib.automata.guards.GuardExpression;
Expand Down Expand Up @@ -98,38 +97,8 @@ public SDTGuard relabel(VarMapping relabelling) {
return new SDTOrGuard(sv, gg.toArray(new SDTGuard[]{}));
}

@Override
public Set<SDTGuard> mergeWith(SDTGuard other, List<SymbolicDataValue> regPotential) {
return other.mergeWith(this, regPotential);
}

@Override
public SDTOrGuard copy() {
return new SDTOrGuard(this);
}

//@Override
//public SDTGuard mergeWith(Set<SDTGuard> _merged) {
// return null;
//}
// Set<SDTGuard> merged = new LinkedHashSet<>();
// merged.addAll(_merged);
// for (SDTGuard x : this.getGuards()) {
// if (x instanceof SDTIfGuard) {
// SDTGuard newGuard = x.mergeWith(merged);
// }
// }
// if (merged.isEmpty()) {
// return new SDTTrueGuard(this.parameter);
// } else {
// SDTGuard[] mergedArr = merged.toArray(new SDTGuard[]{});
// if (mergedArr.length == 1) {
// return mergedArr[0];
// }
// else {
// return new SDTOrGuard(this.parameter, mergedArr);
// }
//
// }
// }
}
12 changes: 1 addition & 11 deletions src/main/java/de/learnlib/ralib/theory/SDTTrueGuard.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,15 +81,11 @@ public boolean equals(Object obj) {
public int hashCode() {
int hash = 5;
hash = 59 * hash + Objects.hashCode(this.getClass());
hash = 59 * hash + Objects.hashCode(parameter);

return hash;
}

@Override
public Set<SDTGuard> mergeWith(SDTGuard other, List<SymbolicDataValue> regPotential) {
throw new IllegalStateException("trying to merge true guard");
}

@Override
public Set<SymbolicDataValue> getComparands(SymbolicDataValue dv) {
return new LinkedHashSet<>();
Expand All @@ -100,10 +96,4 @@ public SDTTrueGuard copy() {
return new SDTTrueGuard(this);
}


// @Override
// public SDTGuard mergeWith(Set<SDTGuard> _merged) {
// return new SDTOrGuard(this.parameter, _merged.toArray(new SDTGuard[]{}));
//
// }
}
24 changes: 0 additions & 24 deletions src/main/java/de/learnlib/ralib/theory/equality/DisequalityGuard.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,7 @@
*/
package de.learnlib.ralib.theory.equality;

import java.util.LinkedHashSet;
import java.util.List;
import java.util.Objects;
import java.util.Set;

import de.learnlib.ralib.automata.guards.AtomicGuardExpression;
import de.learnlib.ralib.automata.guards.GuardExpression;
Expand Down Expand Up @@ -107,27 +104,6 @@ public boolean equals(Object obj) {
return Objects.equals(this.parameter, other.parameter);
}

@Override
public Set<SDTGuard> mergeWith(SDTGuard other, List<SymbolicDataValue> regPotential) {
Set<SDTGuard> guards = new LinkedHashSet<>();
if (other instanceof EqualityGuard) {
if (!(other.equals(this.toDeqGuard()))) {
guards.add(this);
guards.add(other);
}
}
else if (other instanceof DisequalityGuard) {
guards.add(this);
guards.add(other);
}
else {
// System.out.println("attempt to merge " + this + " with " + other);
guards.addAll(other.mergeWith(this, regPotential));

}
return guards;
}

@Override
public SDTGuard copy() {
return new DisequalityGuard(this);
Expand Down
Loading