Parse XSTS with clocks in right op of relation exprs

ftsrg · Dec 18, 2023 · 79ecd0d · 79ecd0d
1 parent c790656
commit 79ecd0d
Showing 1 changed file with 19 additions and 4 deletions.
diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java
@@ -245,11 +245,12 @@ public Expr<?> visitRelationExpr(final RelationExprContext ctx) {
 			if (ctx.rightOp != null) {
 				final Expr<?> leftOp = ctx.leftOp.accept(this);
 				final Expr<?> rightOp = ctx.rightOp.accept(this);
+				final int operType = ctx.oper.getType();
 
 				if (leftOp.getType() instanceof ClockType) {
 					final Expr<ClockType> clock = cast(leftOp, Clock());
 					final Expr<IntType> value = cast(rightOp, Int());
-					switch (ctx.oper.getType()) {
+					switch (operType) {
 						case LT:
 							return ClockExprs.Lt(clock, value);
 						case LEQ:
@@ -258,14 +259,28 @@ public Expr<?> visitRelationExpr(final RelationExprContext ctx) {
 							return ClockExprs.Gt(clock, value);
 						case GEQ:
 							return ClockExprs.Geq(clock, value);
-						case EQ:
-							return ClockExprs.Eq(clock, value);
+						default:
+							throw new ParseException(ctx, "Unknown operator");
+					}
+				}
+				if (rightOp.getType() instanceof ClockType) {
+					final Expr<IntType> value = cast(leftOp, Int());
+					final Expr<ClockType> clock = cast(rightOp, Clock());
+					switch (operType) {
+						case LT:
+							return ClockExprs.Gt(clock, value);
+						case LEQ:
+							return ClockExprs.Geq(clock, value);
+						case GT:
+							return ClockExprs.Lt(clock, value);
+						case GEQ:
+							return ClockExprs.Leq(clock, value);
 						default:
 							throw new ParseException(ctx, "Unknown operator");
 					}
 				}
 
-				switch (ctx.oper.getType()) {
+				switch (operType) {
 					case LT:
 						return Lt(leftOp, rightOp);
 					case LEQ: