Clock transformer fixes (reset to value, use cast from int)

ftsrg · Dec 18, 2023 · c790656 · c790656
1 parent 0dd8a53
commit c790656
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 22 deletions.
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/impl/ClockImpl.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/impl/ClockImpl.java
@@ -13,7 +13,6 @@
 import hu.bme.mit.theta.core.type.clocktype.ClockDiffExpr;
 import hu.bme.mit.theta.core.type.clocktype.ClockType;
 import hu.bme.mit.theta.core.type.inttype.IntType;
-import hu.bme.mit.theta.core.type.rattype.RatExprs;
 
 import java.util.ArrayList;
 import java.util.Collection;
@@ -22,12 +21,12 @@
 
 import static com.google.common.base.Preconditions.checkNotNull;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
+import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
 import static java.util.stream.Collectors.toList;
 
 public abstract class ClockImpl<CType extends Ordered<CType>> {
 
     private final HashMap<Decl<ClockType>, VarDecl<CType>> clockLut;
-    private final VarDecl<CType> delayVar;
     private Stmt delayStmt;
 
     protected ClockImpl(final Collection<VarDecl<ClockType>> clocks) {
@@ -37,13 +36,10 @@ protected ClockImpl(final Collection<VarDecl<ClockType>> clocks) {
             final VarDecl<CType> newVar = Decls.Var(clock.getName(), type());
             clockLut.put(clock, newVar);
         }
-        delayVar = Decls.Var("__delay", type());
     }
 
     protected abstract CType type();
 
-    protected abstract Expr<CType> zeroExpr();
-
     protected abstract Expr<CType> addExpr(final Expr<CType> leftOp, final Expr<CType> rightOp);
 
     protected abstract Expr<CType> subExpr(final Expr<CType> leftOp, final Expr<CType> rightOp);
@@ -116,13 +112,20 @@ public Stmt visit(IfStmt stmt, Void param) {
             public Stmt visit(DelayStmt stmt, Void param) {
                 if (delayStmt == null) {
                     final List<Stmt> stmts = new ArrayList<>();
+
+                    final VarDecl<CType> delayVar = Decls.Var("__delay", type());
                     stmts.add(HavocStmt.of(delayVar));
-                    stmts.add(AssumeStmt.of(type().Geq(delayVar.getRef(), zeroExpr())));
+
+                    final Expr<IntType> intZeroExpr = Int(0);
+                    final Expr<CType> tZeroExpr = IntType.getInstance().Cast(intZeroExpr, type());
+                    stmts.add(AssumeStmt.of(type().Geq(delayVar.getRef(), tZeroExpr)));
+
                     for (Decl<ClockType> clock : clockLut.keySet()) {
                         final VarDecl<CType> replacementVar = clockLut.get(clock);
                         final Expr<CType> addDelayExpr = addExpr(replacementVar.getRef(), delayVar.getRef());
                         stmts.add(AssignStmt.of(replacementVar, addDelayExpr));
                     }
+
                     delayStmt = SequenceStmt.of(stmts);
                 }
                 return delayStmt;
@@ -131,8 +134,12 @@ public Stmt visit(DelayStmt stmt, Void param) {
             @Override
             public Stmt visit(ResetStmt stmt, Void param) {
                 final VarDecl<ClockType> clockVar = stmt.getClockDecl();
-                final VarDecl<CType> var = clockLut.get(clockVar);
-                return AssignStmt.of(var, zeroExpr());
+                final VarDecl<CType> tVar = clockLut.get(clockVar);
+
+                final Expr<IntType> intValueExpr = Int(stmt.getValue());
+                final Expr<CType> tValueExpr = IntType.getInstance().Cast(intValueExpr, type());
+
+                return AssignStmt.of(tVar, tValueExpr);
             }
 
             private List<Stmt> visitStmts(final List<Stmt> stmts) {

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/impl/IntClockImpl.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/impl/IntClockImpl.java
@@ -13,8 +13,6 @@
 
 public final class IntClockImpl extends ClockImpl<IntType> {
 
-    private static final Expr<IntType> ZERO = Int(0);
-
     protected IntClockImpl(final Collection<VarDecl<ClockType>> clocks) {
         super(clocks);
     }
@@ -28,11 +26,6 @@ protected IntType type() {
         return Int();
     }
 
-    @Override
-    protected Expr<IntType> zeroExpr() {
-        return ZERO;
-    }
-
     @Override
     protected Expr<IntType> addExpr(Expr<IntType> leftOp, Expr<IntType> rightOp) {
         return Add(leftOp, rightOp);

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/impl/RatClockImpl.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/impl/RatClockImpl.java
@@ -13,8 +13,6 @@
 
 public final class RatClockImpl extends ClockImpl<RatType> {
 
-    private static final Expr<RatType> ZERO = Rat(0, 1);
-
     protected RatClockImpl(final Collection<VarDecl<ClockType>> clocks) {
         super(clocks);
     }
@@ -28,11 +26,6 @@ protected RatType type() {
         return Rat();
     }
 
-    @Override
-    protected Expr<RatType> zeroExpr() {
-        return ZERO;
-    }
-
     @Override
     protected Expr<RatType> addExpr(Expr<RatType> leftOp, Expr<RatType> rightOp) {
         return Add(leftOp, rightOp);

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java
@@ -123,6 +123,10 @@ public IntGeqExpr Geq(final Expr<IntType> leftOp, final Expr<IntType> rightOp) {
 
 	@Override
 	public <TargetType extends Type> Expr<TargetType> Cast(final Expr<IntType> op, final TargetType type) {
+		if (type instanceof IntType) {
+			@SuppressWarnings("unchecked") final Expr<TargetType> result = (Expr<TargetType>) op;
+			return result;
+		}
 		if (type instanceof RatType) {
 			@SuppressWarnings("unchecked") final Expr<TargetType> result = (Expr<TargetType>) IntExprs.ToRat(op);
 			return result;

diff --git a/...xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/clocks/XstsClockReplacers.java b/...xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/clocks/XstsClockReplacers.java
@@ -54,6 +54,9 @@ private static <T extends Ordered<T>> XSTS replaceClocks(
                 .filter(v -> v.getType() instanceof ClockType)
                 .map(v -> cast(v, Clock()))
                 .toList();
+        if (clockVars.isEmpty()) {
+            return xsts;
+        }
         final ClockImpl<T> clockImpl = clockImplFromClocks.apply(clockVars);
 
         final Map<VarDecl<?>, XstsType<?>> varToType = xsts.getVarToType();