From d4519c9f3ecf2ead565710eec75b8820e82c3c4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hajdu=20=C3=81kos?= <hajdua@mit.bme.hu>
Date: Thu, 30 Jul 2020 11:56:27 +0200
Subject: [PATCH] Support XOR in STS DSL

---
 build.gradle.kts                              |  2 +-
 subprojects/sts/README.md                     |  2 +-
 subprojects/sts/src/main/antlr/StsDsl.g4      |  9 +++++++-
 .../theta/sts/dsl/StsExprCreatorVisitor.java  | 23 +++++++++++--------
 4 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/build.gradle.kts b/build.gradle.kts
index a22e2aed1f..2c18f970d5 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "1.4.1"
+    version = "1.4.2"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
diff --git a/subprojects/sts/README.md b/subprojects/sts/README.md
index 78f73067ca..8351b08973 100644
--- a/subprojects/sts/README.md
+++ b/subprojects/sts/README.md
@@ -34,7 +34,7 @@ Expressions of the STS include the following.
 - Primed expressions (only in transition expression) to represent the next state, e.g., `x'`.
 - Literals, e.g., `true`, `false` (Bool), `0`, `123` (integer), `4 % 5` (rational).
 - Comparison, e.g., `=`, `/=`, `<`, `>`, `<=`, `>=`.
-- Boolean operators, e.g., `and`, `or`, `not`, `imply`, `iff`.
+- Boolean operators, e.g., `and`, `or`, `xor`, `not`, `imply`, `iff`.
 - Arithmetic, e.g., `+`, `-`, `/`, `*`, `mod`, `rem`.
 - Conditional: `if . then . else .`
 - Array read (`a[i]`) and write (`a[i <- v]`).
diff --git a/subprojects/sts/src/main/antlr/StsDsl.g4 b/subprojects/sts/src/main/antlr/StsDsl.g4
index aa23dbf312..42aed2a5df 100644
--- a/subprojects/sts/src/main/antlr/StsDsl.g4
+++ b/subprojects/sts/src/main/antlr/StsDsl.g4
@@ -211,7 +211,11 @@ existsExpr
 	;
 
 orExpr
-	:	ops+=andExpr (OR ops+=andExpr)*
+	:	ops+=xorExpr (OR ops+=xorExpr)*
+	;
+
+xorExpr
+	:	leftOp=andExpr (XOR rightOp=xorExpr)?
 	;
 
 andExpr
@@ -331,6 +335,9 @@ OR	:	'or'
 AND	:	'and'
 	;
 
+XOR	:	'xor'
+	;
+
 NOT	:	'not'
 	;
 
diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java
index 805f3232c7..c651c18cc1 100644
--- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java
+++ b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java
@@ -32,16 +32,7 @@
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neq;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Sub;
 import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Iff;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*;
 import static hu.bme.mit.theta.core.type.functype.FuncExprs.Func;
 import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
 import static hu.bme.mit.theta.core.type.inttype.IntExprs.Mod;
@@ -107,6 +98,7 @@
 import hu.bme.mit.theta.sts.dsl.gen.StsDslParser.RatLitExprContext;
 import hu.bme.mit.theta.sts.dsl.gen.StsDslParser.RelationExprContext;
 import hu.bme.mit.theta.sts.dsl.gen.StsDslParser.TrueExprContext;
+import hu.bme.mit.theta.sts.dsl.gen.StsDslParser.XorExprContext;
 
 final class StsExprCreatorVisitor extends StsDslBaseVisitor<Expr<?>> {
 
@@ -230,6 +222,17 @@ public Expr<?> visitOrExpr(final OrExprContext ctx) {
 		}
 	}
 
+	@Override
+	public Expr<?> visitXorExpr(final XorExprContext ctx) {
+		if (ctx.rightOp != null) {
+			final Expr<BoolType> leftOp = TypeUtils.cast(ctx.leftOp.accept(this), Bool());
+			final Expr<BoolType> rightOp = TypeUtils.cast(ctx.rightOp.accept(this), Bool());
+			return Xor(leftOp, rightOp);
+		} else {
+			return visitChildren(ctx);
+		}
+	}
+
 	@Override
 	public Expr<?> visitAndExpr(final AndExprContext ctx) {
 		if (ctx.ops.size() > 1) {