From 0dd8a53fcfbf674ad6d735d673199b91afe3f039 Mon Sep 17 00:00:00 2001 From: DoriCz Date: Mon, 18 Dec 2023 15:25:40 +0100 Subject: [PATCH] Use ClockType for clocks instead of RatType --- .../mit/theta/analysis/zone/BoundFunc.java | 40 ++-- .../hu/bme/mit/theta/analysis/zone/DBM.java | 146 +++++++------- .../mit/theta/analysis/zone/DbmSignature.java | 36 ++-- .../mit/theta/analysis/zone/DiffBounds.java | 4 +- .../bme/mit/theta/analysis/zone/ZeroVar.java | 8 +- .../bme/mit/theta/analysis/zone/ZonePrec.java | 10 +- .../mit/theta/analysis/zone/ZoneState.java | 30 +-- .../theta/core/clock/constr/AndConstr.java | 6 +- .../theta/core/clock/constr/ClockConstr.java | 4 +- .../theta/core/clock/constr/ClockConstrs.java | 178 +++++++++++++++--- .../theta/core/clock/constr/DiffConstr.java | 14 +- .../theta/core/clock/constr/DiffEqConstr.java | 24 +-- .../core/clock/constr/DiffGeqConstr.java | 24 +-- .../theta/core/clock/constr/DiffGtConstr.java | 24 +-- .../core/clock/constr/DiffLeqConstr.java | 24 +-- .../theta/core/clock/constr/DiffLtConstr.java | 24 +-- .../theta/core/clock/constr/FalseConstr.java | 4 +- .../theta/core/clock/constr/TrueConstr.java | 4 +- .../theta/core/clock/constr/UnitConstr.java | 10 +- .../theta/core/clock/constr/UnitEqConstr.java | 17 +- .../core/clock/constr/UnitGeqConstr.java | 17 +- .../theta/core/clock/constr/UnitGtConstr.java | 17 +- .../core/clock/constr/UnitLeqConstr.java | 17 +- .../theta/core/clock/constr/UnitLtConstr.java | 17 +- .../bme/mit/theta/core/clock/op/ClockOp.java | 4 +- .../bme/mit/theta/core/clock/op/ClockOps.java | 34 +++- .../bme/mit/theta/core/clock/op/CopyOp.java | 20 +- .../bme/mit/theta/core/clock/op/FreeOp.java | 16 +- .../bme/mit/theta/core/clock/op/GuardOp.java | 4 +- .../bme/mit/theta/core/clock/op/ResetOp.java | 21 +-- .../bme/mit/theta/core/clock/op/ShiftOp.java | 19 +- .../theta/solver/z3/Z3ExprTransformer.java | 49 +++++ .../theta/solver/z3/Z3TypeTransformer.java | 3 + .../bme/mit/theta/xta/analysis/XtaAction.java | 22 +-- .../xta/analysis/zone/XtaActZoneUtils.java | 12 +- .../xta/analysis/zone/XtaLuZoneUtils.java | 4 +- .../theta/xta/analysis/zone/XtaZoneUtils.java | 6 +- .../xta/analysis/zone/lu/LuZoneState.java | 31 +-- .../main/java/hu/bme/mit/theta/xta/Guard.java | 5 +- .../java/hu/bme/mit/theta/xta/XtaProcess.java | 4 +- .../java/hu/bme/mit/theta/xta/XtaSystem.java | 10 +- .../bme/mit/theta/xta/dsl/XtaExpression.java | 25 +++ .../mit/theta/xta/dsl/XtaProcessSymbol.java | 4 +- .../mit/theta/xta/dsl/XtaSpecification.java | 4 +- .../mit/theta/xta/dsl/XtaVariableSymbol.java | 14 +- 45 files changed, 630 insertions(+), 380 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java index 45765cda73..be2f550dd8 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BoundFunc.java @@ -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, Integer> varToLower; - private final Map, Integer> varToUpper; + private final Map, Integer> varToLower; + private final Map, Integer> varToUpper; private volatile int hashCode = 0; @@ -51,16 +51,16 @@ private BoundFunc(final Builder builder) { varToUpper = builder.varToUpper; } - private BoundFunc(final Map, Integer> varToLower, - final Map, Integer> varToUpper) { + private BoundFunc(final Map, Integer> varToLower, + final Map, Integer> varToUpper) { this.varToLower = varToLower; this.varToUpper = varToUpper; } public BoundFunc merge(final BoundFunc that) { checkNotNull(that); - final Map, Integer> varToLower = Containers.createMap(this.varToLower); - final Map, Integer> varToUpper = Containers.createMap(this.varToUpper); + final Map, Integer> varToLower = Containers.createMap(this.varToLower); + final Map, 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)); @@ -80,7 +80,7 @@ public Builder transform() { return new Builder(this); } - public Optional getLower(final VarDecl varDecl) { + public Optional getLower(final VarDecl varDecl) { checkNotNull(varDecl); if (varDecl.equals(ZeroVar.getInstance())) { return Optional.of(0); @@ -89,7 +89,7 @@ public Optional getLower(final VarDecl varDecl) { } } - public Optional getUpper(final VarDecl varDecl) { + public Optional getUpper(final VarDecl varDecl) { checkNotNull(varDecl); if (varDecl.equals(ZeroVar.getInstance())) { return Optional.of(0); @@ -98,11 +98,11 @@ public Optional getUpper(final VarDecl varDecl) { } } - public Collection> getLowerVars() { + public Collection> getLowerVars() { return Collections.unmodifiableCollection(varToLower.keySet()); } - public Collection> getUpperVars() { + public Collection> getUpperVars() { return Collections.unmodifiableCollection(varToUpper.keySet()); } @@ -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, Integer> map1, final Map, Integer> map2) { + private static boolean isLeq(final Map, Integer> map1, final Map, Integer> map2) { return map1.entrySet().stream() .allMatch(e1 -> map2.containsKey(e1.getKey()) && e1.getValue() <= map2.get(e1.getKey())); } @@ -155,8 +155,8 @@ public String toString() { public static final class Builder { private volatile BoundFunc boundFunction; - private final Map, Integer> varToLower; - private final Map, Integer> varToUpper; + private final Map, Integer> varToLower; + private final Map, Integer> varToUpper; private Builder() { this.boundFunction = null; @@ -170,7 +170,7 @@ private Builder(final BoundFunc boundFunction) { this.varToUpper = Containers.createMap(boundFunction.varToUpper); } - public Builder remove(final VarDecl varDecl) { + public Builder remove(final VarDecl varDecl) { checkState(!isBuilt(), "Already built."); varToLower.remove(varDecl); varToUpper.remove(varDecl); @@ -205,7 +205,7 @@ private BoundFunctionVarConstrVisitor() { @Override public Void visit(final UnitLtConstr constr, final Builder builder) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); final int bound = constr.getBound(); builder.varToUpper.merge(varDecl, bound, Integer::max); return null; @@ -213,7 +213,7 @@ public Void visit(final UnitLtConstr constr, final Builder builder) { @Override public Void visit(final UnitLeqConstr constr, final Builder builder) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); final int bound = constr.getBound(); builder.varToUpper.merge(varDecl, bound, Integer::max); return null; @@ -221,7 +221,7 @@ public Void visit(final UnitLeqConstr constr, final Builder builder) { @Override public Void visit(final UnitGtConstr constr, final Builder builder) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); final int bound = constr.getBound(); builder.varToLower.merge(varDecl, bound, Integer::max); return null; @@ -229,7 +229,7 @@ public Void visit(final UnitGtConstr constr, final Builder builder) { @Override public Void visit(final UnitGeqConstr constr, final Builder builder) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); final int bound = constr.getBound(); builder.varToLower.merge(varDecl, bound, Integer::max); return null; @@ -237,7 +237,7 @@ public Void visit(final UnitGeqConstr constr, final Builder builder) { @Override public Void visit(final UnitEqConstr constr, final Builder builder) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); final int bound = constr.getBound(); builder.varToLower.merge(varDecl, bound, Integer::max); builder.varToUpper.merge(varDecl, bound, Integer::max); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java index 2afd5ce14e..d0de5ad75f 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java @@ -63,7 +63,7 @@ import hu.bme.mit.theta.core.clock.op.ResetOp; import hu.bme.mit.theta.core.clock.op.ShiftOp; 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; final class DBM { @@ -89,7 +89,7 @@ private DBM(final DbmSignature signature, final BasicDbm dbm) { // TODO replace BiFunction by IntBiFunction private DBM(final DbmSignature signature, - final BiFunction, ? super VarDecl, ? extends Integer> values) { + final BiFunction, ? super VarDecl, ? extends Integer> values) { this(signature, (final int x, final int y) -> { return values.apply(signature.getVar(x), signature.getVar(y)); }); @@ -107,13 +107,13 @@ public Collection complement() { if (!dbm.isConsistent()) { result.add(DBM.top(Collections.emptySet())); } else { - for (final VarDecl x : signature) { - for (final VarDecl y : signature) { + for (final VarDecl x : signature) { + for (final VarDecl y : signature) { final int bound = get(x, y); if (bound != defaultBound(x, y)) { final int newBound = negate(bound); final DbmSignature newSignature = DbmSignature.over(Arrays.asList(x, y)); - final BiFunction, VarDecl, Integer> newValues = (c1, + final BiFunction, VarDecl, Integer> newValues = (c1, c2) -> (c1 == y && c2 == x) ? newBound : defaultBound(c1, c2); final DBM newDBM = new DBM(newSignature, newValues); result.add(newDBM); @@ -131,22 +131,22 @@ public static DBM copyOf(final DBM dbm) { return new DBM(dbm); } - public static DBM zero(final Iterable> vars) { + public static DBM zero(final Iterable> vars) { checkNotNull(vars); return new DBM(DbmSignature.over(vars), ZERO_DBM_VALUES); } - public static DBM top(final Iterable> vars) { + public static DBM top(final Iterable> vars) { checkNotNull(vars); return new DBM(DbmSignature.over(vars), TOP_DBM_VALUES); } - public static DBM bottom(final Iterable> vars) { + public static DBM bottom(final Iterable> vars) { checkNotNull(vars); return new DBM(DbmSignature.over(vars), BOTTOM_DBM_VALUES); } - public static DBM project(final DBM dbm, final Iterable> vars) { + public static DBM project(final DBM dbm, final Iterable> vars) { checkNotNull(vars); return new DBM(DbmSignature.over(vars), dbm::getOrDefault); } @@ -158,7 +158,7 @@ public static DBM intersection(final DBM dbm1, final DBM dbm2) { checkNotNull(dbm2); final DbmSignature signature = DbmSignature.union(dbm1.signature, dbm2.signature); - final BiFunction, VarDecl, Integer> values = (x, y) -> { + final BiFunction, VarDecl, Integer> values = (x, y) -> { final int bound1 = dbm1.getOrDefault(x, y); final int bound2 = dbm2.getOrDefault(x, y); return min(bound1, bound2); @@ -175,7 +175,7 @@ public static DBM enclosure(final DBM dbm1, final DBM dbm2) { checkNotNull(dbm2); final DbmSignature signature = DbmSignature.union(dbm1.signature, dbm2.signature); - final BiFunction, VarDecl, Integer> values = (x, y) -> { + final BiFunction, VarDecl, Integer> values = (x, y) -> { final int bound1 = dbm1.getOrDefault(x, y); final int bound2 = dbm2.getOrDefault(x, y); return max(bound1, bound2); @@ -205,7 +205,7 @@ public static DBM weakInterpolant(final DBM dbmA, final DBM dbmB) { assert dbmB.isClosed(); final DbmSignature interpolantSignature = interpolantSignature(dbmA, dbmB); - final BiFunction, VarDecl, Integer> values = (x, y) -> { + final BiFunction, VarDecl, Integer> values = (x, y) -> { final int bound1 = dbmA.get(x, y); final int bound2 = dbmB.get(x, y); return min(bound1, bound2); @@ -220,8 +220,8 @@ public static DBM weakInterpolant(final DBM dbmA, final DBM dbmB) { if (cycle.length == 3) { final int x = cycle[0]; final int y = cycle[1]; - final VarDecl leftVar = interpolantSignature.getVar(x); - final VarDecl rightVar = interpolantSignature.getVar(y); + final VarDecl leftVar = interpolantSignature.getVar(x); + final VarDecl rightVar = interpolantSignature.getVar(y); final int boundA1 = dbmA.get(leftVar, rightVar); final int boundB1 = dbmB.get(leftVar, rightVar); if (boundA1 < boundB1) { @@ -239,8 +239,8 @@ public static DBM weakInterpolant(final DBM dbmA, final DBM dbmB) { for (int i = 0; i + 1 < cycle.length; i++) { final int x = cycle[i]; final int y = cycle[i + 1]; - final VarDecl leftVar = interpolantSignature.getVar(x); - final VarDecl rightVar = interpolantSignature.getVar(y); + final VarDecl leftVar = interpolantSignature.getVar(x); + final VarDecl rightVar = interpolantSignature.getVar(y); final int boundA = dbmA.get(leftVar, rightVar); final int boundB = dbmB.get(leftVar, rightVar); if (boundA < boundB) { @@ -274,7 +274,7 @@ public static DBM interpolant(final DBM dbmA, final DBM dbmB) { assert dbmB.isClosed(); final DbmSignature interpolantSignature = interpolantSignature(dbmA, dbmB); - final BiFunction, VarDecl, Integer> values = (x, y) -> { + final BiFunction, VarDecl, Integer> values = (x, y) -> { final int bound1 = dbmA.get(x, y); final int bound2 = dbmB.get(x, y); return min(bound1, bound2); @@ -290,8 +290,8 @@ public static DBM interpolant(final DBM dbmA, final DBM dbmB) { for (int i = 0; i + 1 < cycle.length; i++) { final int x = cycle[i]; final int y = cycle[i + 1]; - final VarDecl leftVar = interpolantSignature.getVar(x); - final VarDecl rightVar = interpolantSignature.getVar(y); + final VarDecl leftVar = interpolantSignature.getVar(x); + final VarDecl rightVar = interpolantSignature.getVar(y); final int boundA = dbmA.get(leftVar, rightVar); final int boundB = dbmB.get(leftVar, rightVar); if (boundA < boundB) { @@ -307,16 +307,16 @@ public static DBM interpolant(final DBM dbmA, final DBM dbmB) { } private static DbmSignature signatureFrom(final DbmSignature interpolantSignature, final int[] cycle) { - final Collection> vars = new ArrayList<>(); + final Collection> vars = new ArrayList<>(); for (int i = 0; i + 1 < cycle.length; i++) { - final VarDecl varDecl = interpolantSignature.getVar(cycle[i]); + final VarDecl varDecl = interpolantSignature.getVar(cycle[i]); vars.add(varDecl); } return DbmSignature.over(vars); } private static DbmSignature interpolantSignature(final DBM dbmA, final DBM dbmB) { - final Set> varsConstrainedByBothDBMS = Sets + final Set> varsConstrainedByBothDBMS = Sets .intersection(dbmA.signature.toSet(), dbmB.signature.toSet()).stream() .filter(c -> dbmA.constrains(c) && dbmB.constrains(c)).collect(Collectors.toSet()); return DbmSignature.over(varsConstrainedByBothDBMS); @@ -324,7 +324,7 @@ private static DbmSignature interpolantSignature(final DBM dbmA, final DBM dbmB) //// - private int getOrDefault(final VarDecl x, final VarDecl y) { + private int getOrDefault(final VarDecl x, final VarDecl y) { if (!tracks(x) || !tracks(y)) { return defaultBound(x, y); } else { @@ -332,7 +332,7 @@ private int getOrDefault(final VarDecl x, final VarDecl y) { } } - private void set(final VarDecl x, final VarDecl y, final int b) { + private void set(final VarDecl x, final VarDecl y, final int b) { checkArgument(tracks(x), "Var not tracked"); checkArgument(tracks(y), "Var not tracked"); final int i = signature.indexOf(x); @@ -340,7 +340,7 @@ private void set(final VarDecl x, final VarDecl y, final int b dbm.set(i, j, b); } - private int get(final VarDecl x, final VarDecl y) { + private int get(final VarDecl x, final VarDecl y) { checkArgument(tracks(x), "Var not tracked"); checkArgument(tracks(y), "Var not tracked"); final int i = signature.indexOf(x); @@ -348,7 +348,7 @@ private int get(final VarDecl x, final VarDecl y) { return dbm.get(i, j); } - private static int defaultBound(final VarDecl x, final VarDecl y) { + private static int defaultBound(final VarDecl x, final VarDecl y) { if (x.equals(y)) { return Leq(0); } else { @@ -377,13 +377,13 @@ public boolean isSatisfied(final ClockConstr constr) { } public DbmRelation getRelation(final DBM that) { - final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); + final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); boolean leq = true; boolean geq = true; - for (final VarDecl x : vars) { - for (final VarDecl y : vars) { + for (final VarDecl x : vars) { + for (final VarDecl y : vars) { leq = leq && this.getOrDefault(x, y) <= that.getOrDefault(x, y); geq = geq && this.getOrDefault(x, y) >= that.getOrDefault(x, y); } @@ -392,10 +392,10 @@ public DbmRelation getRelation(final DBM that) { } public boolean isLeq(final DBM that) { - final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); + final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); - for (final VarDecl x : vars) { - for (final VarDecl y : vars) { + for (final VarDecl x : vars) { + for (final VarDecl y : vars) { if (this.getOrDefault(x, y) > that.getOrDefault(x, y)) { return false; } @@ -405,15 +405,15 @@ public boolean isLeq(final DBM that) { return true; } - public boolean isLeq(final DBM that, final Collection> activeVars) { - final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); + public boolean isLeq(final DBM that, final Collection> activeVars) { + final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); - for (final VarDecl x : vars) { + for (final VarDecl x : vars) { if (!activeVars.contains(x)) { continue; } - for (final VarDecl y : vars) { + for (final VarDecl y : vars) { if (!activeVars.contains(y)) { continue; } @@ -428,7 +428,7 @@ public boolean isLeq(final DBM that, final Collection } public boolean isLeq(final DBM that, final BoundFunc bound) { - final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); + final Set> vars = Sets.union(this.signature.toSet(), that.signature.toSet()); if (!this.isConsistent()) { return true; @@ -438,8 +438,8 @@ public boolean isLeq(final DBM that, final BoundFunc bound) { return false; } - for (final VarDecl x : vars) { - final VarDecl zero = ZeroVar.getInstance(); + for (final VarDecl x : vars) { + final VarDecl zero = ZeroVar.getInstance(); final int Zx0 = this.get(zero, x); final int leqMinusUx = LeqMinusUx(x, bound); @@ -449,7 +449,7 @@ public boolean isLeq(final DBM that, final BoundFunc bound) { continue; } - for (final VarDecl y : vars) { + for (final VarDecl y : vars) { final int Zxy = this.get(y, x); final int Zpxy = that.get(y, x); @@ -469,19 +469,19 @@ public boolean isLeq(final DBM that, final BoundFunc bound) { return true; } - private static final int LeqMinusUx(final VarDecl x, final BoundFunc boundFunction) { + private static final int LeqMinusUx(final VarDecl x, final BoundFunc boundFunction) { return boundFunction.getUpper(x).map(Ux -> Leq(-Ux)).orElse(Inf()); } - private static final int LtMinusLy(final VarDecl y, final BoundFunc boundFunction) { + private static final int LtMinusLy(final VarDecl y, final BoundFunc boundFunction) { return boundFunction.getLower(y).map(Ly -> Lt(-Ly)).orElse(Inf()); } public Collection getConstrs() { final Collection result = Containers.createSet(); - for (final VarDecl leftVar : signature) { - for (final VarDecl rightVar : signature) { + for (final VarDecl leftVar : signature) { + for (final VarDecl rightVar : signature) { final int b = get(leftVar, rightVar); final ClockConstr constr = DiffBounds.toConstr(leftVar, rightVar, b); @@ -522,7 +522,7 @@ public void and(final ClockConstr constr) { constr.accept(AndOperationVisitor.INSTANCE, this); } - public void free(final VarDecl varDecl) { + public void free(final VarDecl varDecl) { checkNotNull(varDecl); checkArgument(!isZeroClock(varDecl), "Var is zero"); ifTracks(varDecl, dbm::free); @@ -532,13 +532,13 @@ public void free() { dbm.free(); } - public void reset(final VarDecl varDecl, final int m) { + public void reset(final VarDecl varDecl, final int m) { checkNotNull(varDecl); checkArgument(!isZeroClock(varDecl), "Var is zero"); ifTracks(varDecl, x -> dbm.reset(x, m)); } - public void copy(final VarDecl lhs, final VarDecl rhs) { + public void copy(final VarDecl lhs, final VarDecl rhs) { checkNotNull(lhs); checkNotNull(rhs); checkArgument(!isZeroClock(lhs), "Var is zero"); @@ -546,16 +546,16 @@ public void copy(final VarDecl lhs, final VarDecl rhs) { ifTracks(lhs, x -> ifTracksElse(rhs, y -> dbm.copy(x, y), () -> dbm.free(x))); } - public void shift(final VarDecl varDecl, final int m) { + public void shift(final VarDecl varDecl, final int m) { checkNotNull(varDecl); checkArgument(!isZeroClock(varDecl), "Var is zero"); ifTracks(varDecl, x -> dbm.shift(x, m)); } - public void norm(final Map, ? extends Integer> bounds) { + public void norm(final Map, ? extends Integer> bounds) { final int[] k = new int[signature.size()]; for (int i = 0; i < signature.size(); i++) { - final VarDecl varDecl = signature.getVar(i); + final VarDecl varDecl = signature.getVar(i); final Integer bound = bounds.get(varDecl); if (bound != null) { k[i] = bound; @@ -603,14 +603,14 @@ public String toString() { final StringBuilder sb = new StringBuilder(); sb.append(String.format("%-12s", "")); - for (final VarDecl varDecl : signature) { + for (final VarDecl varDecl : signature) { sb.append(String.format("%-12s", varDecl.getName())); } sb.append(System.lineSeparator()); - for (final VarDecl x : signature) { + for (final VarDecl x : signature) { sb.append(String.format("%-12s", x.getName())); - for (final VarDecl y : signature) { + for (final VarDecl y : signature) { sb.append(String.format("%-12s", asString(get(x, y)))); } sb.append(System.lineSeparator()); @@ -620,19 +620,19 @@ public String toString() { //// - private boolean tracks(final VarDecl varDecl) { + private boolean tracks(final VarDecl varDecl) { checkNotNull(varDecl); return signature.contains(varDecl); } - private void ifTracks(final VarDecl varDecl, final IntConsumer consumer) { + private void ifTracks(final VarDecl varDecl, final IntConsumer consumer) { if (tracks(varDecl)) { final int x = signature.indexOf(varDecl); consumer.accept(x); } } - private void ifTracksElse(final VarDecl varDecl, final IntConsumer consumer, final Procedure procedure) { + private void ifTracksElse(final VarDecl varDecl, final IntConsumer consumer, final Procedure procedure) { if (tracks(varDecl)) { final int x = signature.indexOf(varDecl); consumer.accept(x); @@ -641,12 +641,12 @@ private void ifTracksElse(final VarDecl varDecl, final IntConsumer cons } } - private boolean constrains(final VarDecl varDecl) { + private boolean constrains(final VarDecl varDecl) { checkNotNull(varDecl); return this.tracks(varDecl) && dbm.constrains(signature.indexOf(varDecl)); } - private boolean isZeroClock(final VarDecl varDecl) { + private boolean isZeroClock(final VarDecl varDecl) { return varDecl.equals(ZeroVar.getInstance()); } @@ -713,7 +713,7 @@ public Void visit(final FalseConstr constr, final DBM dbm) { @Override public Void visit(final UnitLtConstr constr, final DBM dbm) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); if (dbm.tracks(varDecl)) { final int x = dbm.signature.indexOf(varDecl); final int m = constr.getBound(); @@ -724,7 +724,7 @@ public Void visit(final UnitLtConstr constr, final DBM dbm) { @Override public Void visit(final UnitLeqConstr constr, final DBM dbm) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); if (dbm.tracks(varDecl)) { final int x = dbm.signature.indexOf(varDecl); final int m = constr.getBound(); @@ -735,7 +735,7 @@ public Void visit(final UnitLeqConstr constr, final DBM dbm) { @Override public Void visit(final UnitGtConstr constr, final DBM dbm) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); if (dbm.tracks(varDecl)) { final int x = dbm.signature.indexOf(varDecl); final int m = constr.getBound(); @@ -746,7 +746,7 @@ public Void visit(final UnitGtConstr constr, final DBM dbm) { @Override public Void visit(final UnitGeqConstr constr, final DBM dbm) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); if (dbm.tracks(varDecl)) { final int x = dbm.signature.indexOf(varDecl); final int m = constr.getBound(); @@ -757,7 +757,7 @@ public Void visit(final UnitGeqConstr constr, final DBM dbm) { @Override public Void visit(final UnitEqConstr constr, final DBM dbm) { - final VarDecl varDecl = constr.getVar(); + final VarDecl varDecl = constr.getVar(); if (dbm.tracks(varDecl)) { final int x = dbm.signature.indexOf(varDecl); final int m = constr.getBound(); @@ -769,8 +769,8 @@ public Void visit(final UnitEqConstr constr, final DBM dbm) { @Override public Void visit(final DiffLtConstr constr, final DBM dbm) { - final VarDecl leftVar = constr.getLeftVar(); - final VarDecl rightVar = constr.getRightVar(); + final VarDecl leftVar = constr.getLeftVar(); + final VarDecl rightVar = constr.getRightVar(); if (dbm.tracks(leftVar) && dbm.tracks(rightVar)) { final int x = dbm.signature.indexOf(leftVar); final int y = dbm.signature.indexOf(rightVar); @@ -782,8 +782,8 @@ public Void visit(final DiffLtConstr constr, final DBM dbm) { @Override public Void visit(final DiffLeqConstr constr, final DBM dbm) { - final VarDecl leftVar = constr.getLeftVar(); - final VarDecl rightVar = constr.getRightVar(); + final VarDecl leftVar = constr.getLeftVar(); + final VarDecl rightVar = constr.getRightVar(); if (dbm.tracks(leftVar) && dbm.tracks(rightVar)) { final int x = dbm.signature.indexOf(leftVar); final int y = dbm.signature.indexOf(rightVar); @@ -795,8 +795,8 @@ public Void visit(final DiffLeqConstr constr, final DBM dbm) { @Override public Void visit(final DiffGtConstr constr, final DBM dbm) { - final VarDecl leftVar = constr.getLeftVar(); - final VarDecl rightVar = constr.getRightVar(); + final VarDecl leftVar = constr.getLeftVar(); + final VarDecl rightVar = constr.getRightVar(); if (dbm.tracks(leftVar) && dbm.tracks(rightVar)) { final int x = dbm.signature.indexOf(leftVar); final int y = dbm.signature.indexOf(rightVar); @@ -808,8 +808,8 @@ public Void visit(final DiffGtConstr constr, final DBM dbm) { @Override public Void visit(final DiffGeqConstr constr, final DBM dbm) { - final VarDecl leftVar = constr.getLeftVar(); - final VarDecl rightVar = constr.getRightVar(); + final VarDecl leftVar = constr.getLeftVar(); + final VarDecl rightVar = constr.getRightVar(); if (dbm.tracks(leftVar) && dbm.tracks(rightVar)) { final int x = dbm.signature.indexOf(leftVar); final int y = dbm.signature.indexOf(rightVar); @@ -821,8 +821,8 @@ public Void visit(final DiffGeqConstr constr, final DBM dbm) { @Override public Void visit(final DiffEqConstr constr, final DBM dbm) { - final VarDecl leftVar = constr.getLeftVar(); - final VarDecl rightVar = constr.getRightVar(); + final VarDecl leftVar = constr.getLeftVar(); + final VarDecl rightVar = constr.getRightVar(); if (dbm.tracks(leftVar) && dbm.tracks(rightVar)) { final int x = dbm.signature.indexOf(leftVar); final int y = dbm.signature.indexOf(rightVar); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java index 43d7a4f77f..cdea6d0aaa 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DbmSignature.java @@ -31,26 +31,26 @@ import hu.bme.mit.theta.common.Utils; 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; -final class DbmSignature implements Iterable> { +final class DbmSignature implements Iterable> { - private final List> indexToVar; - private final Map, Integer> varToIndex; + private final List> indexToVar; + private final Map, Integer> varToIndex; - private DbmSignature(final Iterable> varDecls) { + private DbmSignature(final Iterable> varDecls) { checkNotNull(varDecls); - final ImmutableList.Builder> indexToVarBuilder = ImmutableList.builder(); - final ImmutableMap.Builder, Integer> varToIndexBuilder = ImmutableMap.builder(); + final ImmutableList.Builder> indexToVarBuilder = ImmutableList.builder(); + final ImmutableMap.Builder, Integer> varToIndexBuilder = ImmutableMap.builder(); - final Set> addedVars = Containers.createSet(); + final Set> addedVars = Containers.createSet(); indexToVarBuilder.add(ZeroVar.getInstance()); varToIndexBuilder.put(ZeroVar.getInstance(), addedVars.size()); addedVars.add(ZeroVar.getInstance()); - for (final VarDecl varDecl : varDecls) { + for (final VarDecl varDecl : varDecls) { if (!addedVars.contains(varDecl)) { indexToVarBuilder.add(varDecl); varToIndexBuilder.put(varDecl, addedVars.size()); @@ -64,36 +64,36 @@ private DbmSignature(final Iterable> varDecls) { //// - static DbmSignature over(final Iterable> vars) { + static DbmSignature over(final Iterable> vars) { return new DbmSignature(vars); } public static DbmSignature union(final DbmSignature signature1, final DbmSignature signature2) { checkNotNull(signature1); checkNotNull(signature2); - final Iterable> vars = Sets.union(signature1.toSet(), signature2.toSet()); + final Iterable> vars = Sets.union(signature1.toSet(), signature2.toSet()); return new DbmSignature(vars); } public static DbmSignature intersection(final DbmSignature signature1, final DbmSignature signature2) { checkNotNull(signature1); checkNotNull(signature2); - final Set> vars = Sets.intersection(signature1.toSet(), signature2.toSet()); + final Set> vars = Sets.intersection(signature1.toSet(), signature2.toSet()); return new DbmSignature(vars); } //// - public List> toList() { + public List> toList() { return indexToVar; } - public Set> toSet() { + public Set> toSet() { return varToIndex.keySet(); } @Override - public Iterator> iterator() { + public Iterator> iterator() { return indexToVar.iterator(); } @@ -103,17 +103,17 @@ public int size() { return indexToVar.size(); } - public boolean contains(final VarDecl varDecl) { + public boolean contains(final VarDecl varDecl) { checkNotNull(varDecl); return varToIndex.containsKey(varDecl); } - public int indexOf(final VarDecl varDecl) { + public int indexOf(final VarDecl varDecl) { checkArgument(contains(varDecl), "Unknown variable"); return varToIndex.get(varDecl); } - public VarDecl getVar(final int index) { + public VarDecl getVar(final int index) { checkElementIndex(index, varToIndex.size()); return indexToVar.get(index); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java index 2a06e50e36..d20d4ba26d 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java @@ -21,7 +21,7 @@ import hu.bme.mit.theta.core.clock.constr.ClockConstr; import hu.bme.mit.theta.core.clock.constr.ClockConstrs; 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; final class DiffBounds { @@ -50,7 +50,7 @@ public static int Leq(final int m) { //// - public static ClockConstr toConstr(final VarDecl leftVar, final VarDecl rightVar, final int b) { + public static ClockConstr toConstr(final VarDecl leftVar, final VarDecl rightVar, final int b) { checkNotNull(leftVar); checkNotNull(rightVar); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZeroVar.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZeroVar.java index 31acaf7c4f..d6ab4e8757 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZeroVar.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZeroVar.java @@ -16,19 +16,19 @@ package hu.bme.mit.theta.analysis.zone; import static hu.bme.mit.theta.core.decl.Decls.Var; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; 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; final class ZeroVar { - private static final VarDecl ZERO_VAR = Var("_zero", Rat()); + private static final VarDecl ZERO_VAR = Var("_zero", Clock()); private ZeroVar() { } - static VarDecl getInstance() { + static VarDecl getInstance() { return ZERO_VAR; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java index f30eed570a..6a14355e50 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java @@ -19,7 +19,7 @@ import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.common.Utils; 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; import java.util.Collection; import java.util.Set; @@ -29,18 +29,18 @@ public final class ZonePrec implements Prec { - private final Set> clocks; + private final Set> clocks; - private ZonePrec(final Collection> clocks) { + private ZonePrec(final Collection> clocks) { checkNotNull(clocks); this.clocks = ImmutableSet.copyOf(clocks); } - public static ZonePrec of(final Collection> clocks) { + public static ZonePrec of(final Collection> clocks) { return new ZonePrec(clocks); } - public Set> getVars() { + public Set> getVars() { return clocks; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java index a337e506b0..759d17a3c6 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java @@ -25,7 +25,7 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.rattype.RatLitExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import java.math.BigInteger; import java.util.Collection; @@ -61,13 +61,14 @@ private ZoneState(final Builder ops) { //// - public static ZoneState region(final Valuation valuation, final Collection> vars) { + /* + public static ZoneState region(final Valuation valuation, final Collection> vars) { checkNotNull(valuation); - final Iterable> constrainedVars = Iterables.filter(vars, v -> valuation.eval(v).isPresent()); + final Iterable> constrainedVars = Iterables.filter(vars, v -> valuation.eval(v).isPresent()); final DBM dbm = DBM.top(constrainedVars); - for (final VarDecl x : constrainedVars) { + for (final VarDecl x : constrainedVars) { final RatLitExpr sx = (RatLitExpr) valuation.eval(x).get(); final RatLitExpr fx = sx.frac(); @@ -78,7 +79,7 @@ public static ZoneState region(final Valuation valuation, final Collection y : constrainedVars) { + for (final VarDecl y : constrainedVars) { if (x == y) { continue; } @@ -97,6 +98,7 @@ public static ZoneState region(final Valuation valuation, final Collection> clocks) { + public static ZoneState zero(final Collection> clocks) { return new ZoneState(DBM.zero(clocks)); } @@ -145,7 +147,7 @@ public Builder transform() { return Builder.transform(this); } - public Builder project(final Collection> clocks) { + public Builder project(final Collection> clocks) { checkNotNull(clocks); return Builder.project(this, clocks); } @@ -165,7 +167,7 @@ public boolean isLeq(final ZoneState that) { return this.dbm.isLeq(that.dbm); } - public boolean isLeq(final ZoneState that, final Collection> activeVars) { + public boolean isLeq(final ZoneState that, final Collection> activeVars) { return this.dbm.isLeq(that.dbm, activeVars); } @@ -237,7 +239,7 @@ private static Builder transform(final ZoneState state) { return new Builder(DBM.copyOf(state.dbm)); } - private static Builder project(final ZoneState state, final Collection> clocks) { + private static Builder project(final ZoneState state, final Collection> clocks) { return new Builder(DBM.project(state.dbm, clocks)); } @@ -274,27 +276,27 @@ public Builder and(final ClockConstr constr) { return this; } - public Builder free(final VarDecl varDecl) { + public Builder free(final VarDecl varDecl) { dbm.free(varDecl); return this; } - public Builder reset(final VarDecl varDecl, final int m) { + public Builder reset(final VarDecl varDecl, final int m) { dbm.reset(varDecl, m); return this; } - public Builder copy(final VarDecl lhs, final VarDecl rhs) { + public Builder copy(final VarDecl lhs, final VarDecl rhs) { dbm.copy(lhs, rhs); return this; } - public Builder shift(final VarDecl varDecl, final int m) { + public Builder shift(final VarDecl varDecl, final int m) { dbm.shift(varDecl, m); return this; } - public Builder norm(final Map, ? extends Integer> ceilings) { + public Builder norm(final Map, ? extends Integer> ceilings) { dbm.norm(ceilings); return this; } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/AndConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/AndConstr.java index d3ee7b41fa..fd2352d988 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/AndConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/AndConstr.java @@ -26,7 +26,7 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.booltype.AndExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class AndConstr implements ClockConstr { @@ -47,8 +47,8 @@ public Collection getConstrs() { } @Override - public Collection> getVars() { - final ImmutableSet.Builder> builder = ImmutableSet.builder(); + public Collection> getVars() { + final ImmutableSet.Builder> builder = ImmutableSet.builder(); for (final ClockConstr constr : constrs) { builder.addAll(constr.getVars()); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstr.java index 20140b27b9..cdf8d8fe75 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstr.java @@ -20,11 +20,11 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public interface ClockConstr { - Collection> getVars(); + Collection> getVars(); Expr toExpr(); diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java index a72225f5af..0faa895ad2 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java @@ -16,6 +16,7 @@ package hu.bme.mit.theta.core.clock.constr; import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import java.util.Collection; @@ -34,14 +35,10 @@ import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.booltype.FalseExpr; import hu.bme.mit.theta.core.type.booltype.TrueExpr; -import hu.bme.mit.theta.core.type.rattype.RatEqExpr; -import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatGtExpr; -import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatLitExpr; -import hu.bme.mit.theta.core.type.rattype.RatLtExpr; -import hu.bme.mit.theta.core.type.rattype.RatSubExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.*; +import hu.bme.mit.theta.core.type.inttype.IntLitExpr; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.core.type.rattype.*; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.TypeUtils; @@ -60,10 +57,14 @@ private ClockConstrs() { //// - public static ClockConstr formExpr(final Expr expr) { + public static ClockConstr fromExpr(final Expr expr) { return FromExprHelper.INSTANCE.transform(expr); } + public static ClockConstr fromClockExpr(final ClockConstraintExpr expr) { + return FromClockExprHelper.INSTANCE.transform(expr); + } + //// public static TrueConstr True() { @@ -74,60 +75,60 @@ public static FalseConstr False() { return FALSE_CONSTR; } - public static UnitLtConstr Lt(final VarDecl clock, final int bound) { + public static UnitLtConstr Lt(final VarDecl clock, final int bound) { checkNotNull(clock); return new UnitLtConstr(clock, bound); } - public static UnitLeqConstr Leq(final VarDecl clock, final int bound) { + public static UnitLeqConstr Leq(final VarDecl clock, final int bound) { checkNotNull(clock); return new UnitLeqConstr(clock, bound); } - public static UnitGtConstr Gt(final VarDecl clock, final int bound) { + public static UnitGtConstr Gt(final VarDecl clock, final int bound) { checkNotNull(clock); return new UnitGtConstr(clock, bound); } - public static UnitGeqConstr Geq(final VarDecl clock, final int bound) { + public static UnitGeqConstr Geq(final VarDecl clock, final int bound) { checkNotNull(clock); return new UnitGeqConstr(clock, bound); } - public static UnitEqConstr Eq(final VarDecl clock, final int bound) { + public static UnitEqConstr Eq(final VarDecl clock, final int bound) { checkNotNull(clock); return new UnitEqConstr(clock, bound); } - public static DiffLtConstr Lt(final VarDecl leftClock, final VarDecl rightClock, + public static DiffLtConstr Lt(final VarDecl leftClock, final VarDecl rightClock, final int bound) { checkNotNull(leftClock); checkNotNull(rightClock); return new DiffLtConstr(leftClock, rightClock, bound); } - public static DiffLeqConstr Leq(final VarDecl leftClock, final VarDecl rightClock, + public static DiffLeqConstr Leq(final VarDecl leftClock, final VarDecl rightClock, final int bound) { checkNotNull(leftClock); checkNotNull(rightClock); return new DiffLeqConstr(leftClock, rightClock, bound); } - public static DiffGtConstr Gt(final VarDecl leftClock, final VarDecl rightClock, + public static DiffGtConstr Gt(final VarDecl leftClock, final VarDecl rightClock, final int bound) { checkNotNull(leftClock); checkNotNull(rightClock); return new DiffGtConstr(leftClock, rightClock, bound); } - public static DiffGeqConstr Geq(final VarDecl leftClock, final VarDecl rightClock, + public static DiffGeqConstr Geq(final VarDecl leftClock, final VarDecl rightClock, final int bound) { checkNotNull(leftClock); checkNotNull(rightClock); return new DiffGeqConstr(leftClock, rightClock, bound); } - public static DiffEqConstr Eq(final VarDecl leftClock, final VarDecl rightClock, + public static DiffEqConstr Eq(final VarDecl leftClock, final VarDecl rightClock, final int bound) { checkNotNull(leftClock); checkNotNull(rightClock); @@ -193,7 +194,7 @@ private FalseConstr transformFalse(final FalseExpr expr) { } private ClockConstr transformLt(final RatLtExpr expr) { - final List> lhs = extractConstrLhs(expr); + final List> lhs = extractConstrLhs(expr); final int rhs = extractConstrRhs(expr); if (lhs.size() == 1) { return Lt(lhs.get(0), rhs); @@ -203,7 +204,7 @@ private ClockConstr transformLt(final RatLtExpr expr) { } private ClockConstr transformLeq(final RatLeqExpr expr) { - final List> lhs = extractConstrLhs(expr); + final List> lhs = extractConstrLhs(expr); final int rhs = extractConstrRhs(expr); if (lhs.size() == 1) { return Leq(lhs.get(0), rhs); @@ -213,7 +214,7 @@ private ClockConstr transformLeq(final RatLeqExpr expr) { } private ClockConstr transformGt(final RatGtExpr expr) { - final List> lhs = extractConstrLhs(expr); + final List> lhs = extractConstrLhs(expr); final int rhs = extractConstrRhs(expr); if (lhs.size() == 1) { return Gt(lhs.get(0), rhs); @@ -223,7 +224,7 @@ private ClockConstr transformGt(final RatGtExpr expr) { } private ClockConstr transformGeq(final RatGeqExpr expr) { - final List> lhs = extractConstrLhs(expr); + final List> lhs = extractConstrLhs(expr); final int rhs = extractConstrRhs(expr); if (lhs.size() == 1) { return Geq(lhs.get(0), rhs); @@ -233,7 +234,7 @@ private ClockConstr transformGeq(final RatGeqExpr expr) { } private ClockConstr transformEq(final RatEqExpr expr) { - final List> lhs = extractConstrLhs(expr); + final List> lhs = extractConstrLhs(expr); final int rhs = extractConstrRhs(expr); if (lhs.size() == 1) { return Eq(lhs.get(0), rhs); @@ -250,7 +251,7 @@ private AndConstr transformAnd(final AndExpr expr) { return And(builder.build()); } - private static List> extractConstrLhs(final BinaryExpr expr) { + private static List> extractConstrLhs(final BinaryExpr expr) { final Expr leftOp = expr.getLeftOp(); if (leftOp instanceof RefExpr) { @@ -258,7 +259,7 @@ private static List> extractConstrLhs(final BinaryExpr leftDecl = leftRef.getDecl(); if (leftDecl instanceof VarDecl) { final VarDecl leftVar = (VarDecl) leftDecl; - final VarDecl leftRatVar = TypeUtils.cast(leftVar, Rat()); + final VarDecl leftRatVar = TypeUtils.cast(leftVar, Clock()); return ImmutableList.of(leftRatVar); } } @@ -276,8 +277,8 @@ private static List> extractConstrLhs(final BinaryExpr subLeftVar = (VarDecl) subLeftDecl; final VarDecl subRightVar = (VarDecl) subRightDecl; - final VarDecl subLeftRatVar = TypeUtils.cast(subLeftVar, Rat()); - final VarDecl subRightRatVar = TypeUtils.cast(subRightVar, Rat()); + final VarDecl subLeftRatVar = TypeUtils.cast(subLeftVar, Clock()); + final VarDecl subRightRatVar = TypeUtils.cast(subRightVar, Clock()); return ImmutableList.of(subLeftRatVar, subRightRatVar); } } @@ -302,4 +303,125 @@ private static int extractConstrRhs(final BinaryExpr expr) { } + private static final class FromClockExprHelper { + + private static final FromClockExprHelper INSTANCE = new FromClockExprHelper(); + + private final DispatchTable table; + + private FromClockExprHelper() { + table = DispatchTable.builder() + + .addCase(ClockLtExpr.class, this::transformLt) + + .addCase(ClockLeqExpr.class, this::transformLeq) + + .addCase(ClockGtExpr.class, this::transformGt) + + .addCase(ClockGeqExpr.class, this::transformGeq) + + .addCase(ClockEqExpr.class, this::transformEq) + + .addDefault(o -> { + throw new IllegalArgumentException(); + }) + + .build(); + } + + public ClockConstr transform(final Expr expr) { + return table.dispatch(expr); + } + + private ClockConstr transformLt(final ClockLtExpr expr) { + final List> lhs = extractClocks(expr.getLeftOp()); + final int rhs = extractValue(expr.getRightOp()); + if (lhs.size() == 1) { + return Lt(lhs.get(0), rhs); + } else { + return Lt(lhs.get(0), lhs.get(1), rhs); + } + } + + private ClockConstr transformLeq(final ClockLeqExpr expr) { + final List> lhs = extractClocks(expr.getLeftOp()); + final int rhs = extractValue(expr.getRightOp()); + if (lhs.size() == 1) { + return Leq(lhs.get(0), rhs); + } else { + return Leq(lhs.get(0), lhs.get(1), rhs); + } + } + + private ClockConstr transformGt(final ClockGtExpr expr) { + final List> lhs = extractClocks(expr.getLeftOp()); + final int rhs = extractValue(expr.getRightOp()); + if (lhs.size() == 1) { + return Gt(lhs.get(0), rhs); + } else { + return Gt(lhs.get(0), lhs.get(1), rhs); + } + } + + private ClockConstr transformGeq(final ClockGeqExpr expr) { + final List> lhs = extractClocks(expr.getLeftOp()); + final int rhs = extractValue(expr.getRightOp()); + if (lhs.size() == 1) { + return Geq(lhs.get(0), rhs); + } else { + return Geq(lhs.get(0), lhs.get(1), rhs); + } + } + + private ClockConstr transformEq(final ClockEqExpr expr) { + final List> lhs = extractClocks(expr.getLeftOp()); + final int rhs = extractValue(expr.getRightOp()); + if (lhs.size() == 1) { + return Eq(lhs.get(0), rhs); + } else { + return Eq(lhs.get(0), lhs.get(1), rhs); + } + } + + private static List> extractClocks(final Expr expr) { + + if (expr instanceof RefExpr) { + final RefExpr clockRefExpr = (RefExpr) expr; + final Decl clockDecl = clockRefExpr.getDecl(); + if (clockDecl instanceof VarDecl) { + final VarDecl clockVar = (VarDecl) clockDecl; + return ImmutableList.of(clockVar); + } + } + + if (expr instanceof ClockDiffExpr) { + final ClockDiffExpr clockDiffExpr = (ClockDiffExpr) expr; + final Expr leftClockExpr = clockDiffExpr.getLeftOp(); + final Expr rightClockExpr = clockDiffExpr.getRightOp(); + if (leftClockExpr instanceof RefExpr && rightClockExpr instanceof RefExpr) { + final Decl leftClockDecl = ((RefExpr) leftClockExpr).getDecl(); + final Decl rightClockDecl = ((RefExpr) rightClockExpr).getDecl(); + if (leftClockDecl instanceof VarDecl && rightClockDecl instanceof VarDecl) { + final VarDecl leftClockVar = (VarDecl) leftClockDecl; + final VarDecl rightClockVar = (VarDecl) rightClockDecl; + return ImmutableList.of(leftClockVar, rightClockVar); + } + } + } + + throw new IllegalArgumentException(); + } + + private static int extractValue(final Expr expr) { + final Expr simplifiedExpr = ExprUtils.simplify(expr); + + if (simplifiedExpr instanceof IntLitExpr) { + final IntLitExpr intLitExpr = (IntLitExpr) simplifiedExpr; + return intLitExpr.getValue().intValueExact(); + } + + throw new IllegalArgumentException(); + } + } + } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffConstr.java index ac01fd63c2..10c57f6e95 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffConstr.java @@ -22,31 +22,31 @@ import com.google.common.collect.ImmutableSet; 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 abstract class DiffConstr extends AtomicConstr { - private final VarDecl leftVar; - private final VarDecl rightVar; + private final VarDecl leftVar; + private final VarDecl rightVar; private volatile int hashCode = 0; - protected DiffConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { + protected DiffConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { super(bound); this.leftVar = checkNotNull(leftVar); this.rightVar = checkNotNull(rightVar); } - public final VarDecl getLeftVar() { + public final VarDecl getLeftVar() { return leftVar; } - public final VarDecl getRightVar() { + public final VarDecl getRightVar() { return rightVar; } @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(leftVar, rightVar); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffEqConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffEqConstr.java index fdb534fc32..29a874585a 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffEqConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffEqConstr.java @@ -15,14 +15,15 @@ */ package hu.bme.mit.theta.core.clock.constr; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Eq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.rattype.RatEqExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockDiffExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockEqExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class DiffEqConstr extends DiffConstr { @@ -30,19 +31,20 @@ public final class DiffEqConstr extends DiffConstr { private static final String OPERATOR_LABEL = "="; - private volatile RatEqExpr expr = null; + private volatile ClockEqExpr expr = null; - DiffEqConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { + DiffEqConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { super(leftVar, rightVar, bound); } @Override - public RatEqExpr toExpr() { - RatEqExpr result = expr; + public ClockEqExpr toExpr() { + ClockEqExpr result = expr; if (result == null) { - final RefExpr leftRef = getLeftVar().getRef(); - final RefExpr rightRef = getRightVar().getRef(); - result = Eq(Sub(leftRef, rightRef), Rat(getBound(), 1)); + final RefExpr leftRef = getLeftVar().getRef(); + final RefExpr rightRef = getRightVar().getRef(); + final ClockDiffExpr diffExpr = ClockExprs.Diff(leftRef, rightRef); + result = ClockExprs.Eq(diffExpr, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGeqConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGeqConstr.java index 19ad8a6971..32873080a5 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGeqConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGeqConstr.java @@ -15,14 +15,15 @@ */ package hu.bme.mit.theta.core.clock.constr; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Geq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockDiffExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockGeqExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class DiffGeqConstr extends DiffConstr { @@ -30,19 +31,20 @@ public final class DiffGeqConstr extends DiffConstr { private static final String OPERATOR_LABEL = ">="; - private volatile RatGeqExpr expr = null; + private volatile ClockGeqExpr expr = null; - DiffGeqConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { + DiffGeqConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { super(leftVar, rightVar, bound); } @Override - public RatGeqExpr toExpr() { - RatGeqExpr result = expr; + public ClockGeqExpr toExpr() { + ClockGeqExpr result = expr; if (result == null) { - final RefExpr leftRef = getLeftVar().getRef(); - final RefExpr rightRef = getRightVar().getRef(); - result = Geq(Sub(leftRef, rightRef), Rat(getBound(), 1)); + final RefExpr leftRef = getLeftVar().getRef(); + final RefExpr rightRef = getRightVar().getRef(); + final ClockDiffExpr diffExpr = ClockExprs.Diff(leftRef, rightRef); + result = ClockExprs.Geq(diffExpr, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGtConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGtConstr.java index 68e4daab56..c46543aec3 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGtConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffGtConstr.java @@ -15,14 +15,15 @@ */ package hu.bme.mit.theta.core.clock.constr; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Gt; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.rattype.RatGtExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockDiffExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockGtExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class DiffGtConstr extends DiffConstr { @@ -30,19 +31,20 @@ public final class DiffGtConstr extends DiffConstr { private static final String OPERATOR_LABEL = ">"; - private volatile RatGtExpr expr = null; + private volatile ClockGtExpr expr = null; - DiffGtConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { + DiffGtConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { super(leftVar, rightVar, bound); } @Override - public RatGtExpr toExpr() { - RatGtExpr result = expr; + public ClockGtExpr toExpr() { + ClockGtExpr result = expr; if (result == null) { - final RefExpr leftRef = getLeftVar().getRef(); - final RefExpr rightRef = getRightVar().getRef(); - result = Gt(Sub(leftRef, rightRef), Rat(getBound(), 1)); + final RefExpr leftRef = getLeftVar().getRef(); + final RefExpr rightRef = getRightVar().getRef(); + final ClockDiffExpr diffExpr = ClockExprs.Diff(leftRef, rightRef); + result = ClockExprs.Gt(diffExpr, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLeqConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLeqConstr.java index ce5164445a..ac96fae1e6 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLeqConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLeqConstr.java @@ -15,14 +15,15 @@ */ package hu.bme.mit.theta.core.clock.constr; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Leq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockDiffExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockLeqExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class DiffLeqConstr extends DiffConstr { @@ -30,19 +31,20 @@ public final class DiffLeqConstr extends DiffConstr { private static final String OPERATOR_LABEL = "<="; - private volatile RatLeqExpr expr = null; + private volatile ClockLeqExpr expr = null; - DiffLeqConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { + DiffLeqConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { super(leftVar, rightVar, bound); } @Override - public RatLeqExpr toExpr() { - RatLeqExpr result = expr; + public ClockLeqExpr toExpr() { + ClockLeqExpr result = expr; if (result == null) { - final RefExpr leftRef = getLeftVar().getRef(); - final RefExpr rightRef = getRightVar().getRef(); - result = Leq(Sub(leftRef, rightRef), Rat(getBound(), 1)); + final RefExpr leftRef = getLeftVar().getRef(); + final RefExpr rightRef = getRightVar().getRef(); + final ClockDiffExpr diffExpr = ClockExprs.Diff(leftRef, rightRef); + result = ClockExprs.Leq(diffExpr, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLtConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLtConstr.java index 79fd3a25f0..d358278089 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLtConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/DiffLtConstr.java @@ -15,14 +15,15 @@ */ package hu.bme.mit.theta.core.clock.constr; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Lt; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.rattype.RatLtExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockDiffExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockLtExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class DiffLtConstr extends DiffConstr { @@ -30,19 +31,20 @@ public final class DiffLtConstr extends DiffConstr { private static final String OPERATOR_LABEL = "<"; - private volatile RatLtExpr expr = null; + private volatile ClockLtExpr expr = null; - DiffLtConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { + DiffLtConstr(final VarDecl leftVar, final VarDecl rightVar, final int bound) { super(leftVar, rightVar, bound); } @Override - public RatLtExpr toExpr() { - RatLtExpr result = expr; + public ClockLtExpr toExpr() { + ClockLtExpr result = expr; if (result == null) { - final RefExpr leftRef = getLeftVar().getRef(); - final RefExpr rightRef = getRightVar().getRef(); - result = Lt(Sub(leftRef, rightRef), Rat(getBound(), 1)); + final RefExpr leftRef = getLeftVar().getRef(); + final RefExpr rightRef = getRightVar().getRef(); + final ClockDiffExpr diffExpr = ClockExprs.Diff(leftRef, rightRef); + result = ClockExprs.Lt(diffExpr, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/FalseConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/FalseConstr.java index bdde06995c..7f4c395168 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/FalseConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/FalseConstr.java @@ -23,7 +23,7 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.booltype.FalseExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class FalseConstr implements ClockConstr { @@ -32,7 +32,7 @@ public final class FalseConstr implements ClockConstr { private static final String CC_LABEL = "false"; @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/TrueConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/TrueConstr.java index fe65c24c6e..6f83b999b9 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/TrueConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/TrueConstr.java @@ -23,7 +23,7 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.booltype.TrueExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class TrueConstr implements ClockConstr { @@ -32,7 +32,7 @@ public final class TrueConstr implements ClockConstr { private static final String CC_LABEL = "true"; @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitConstr.java index deadd6c389..c431517377 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitConstr.java @@ -22,25 +22,25 @@ import com.google.common.collect.ImmutableSet; 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 abstract class UnitConstr extends AtomicConstr { - private final VarDecl varDecl; + private final VarDecl varDecl; private volatile int hashCode = 0; - protected UnitConstr(final VarDecl varDecl, final int bound) { + protected UnitConstr(final VarDecl varDecl, final int bound) { super(bound); this.varDecl = checkNotNull(varDecl); } - public final VarDecl getVar() { + public final VarDecl getVar() { return varDecl; } @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(varDecl); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitEqConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitEqConstr.java index 783ec329de..caaf6db6cd 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitEqConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitEqConstr.java @@ -15,13 +15,16 @@ */ package hu.bme.mit.theta.core.clock.constr; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Eq; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockEqExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; import hu.bme.mit.theta.core.type.rattype.RatEqExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class UnitEqConstr extends UnitConstr { @@ -29,18 +32,18 @@ public final class UnitEqConstr extends UnitConstr { private static final String OPERATOR_LABEL = "="; - private volatile RatEqExpr expr = null; + private volatile ClockEqExpr expr = null; - UnitEqConstr(final VarDecl clock, final int bound) { + UnitEqConstr(final VarDecl clock, final int bound) { super(clock, bound); } @Override - public RatEqExpr toExpr() { - RatEqExpr result = expr; + public ClockEqExpr toExpr() { + ClockEqExpr result = expr; if (result == null) { - final RefExpr ref = getVar().getRef(); - result = Eq(ref, Rat(getBound(), 1)); + final RefExpr ref = getVar().getRef(); + result = ClockExprs.Eq(ref, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGeqConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGeqConstr.java index 9f682c206b..94f5a32469 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGeqConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGeqConstr.java @@ -15,13 +15,16 @@ */ package hu.bme.mit.theta.core.clock.constr; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Geq; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockGeqExpr; import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class UnitGeqConstr extends UnitConstr { @@ -29,18 +32,18 @@ public final class UnitGeqConstr extends UnitConstr { private static final String OPERATOR_LABEL = ">="; - private volatile RatGeqExpr expr = null; + private volatile ClockGeqExpr expr = null; - UnitGeqConstr(final VarDecl clock, final int bound) { + UnitGeqConstr(final VarDecl clock, final int bound) { super(clock, bound); } @Override - public RatGeqExpr toExpr() { - RatGeqExpr result = expr; + public ClockGeqExpr toExpr() { + ClockGeqExpr result = expr; if (result == null) { - final RefExpr ref = getVar().getRef(); - result = Geq(ref, Rat(getBound(), 1)); + final RefExpr ref = getVar().getRef(); + result = ClockExprs.Geq(ref, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGtConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGtConstr.java index 420ccbe924..4ee9346a19 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGtConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitGtConstr.java @@ -15,13 +15,16 @@ */ package hu.bme.mit.theta.core.clock.constr; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Gt; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockGtExpr; import hu.bme.mit.theta.core.type.rattype.RatGtExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class UnitGtConstr extends UnitConstr { @@ -29,18 +32,18 @@ public final class UnitGtConstr extends UnitConstr { private static final String OPERATOR_LABEL = ">"; - private volatile RatGtExpr expr = null; + private volatile ClockGtExpr expr = null; - UnitGtConstr(final VarDecl clock, final int bound) { + UnitGtConstr(final VarDecl clock, final int bound) { super(clock, bound); } @Override - public RatGtExpr toExpr() { - RatGtExpr result = expr; + public ClockGtExpr toExpr() { + ClockGtExpr result = expr; if (result == null) { - final RefExpr ref = getVar().getRef(); - result = Gt(ref, Rat(getBound(), 1)); + final RefExpr ref = getVar().getRef(); + result = ClockExprs.Gt(ref, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLeqConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLeqConstr.java index fe51fb9d57..326c6dca6b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLeqConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLeqConstr.java @@ -15,13 +15,16 @@ */ package hu.bme.mit.theta.core.clock.constr; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Leq; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockLeqExpr; import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class UnitLeqConstr extends UnitConstr { @@ -29,18 +32,18 @@ public final class UnitLeqConstr extends UnitConstr { private static final String OPERATOR_LABEL = "<="; - private volatile RatLeqExpr expr = null; + private volatile ClockLeqExpr expr = null; - UnitLeqConstr(final VarDecl clock, final int bound) { + UnitLeqConstr(final VarDecl clock, final int bound) { super(clock, bound); } @Override - public RatLeqExpr toExpr() { - RatLeqExpr result = expr; + public ClockLeqExpr toExpr() { + ClockLeqExpr result = expr; if (result == null) { - final RefExpr ref = getVar().getRef(); - result = Leq(ref, Rat(getBound(), 1)); + final RefExpr ref = getVar().getRef(); + result = ClockExprs.Leq(ref, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLtConstr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLtConstr.java index b5d04cc4bd..4dbf5c3adc 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLtConstr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/constr/UnitLtConstr.java @@ -15,13 +15,16 @@ */ package hu.bme.mit.theta.core.clock.constr; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Lt; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockLtExpr; import hu.bme.mit.theta.core.type.rattype.RatLtExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class UnitLtConstr extends UnitConstr { @@ -29,18 +32,18 @@ public final class UnitLtConstr extends UnitConstr { private static final String OPERATOR_LABEL = "<"; - private volatile RatLtExpr expr = null; + private volatile ClockLtExpr expr = null; - UnitLtConstr(final VarDecl clock, final int bound) { + UnitLtConstr(final VarDecl clock, final int bound) { super(clock, bound); } @Override - public RatLtExpr toExpr() { - RatLtExpr result = expr; + public ClockLtExpr toExpr() { + ClockLtExpr result = expr; if (result == null) { - final RefExpr ref = getVar().getRef(); - result = Lt(ref, Rat(getBound(), 1)); + final RefExpr ref = getVar().getRef(); + result = ClockExprs.Lt(ref, Int(getBound())); expr = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOp.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOp.java index ea9515ece1..82696a8f8a 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOp.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOp.java @@ -19,11 +19,11 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.Stmt; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public interface ClockOp { - Collection> getVars(); + Collection> getVars(); Stmt toStmt(); diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java index c8d20480d4..16c740be63 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java @@ -21,11 +21,13 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.AssignStmt; import hu.bme.mit.theta.core.stmt.AssumeStmt; +import hu.bme.mit.theta.core.stmt.DelayStmt; import hu.bme.mit.theta.core.stmt.HavocStmt; import hu.bme.mit.theta.core.stmt.IfStmt; import hu.bme.mit.theta.core.stmt.LoopStmt; import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.stmt.OrtStmt; +import hu.bme.mit.theta.core.stmt.ResetStmt; import hu.bme.mit.theta.core.stmt.SequenceStmt; import hu.bme.mit.theta.core.stmt.SkipStmt; import hu.bme.mit.theta.core.stmt.Stmt; @@ -37,9 +39,10 @@ import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.inttype.IntLitExpr; import hu.bme.mit.theta.core.type.rattype.RatLitExpr; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.core.utils.TypeUtils; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; public final class ClockOps { @@ -61,11 +64,11 @@ public static ClockOp fromStmt(final Stmt stmt) { //// - public static CopyOp Copy(final VarDecl varDecl, final VarDecl value) { + public static CopyOp Copy(final VarDecl varDecl, final VarDecl value) { return new CopyOp(varDecl, value); } - public static FreeOp Free(final VarDecl varDecl) { + public static FreeOp Free(final VarDecl varDecl) { return new FreeOp(varDecl); } @@ -73,11 +76,11 @@ public static GuardOp Guard(final ClockConstr constr) { return new GuardOp(constr); } - public static ResetOp Reset(final VarDecl varDecl, final int value) { + public static ResetOp Reset(final VarDecl varDecl, final int value) { return new ResetOp(varDecl, value); } - public static ShiftOp Shift(final VarDecl varDecl, final int offset) { + public static ShiftOp Shift(final VarDecl varDecl, final int offset) { return new ShiftOp(varDecl, offset); } @@ -95,7 +98,7 @@ public ClockOp visit(final SkipStmt stmt, final Void param) { @Override public ClockOp visit(final HavocStmt stmt, final Void param) { - final VarDecl varDecl = TypeUtils.cast(stmt.getVarDecl(), Rat()); + final VarDecl varDecl = TypeUtils.cast(stmt.getVarDecl(), Clock()); return Free(varDecl); } @@ -124,10 +127,21 @@ public ClockOp visit(IfStmt stmt, Void param) { throw new UnsupportedOperationException(); } + @Override + public ClockOp visit(DelayStmt stmt, Void param) { + throw new UnsupportedOperationException(); + } + + @Override + public ClockOp visit(ResetStmt stmt, Void param) { + final VarDecl varDecl = TypeUtils.cast(stmt.getClockDecl(), Clock()); + return Reset(varDecl, stmt.getValue()); + } + @Override public ClockOp visit(final AssignStmt stmt, final Void param) { - final VarDecl varDecl = TypeUtils.cast(stmt.getVarDecl(), Rat()); + final VarDecl varDecl = TypeUtils.cast(stmt.getVarDecl(), Clock()); final Expr expr = stmt.getExpr(); if (expr instanceof IntLitExpr) { @@ -140,12 +154,12 @@ public ClockOp visit(final AssignStmt stmt, fi final Decl rightDecl = rightRef.getDecl(); if (rightDecl instanceof VarDecl) { final VarDecl rightVar = (VarDecl) rightDecl; - final VarDecl rightRatVar = TypeUtils.cast(rightVar, Rat()); + final VarDecl rightRatVar = TypeUtils.cast(rightVar, Clock()); return Copy(varDecl, rightRatVar); } } else if (expr instanceof AddExpr) { - final RefExpr varRef = varDecl.getRef(); + final RefExpr varRef = varDecl.getRef(); final AddExpr addExpr = (AddExpr) expr; final Expr[] ops = addExpr.getOps().toArray(new Expr[0]); @@ -176,7 +190,7 @@ public ClockOp visit(final AssignStmt stmt, fi public ClockOp visit(final AssumeStmt stmt, final Void param) { try { final Expr cond = stmt.getCond(); - final ClockConstr constr = ClockConstrs.formExpr(cond); + final ClockConstr constr = ClockConstrs.fromExpr(cond); return Guard(constr); } catch (final IllegalArgumentException e) { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/CopyOp.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/CopyOp.java index cb6e143263..76f0643b1b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/CopyOp.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/CopyOp.java @@ -25,39 +25,39 @@ import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.AssignStmt; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class CopyOp implements ClockOp { private static final int HASH_SEED = 1289; - private final VarDecl varDecl; - private final VarDecl value; + private final VarDecl varDecl; + private final VarDecl value; private volatile int hashCode = 0; - private volatile AssignStmt stmt = null; + private volatile AssignStmt stmt = null; - CopyOp(final VarDecl varDecl, final VarDecl value) { + CopyOp(final VarDecl varDecl, final VarDecl value) { this.varDecl = checkNotNull(varDecl); this.value = checkNotNull(value); } - public VarDecl getVar() { + public VarDecl getVar() { return varDecl; } - public VarDecl getValue() { + public VarDecl getValue() { return value; } @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(varDecl, value); } @Override - public AssignStmt toStmt() { - AssignStmt result = stmt; + public AssignStmt toStmt() { + AssignStmt result = stmt; if (result == null) { result = Assign(varDecl, value.getRef()); stmt = result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/FreeOp.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/FreeOp.java index aae1e40f85..0510959a5b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/FreeOp.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/FreeOp.java @@ -25,33 +25,33 @@ import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.HavocStmt; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class FreeOp implements ClockOp { private static final int HASH_SEED = 2281; - private final VarDecl varDecl; + private final VarDecl varDecl; private volatile int hashCode = 0; - private volatile HavocStmt stmt = null; + private volatile HavocStmt stmt = null; - FreeOp(final VarDecl varDecl) { + FreeOp(final VarDecl varDecl) { this.varDecl = checkNotNull(varDecl); } - public VarDecl getVar() { + public VarDecl getVar() { return varDecl; } @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(varDecl); } @Override - public HavocStmt toStmt() { - HavocStmt result = stmt; + public HavocStmt toStmt() { + HavocStmt result = stmt; if (result == null) { result = Havoc(varDecl); stmt = result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/GuardOp.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/GuardOp.java index f59a5e18b2..a0f1893f1f 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/GuardOp.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/GuardOp.java @@ -24,7 +24,7 @@ import hu.bme.mit.theta.core.clock.constr.ClockConstr; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.AssumeStmt; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class GuardOp implements ClockOp { @@ -44,7 +44,7 @@ public ClockConstr getConstr() { } @Override - public Collection> getVars() { + public Collection> getVars() { return constr.getVars(); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ResetOp.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ResetOp.java index a6aeae9378..a21d037927 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ResetOp.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ResetOp.java @@ -17,7 +17,6 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; -import static hu.bme.mit.theta.core.stmt.Stmts.Assign; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import java.util.Collection; @@ -26,26 +25,26 @@ import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.stmt.AssignStmt; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.stmt.ResetStmt; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class ResetOp implements ClockOp { private static final int HASH_SEED = 4507; - private final VarDecl varDecl; + private final VarDecl varDecl; private final int value; private volatile int hashCode = 0; - private volatile AssignStmt stmt = null; + private volatile ResetStmt stmt = null; - ResetOp(final VarDecl varDecl, final int value) { + ResetOp(final VarDecl varDecl, final int value) { checkArgument(value >= 0); this.varDecl = checkNotNull(varDecl); this.value = value; } - public VarDecl getVar() { + public VarDecl getVar() { return varDecl; } @@ -54,15 +53,15 @@ public int getValue() { } @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(varDecl); } @Override - public AssignStmt toStmt() { - AssignStmt result = stmt; + public ResetStmt toStmt() { + ResetStmt result = stmt; if (result == null) { - result = Assign(varDecl, Rat(value, 1)); + result = ResetStmt.of(varDecl, value); stmt = result; } return result; diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ShiftOp.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ShiftOp.java index 3066513837..72df552c0e 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ShiftOp.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ShiftOp.java @@ -27,24 +27,24 @@ import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.AssignStmt; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; public final class ShiftOp implements ClockOp { private static final int HASH_SEED = 5521; - private final VarDecl varDecl; + private final VarDecl varDecl; private final int offset; private volatile int hashCode = 0; - private volatile AssignStmt stmt = null; + private volatile AssignStmt stmt = null; - ShiftOp(final VarDecl varDecl, final int offset) { + ShiftOp(final VarDecl varDecl, final int offset) { this.varDecl = checkNotNull(varDecl); this.offset = offset; } - public VarDecl getVar() { + public VarDecl getVar() { return varDecl; } @@ -53,15 +53,16 @@ public int getOffset() { } @Override - public Collection> getVars() { + public Collection> getVars() { return ImmutableSet.of(varDecl); } @Override - public AssignStmt toStmt() { - AssignStmt result = stmt; + public AssignStmt toStmt() { + AssignStmt result = stmt; if (result == null) { - result = Assign(varDecl, Add(varDecl.getRef(), Rat(offset, 1))); + // TODO + //result = Assign(varDecl, Add(varDecl.getRef(), Rat(offset, 1))); stmt = result; } return result; diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index 214c9e086d..a436314448 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -84,6 +84,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvURemExpr; import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; +import hu.bme.mit.theta.core.type.clocktype.*; import hu.bme.mit.theta.core.type.fptype.FpAbsExpr; import hu.bme.mit.theta.core.type.fptype.FpAddExpr; import hu.bme.mit.theta.core.type.fptype.FpAssignExpr; @@ -400,6 +401,18 @@ public Z3ExprTransformer(final Z3TransformationManager transformer, final Contex .addCase(ArrayInitExpr.class, this::transformArrayInit) + .addCase(ClockLtExpr.class, this::transformClockLt) + + .addCase(ClockLeqExpr.class, this::transformClockLeq) + + .addCase(ClockGtExpr.class, this::transformClockGt) + + .addCase(ClockGeqExpr.class, this::transformClockGeq) + + .addCase(ClockEqExpr.class, this::transformClockEq) + + .addCase(ClockDiffExpr.class, this::transformClockDiff) + .build(); } @@ -1194,6 +1207,42 @@ private com.microsoft.z3.Expr transformFuncApp(final FuncAppExpr expr) { } } + private com.microsoft.z3.Expr transformClockGeq(final ClockGeqExpr expr) { + final com.microsoft.z3.ArithExpr leftOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.ArithExpr rightOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getRightOp()); + return context.mkGe(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformClockGt(final ClockGtExpr expr) { + final com.microsoft.z3.ArithExpr leftOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.ArithExpr rightOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getRightOp()); + return context.mkGt(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformClockLeq(final ClockLeqExpr expr) { + final com.microsoft.z3.ArithExpr leftOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.ArithExpr rightOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getRightOp()); + return context.mkLe(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformClockLt(final ClockLtExpr expr) { + final com.microsoft.z3.ArithExpr leftOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.ArithExpr rightOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getRightOp()); + return context.mkLt(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformClockEq(final ClockEqExpr expr) { + final com.microsoft.z3.ArithExpr leftOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.ArithExpr rightOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getRightOp()); + return context.mkEq(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformClockDiff(final ClockDiffExpr expr) { + final com.microsoft.z3.ArithExpr leftOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.ArithExpr rightOpTerm = (com.microsoft.z3.ArithExpr) toTerm(expr.getRightOp()); + return context.mkSub(leftOpTerm, rightOpTerm); + } + public void reset() { exprToTerm.invalidateAll(); } diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java index fafb9e2fcb..300e1667af 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java @@ -21,6 +21,7 @@ import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.core.type.fptype.FpType; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.type.rattype.RatType; @@ -84,6 +85,8 @@ public com.microsoft.z3.Sort toSort(final Type type) { final com.microsoft.z3.Sort indexSort = toSort(arrayType.getIndexType()); final com.microsoft.z3.Sort elemSort = toSort(arrayType.getElemType()); return context.mkArraySort(indexSort, elemSort); + } else if (type instanceof ClockType) { + return realSort; } else { throw new UnsupportedOperationException("Unsupporte type: " + type.getClass().getSimpleName()); } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java index 578407d40b..fbb7b936d8 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java @@ -22,11 +22,12 @@ import hu.bme.mit.theta.common.LispStringBuilder; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.stmt.DelayStmt; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.xta.Guard; import hu.bme.mit.theta.xta.Label; import hu.bme.mit.theta.xta.Sync; @@ -51,14 +52,15 @@ import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Or; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.*; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.xta.Sync.Kind.EMIT; public abstract class XtaAction extends StmtAction { - private static final VarDecl DELAY = Var("_delay", Rat()); + private static final VarDecl DELAY = Var("_delay", Clock()); - private final Collection> clockVars; + private final Collection> clockVars; private final List sourceLocs; private XtaAction(final XtaSystem system, final List source) { @@ -81,7 +83,7 @@ public static BroadcastXtaAction broadcast(final XtaSystem system, final List> getClockVars() { + public Collection> getClockVars() { return clockVars; } @@ -551,8 +553,8 @@ public String toString() { } private static void addClocksNonNegative(final ImmutableList.Builder builder, - final Collection> clocks) { - clocks.forEach(c -> builder.add(Assume(Geq(c.getRef(), Rat(0, 1))))); + final Collection> clocks) { + clocks.forEach(c -> builder.add(Assume(Geq(c.getRef(), Int(0))))); } private static void addInvariants(final ImmutableList.Builder builder, final List locs) { @@ -587,10 +589,8 @@ private static void addUpdates(final ImmutableList.Builder builder, final edge.getUpdates().forEach(u -> builder.add(u.toStmt())); } - private static void addDelay(final ImmutableList.Builder builder, final Collection> clocks) { - builder.add(Havoc(DELAY)); - builder.add(Assume(Geq(DELAY.getRef(), Rat(0, 1)))); - clocks.forEach(c -> builder.add(Assign(c, Add(c.getRef(), DELAY.getRef())))); + private static void addDelay(final ImmutableList.Builder builder, final Collection> clocks) { + builder.add(DelayStmt.getInstance()); } private static boolean shouldApplyDelay(final List locs) { diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java index cd5bb7f2bb..ff114c218d 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaActZoneUtils.java @@ -22,7 +22,7 @@ import hu.bme.mit.theta.core.clock.op.ResetOp; 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; import hu.bme.mit.theta.xta.Guard; import hu.bme.mit.theta.xta.Update; import hu.bme.mit.theta.xta.XtaProcess.Edge; @@ -36,8 +36,8 @@ public final class XtaActZoneUtils { private XtaActZoneUtils() { } - public static Set> pre(final Set> activeVars, final XtaAction action) { - final Set> result = Containers.createSet(); + public static Set> pre(final Set> activeVars, final XtaAction action) { + final Set> result = Containers.createSet(); final List sourceLocs = action.getSourceLocs(); final List targetLocs = action.getTargetLocs(); @@ -59,7 +59,7 @@ public static Set> pre(final Set> activeVars, for (final Update update : updates) { if (update.isClockUpdate()) { final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); - final VarDecl varDecl = op.getVar(); + final VarDecl varDecl = op.getVar(); result.remove(varDecl); } } @@ -96,7 +96,7 @@ public static Set> pre(final Set> activeVars, for (final Update update : receivingEdge.getUpdates()) { if (update.isClockUpdate()) { final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); - final VarDecl varDecl = op.getVar(); + final VarDecl varDecl = op.getVar(); result.remove(varDecl); } } @@ -104,7 +104,7 @@ public static Set> pre(final Set> activeVars, for (final Update update : emittingEdge.getUpdates()) { if (update.isClockUpdate()) { final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); - final VarDecl varDecl = op.getVar(); + final VarDecl varDecl = op.getVar(); result.remove(varDecl); } } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java index 52cbc4b201..b8da22a1cf 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaLuZoneUtils.java @@ -20,7 +20,7 @@ import hu.bme.mit.theta.analysis.zone.BoundFunc; import hu.bme.mit.theta.core.clock.op.ResetOp; 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; import hu.bme.mit.theta.xta.Guard; import hu.bme.mit.theta.xta.Update; import hu.bme.mit.theta.xta.XtaProcess.Edge; @@ -83,7 +83,7 @@ private static void applyInverseUpdates(final BoundFunc.Builder succStateBuilder for (final Update update : edge.getUpdates()) { if (update.isClockUpdate()) { final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); - final VarDecl varDecl = op.getVar(); + final VarDecl varDecl = op.getVar(); succStateBuilder.remove(varDecl); } } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java index 5f6c3c65f3..e01cca17f3 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneUtils.java @@ -20,7 +20,7 @@ import hu.bme.mit.theta.analysis.zone.ZoneState; import hu.bme.mit.theta.core.clock.op.ResetOp; 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; import hu.bme.mit.theta.xta.Guard; import hu.bme.mit.theta.xta.Update; import hu.bme.mit.theta.xta.XtaProcess.Edge; @@ -266,7 +266,7 @@ private static void applyUpdates(final ZoneState.Builder builder, final Edge edg for (final Update update : edge.getUpdates()) { if (update.isClockUpdate()) { final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); - final VarDecl varDecl = op.getVar(); + final VarDecl varDecl = op.getVar(); final int value = op.getValue(); builder.reset(varDecl, value); } @@ -277,7 +277,7 @@ private static void applyInverseUpdates(final ZoneState.Builder builder, final E for (final Update update : Lists.reverse(edge.getUpdates())) { if (update.isClockUpdate()) { final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); - final VarDecl varDecl = op.getVar(); + final VarDecl varDecl = op.getVar(); final int value = op.getValue(); builder.and(Eq(varDecl, value)); builder.free(varDecl); diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java index 32f8e57830..9d56a84176 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/lu/LuZoneState.java @@ -20,9 +20,10 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Gt; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Lt; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Gt; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Lt; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import java.util.ArrayList; import java.util.Collection; @@ -40,7 +41,9 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockType; +import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.utils.ExprUtils; public final class LuZoneState implements ExprState { @@ -95,28 +98,32 @@ public Expr toExpr() { final Collection> vars = mapping.keySet(); for (final VarDecl vx : vars) { - @SuppressWarnings("unchecked") final VarDecl dx = (VarDecl) vx; + @SuppressWarnings("unchecked") final VarDecl dx = (VarDecl) vx; - @SuppressWarnings("unchecked") final ParamDecl dxp = (ParamDecl) mapping.get(dx); + @SuppressWarnings("unchecked") final ParamDecl dxp = (ParamDecl) mapping.get(dx); - final Expr x = dx.getRef(); - final Expr xp = dxp.getRef(); + final Expr x = dx.getRef(); + final Expr xp = dxp.getRef(); final Optional optLower = boundFunc.getLower(dx); if (optLower.isPresent()) { final int lower = optLower.get(); - final Expr lx = Rat(lower, 1); + final Expr lx = Int(lower); // x > xp imply xp > L(x) - final Expr lowerExpr = Imply(Gt(x, xp), Gt(xp, lx)); + final Expr xGtXp = Gt(Diff(x, xp), Int(0)); + final Expr xpGtLx = Gt(xp, lx); + final Expr lowerExpr = Imply(xGtXp, xpGtLx); conjuncts.add(lowerExpr); } final Optional optUpper = boundFunc.getUpper(dx); if (optUpper.isPresent()) { final int upper = optUpper.get(); - final Expr ux = Rat(upper, 1); + final Expr ux = Int(upper); // x < xp imply x > U(x) - final Expr upperExpr = Imply(Lt(x, xp), Gt(x, ux)); + final Expr xLtXp = Lt(Diff(x, xp), Int(0)); + final Expr xGtUx = Gt(x, ux); + final Expr upperExpr = Imply(xLtXp, xGtUx); conjuncts.add(upperExpr); } } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/Guard.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/Guard.java index 7977891b5d..860d19322d 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/Guard.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/Guard.java @@ -21,6 +21,7 @@ import hu.bme.mit.theta.core.clock.constr.ClockConstrs; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.clocktype.ClockConstraintExpr; public abstract class Guard { @@ -31,8 +32,8 @@ static DataGuard dataGuard(final Expr expr) { return new DataGuard(expr); } - static ClockGuard clockGuard(final Expr expr) { - return new ClockGuard(ClockConstrs.formExpr(expr)); + static ClockGuard clockGuard(final ClockConstraintExpr expr) { + return new ClockGuard(ClockConstrs.fromClockExpr(expr)); } public abstract Expr toExpr(); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java index 4deb2cc71b..8b0e9ada0a 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java @@ -24,6 +24,7 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.clocktype.ClockConstraintExpr; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.xta.utils.MixedDataTimeNotSupportedException; @@ -147,7 +148,8 @@ private Collection createGuards(final Collection> exprs) { if (dataExpr && !clockExpr) { guard = Guard.dataGuard(expr); } else if (!dataExpr && clockExpr) { - guard = Guard.clockGuard(expr); + assert expr instanceof ClockConstraintExpr; + guard = Guard.clockGuard((ClockConstraintExpr) expr); } else { throw new MixedDataTimeNotSupportedException(expr.toString()); } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java index 56a3ac1571..0c1374c390 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java @@ -22,7 +22,7 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.xta.XtaProcess.Loc; @@ -36,12 +36,12 @@ public final class XtaSystem { private final List processes; private final Collection> dataVars; - private final Collection> clockVars; + private final Collection> clockVars; private final MutableValuation initVal; private final List unmodProcesses; private final Collection> unmodDataVars; - private final Collection> unmodClockVars; + private final Collection> unmodClockVars; private Expr prop; @@ -70,7 +70,7 @@ public Collection> getDataVars() { return unmodDataVars; } - public Collection> getClockVars() { + public Collection> getClockVars() { return unmodClockVars; } @@ -93,7 +93,7 @@ public void addDataVar(final VarDecl varDecl, final LitExpr initValue) { initVal.put(varDecl, initValue); } - public void addClockVar(final VarDecl varDecl) { + public void addClockVar(final VarDecl varDecl) { checkNotNull(varDecl); checkArgument(!dataVars.contains(varDecl)); clockVars.add(varDecl); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java index a54f74eb17..64fde1b153 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java @@ -31,6 +31,8 @@ import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.core.type.inttype.IntLitExpr; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.type.inttype.IntModExpr; @@ -66,6 +68,7 @@ import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Div; import static hu.bme.mit.theta.core.type.inttype.IntExprs.*; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; @@ -303,6 +306,11 @@ public Expr visitEqualityExpression(final EqualityExpressionContext ctx) { final EqualityOpContext op = Utils.singleElementOf(ctx.fOpers); if (op.fEqOp != null) { + if (leftOp.getType() instanceof ClockType) { + final Expr clock = cast(leftOp, Clock()); + final Expr value = cast(rightOp, Int()); + return ClockExprs.Eq(clock, value); + } return Eq(leftOp, rightOp); } else if (op.fNeqOp != null) { return Neq(leftOp, rightOp); @@ -321,6 +329,23 @@ public Expr visitRelationalExpression(final RelationalExpressionContext ctx) final Expr rightOp = ctx.fOps.get(1).accept(this); final RelationalOpContext op = Utils.singleElementOf(ctx.fOpers); + + if (leftOp.getType() instanceof ClockType) { + final Expr clock = cast(leftOp, Clock()); + final Expr value = cast(rightOp, Int()); + if (op.fLtOp != null) { + return ClockExprs.Lt(clock, value); + } else if (op.fLeqOp != null) { + return ClockExprs.Leq(clock, value); + } else if (op.fGtOp != null) { + return ClockExprs.Gt(clock, value); + } else if (op.fGeqOp != null) { + return ClockExprs.Geq(clock, value); + } else { + throw new AssertionError(); + } + } + if (op.fLtOp != null) { return Lt(leftOp, rightOp); } else if (op.fLeqOp != null) { diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java index 9b5032d9ef..f35c659e44 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java @@ -26,7 +26,7 @@ import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.xta.Label; import hu.bme.mit.theta.xta.XtaProcess; import hu.bme.mit.theta.xta.XtaProcess.Loc; @@ -136,7 +136,7 @@ private void createAllLocalVariables(final XtaProcess process, final Env env) { env.define(variable, label); env.define_in_parent(variable, label); } else if (instantiateResult.isClockVariable()) { - final VarDecl varDecl = instantiateResult.asClockVariable().getVarDecl(); + final VarDecl varDecl = instantiateResult.asClockVariable().getVarDecl(); env.define(variable, varDecl); env.define_in_parent(variable, varDecl); process.getSystem().addClockVar(varDecl); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java index bd72505b1f..955c034d35 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java @@ -25,7 +25,7 @@ import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.xta.Label; import hu.bme.mit.theta.xta.XtaSystem; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser; @@ -173,7 +173,7 @@ private void createAllGlobalVariables(final XtaSystem system, final Env env) { final Label label = instantiateResult.asChannel().getLabel(); env.define(variable, label); } else if (instantiateResult.isClockVariable()) { - final VarDecl varDecl = instantiateResult.asClockVariable().getVarDecl(); + final VarDecl varDecl = instantiateResult.asClockVariable().getVarDecl(); env.define(variable, varDecl); system.addClockVar(varDecl); } else if (instantiateResult.isDataVariable()) { diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaVariableSymbol.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaVariableSymbol.java index 80ede43e1e..e634009d8b 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaVariableSymbol.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaVariableSymbol.java @@ -27,7 +27,7 @@ import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.inttype.IntType; -import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.xta.Label; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.TypeContext; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.VariableIdContext; @@ -41,7 +41,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; final class XtaVariableSymbol implements Symbol { @@ -137,7 +137,7 @@ public InstantiateResult instantiate(final String prefix, final Env env) { } else if (initialiser != null) { throw new UnsupportedOperationException("Clock " + name + " should not be initialized."); } else { - final VarDecl varDecl = Decls.Var(prefix + name, Rat()); + final VarDecl varDecl = Decls.Var(prefix + name, Clock()); return InstantiateResult.clockVariable(varDecl); } } else if (isChanArrayType(varType)) { @@ -213,7 +213,7 @@ public static InstantiateResult constant(final LitExpr expr) { return new Constant(expr); } - public static InstantiateResult clockVariable(final VarDecl varDecl) { + public static InstantiateResult clockVariable(final VarDecl varDecl) { return new ClockVariable(varDecl); } @@ -288,9 +288,9 @@ public LitExpr getInitValue() { } public static final class ClockVariable extends InstantiateResult{ - private final VarDecl varDecl; + private final VarDecl varDecl; - private ClockVariable(final VarDecl varDecl) { + private ClockVariable(final VarDecl varDecl) { this.varDecl = checkNotNull(varDecl); } @@ -304,7 +304,7 @@ public ClockVariable asClockVariable() { return this; } - public VarDecl getVarDecl() { + public VarDecl getVarDecl() { return varDecl; } }