Skip to content

Commit

Permalink
Use ClockType for clocks instead of RatType
Browse files Browse the repository at this point in the history
  • Loading branch information
@DoriCz
DoriCz committed Dec 18, 2023
1 parent 14aec3d commit 0dd8a53
Show file tree
Hide file tree
Showing 45 changed files with 630 additions and 380 deletions.
40 changes: 20 additions & 20 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,14 @@
import hu.bme.mit.theta.core.clock.constr.UnitLeqConstr;
import hu.bme.mit.theta.core.clock.constr.UnitLtConstr;
import hu.bme.mit.theta.core.decl.VarDecl;
import hu.bme.mit.theta.core.type.rattype.RatType;
import hu.bme.mit.theta.core.type.clocktype.ClockType;

public final class BoundFunc {
private static final int HASH_SEED = 2903;
private static final BoundFunc TOP = BoundFunc.builder().build();

private final Map<VarDecl<RatType>, Integer> varToLower;
private final Map<VarDecl<RatType>, Integer> varToUpper;
private final Map<VarDecl<ClockType>, Integer> varToLower;
private final Map<VarDecl<ClockType>, Integer> varToUpper;

private volatile int hashCode = 0;

Expand All @@ -51,16 +51,16 @@ private BoundFunc(final Builder builder) {
varToUpper = builder.varToUpper;
}

private BoundFunc(final Map<VarDecl<RatType>, Integer> varToLower,
final Map<VarDecl<RatType>, Integer> varToUpper) {
private BoundFunc(final Map<VarDecl<ClockType>, Integer> varToLower,
final Map<VarDecl<ClockType>, Integer> varToUpper) {
this.varToLower = varToLower;
this.varToUpper = varToUpper;
}

public BoundFunc merge(final BoundFunc that) {
checkNotNull(that);
final Map<VarDecl<RatType>, Integer> varToLower = Containers.createMap(this.varToLower);
final Map<VarDecl<RatType>, Integer> varToUpper = Containers.createMap(this.varToUpper);
final Map<VarDecl<ClockType>, Integer> varToLower = Containers.createMap(this.varToLower);
final Map<VarDecl<ClockType>, Integer> varToUpper = Containers.createMap(this.varToUpper);

that.varToLower.forEach((c, b) -> varToLower.merge(c, b, Integer::max));
that.varToUpper.forEach((c, b) -> varToUpper.merge(c, b, Integer::max));
Expand All @@ -80,7 +80,7 @@ public Builder transform() {
return new Builder(this);
}

public Optional<Integer> getLower(final VarDecl<RatType> varDecl) {
public Optional<Integer> getLower(final VarDecl<ClockType> varDecl) {
checkNotNull(varDecl);
if (varDecl.equals(ZeroVar.getInstance())) {
return Optional.of(0);
Expand All @@ -89,7 +89,7 @@ public Optional<Integer> getLower(final VarDecl<RatType> varDecl) {
}
}

public Optional<Integer> getUpper(final VarDecl<RatType> varDecl) {
public Optional<Integer> getUpper(final VarDecl<ClockType> varDecl) {
checkNotNull(varDecl);
if (varDecl.equals(ZeroVar.getInstance())) {
return Optional.of(0);
Expand All @@ -98,11 +98,11 @@ public Optional<Integer> getUpper(final VarDecl<RatType> varDecl) {
}
}

public Collection<VarDecl<RatType>> getLowerVars() {
public Collection<VarDecl<ClockType>> getLowerVars() {
return Collections.unmodifiableCollection(varToLower.keySet());
}

public Collection<VarDecl<RatType>> getUpperVars() {
public Collection<VarDecl<ClockType>> getUpperVars() {
return Collections.unmodifiableCollection(varToUpper.keySet());
}

Expand All @@ -111,7 +111,7 @@ public boolean isLeq(final BoundFunc that) {
return isLeq(this.varToLower, that.varToLower) && isLeq(this.varToUpper, that.varToUpper);
}

private static boolean isLeq(final Map<VarDecl<RatType>, Integer> map1, final Map<VarDecl<RatType>, Integer> map2) {
private static boolean isLeq(final Map<VarDecl<ClockType>, Integer> map1, final Map<VarDecl<ClockType>, Integer> map2) {
return map1.entrySet().stream()
.allMatch(e1 -> map2.containsKey(e1.getKey()) && e1.getValue() <= map2.get(e1.getKey()));
}
Expand Down Expand Up @@ -155,8 +155,8 @@ public String toString() {

public static final class Builder {
private volatile BoundFunc boundFunction;
private final Map<VarDecl<RatType>, Integer> varToLower;
private final Map<VarDecl<RatType>, Integer> varToUpper;
private final Map<VarDecl<ClockType>, Integer> varToLower;
private final Map<VarDecl<ClockType>, Integer> varToUpper;

private Builder() {
this.boundFunction = null;
Expand All @@ -170,7 +170,7 @@ private Builder(final BoundFunc boundFunction) {
this.varToUpper = Containers.createMap(boundFunction.varToUpper);
}

public Builder remove(final VarDecl<RatType> varDecl) {
public Builder remove(final VarDecl<ClockType> varDecl) {
checkState(!isBuilt(), "Already built.");
varToLower.remove(varDecl);
varToUpper.remove(varDecl);
Expand Down Expand Up @@ -205,39 +205,39 @@ private BoundFunctionVarConstrVisitor() {

@Override
public Void visit(final UnitLtConstr constr, final Builder builder) {
final VarDecl<RatType> varDecl = constr.getVar();
final VarDecl<ClockType> varDecl = constr.getVar();
final int bound = constr.getBound();
builder.varToUpper.merge(varDecl, bound, Integer::max);
return null;
}

@Override
public Void visit(final UnitLeqConstr constr, final Builder builder) {
final VarDecl<RatType> varDecl = constr.getVar();
final VarDecl<ClockType> varDecl = constr.getVar();
final int bound = constr.getBound();
builder.varToUpper.merge(varDecl, bound, Integer::max);
return null;
}

@Override
public Void visit(final UnitGtConstr constr, final Builder builder) {
final VarDecl<RatType> varDecl = constr.getVar();
final VarDecl<ClockType> varDecl = constr.getVar();
final int bound = constr.getBound();
builder.varToLower.merge(varDecl, bound, Integer::max);
return null;
}

@Override
public Void visit(final UnitGeqConstr constr, final Builder builder) {
final VarDecl<RatType> varDecl = constr.getVar();
final VarDecl<ClockType> varDecl = constr.getVar();
final int bound = constr.getBound();
builder.varToLower.merge(varDecl, bound, Integer::max);
return null;
}

@Override
public Void visit(final UnitEqConstr constr, final Builder builder) {
final VarDecl<RatType> varDecl = constr.getVar();
final VarDecl<ClockType> varDecl = constr.getVar();
final int bound = constr.getBound();
builder.varToLower.merge(varDecl, bound, Integer::max);
builder.varToUpper.merge(varDecl, bound, Integer::max);
Expand Down
Loading

0 comments on commit 0dd8a53

Please sign in to comment.