Merge pull request #104 from ftsrg/xsts-dev

Added array support to XSTS
ftsrg · Feb 11, 2021 · f747803 · f747803
2 parents bf33eec + 0201ae3
commit f747803
Show file tree

Hide file tree

Showing 8 changed files with 88 additions and 16 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.9.3"
+    version = "2.10.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java
@@ -110,7 +110,7 @@ public static Collection<Object[]> data() {
 
 				{ "src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PRED_CART},
 
-				{ "src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.EXPL},
+//				{ "src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.EXPL},
 
 //				{ "src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PROD},
 
@@ -184,14 +184,30 @@ public static Collection<Object[]> data() {
 
 				{ "src/test/resources/model/css2003.xsts", "src/test/resources/property/css2003.prop", true, XstsConfigBuilder.Domain.EXPL},
 
-				{ "src/test/resources/model/css2003.xsts", "src/test/resources/property/css2003.prop", true, XstsConfigBuilder.Domain.PROD}
+				{ "src/test/resources/model/css2003.xsts", "src/test/resources/property/css2003.prop", true, XstsConfigBuilder.Domain.PROD},
 
 //				{ "src/test/resources/model/ort.xsts", "src/test/resources/property/x_gt_2.prop", false, XstsConfigBuilder.Domain.PRED_CART},
 
 //				{ "src/test/resources/model/ort2.xsts", "src/test/resources/property/ort2.prop", true, XstsConfigBuilder.Domain.PRED_CART},
 
 //				{ "src/test/resources/model/crossroad_composite.xsts", "src/test/resources/property/both_green.prop", true, XstsConfigBuilder.Domain.EXPL}
 
+				{ "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.PRED_CART},
+
+				{ "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.EXPL},
+
+				{ "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.PROD},
+
+				{ "src/test/resources/model/array_counter.xsts", "src/test/resources/property/array_10.prop", false, XstsConfigBuilder.Domain.PROD_AUTO},
+
+				{ "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PRED_CART},
+
+				{ "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.EXPL},
+
+				{ "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PROD},
+
+				{ "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PROD_AUTO}
+
 		});
 	}
 
@@ -210,7 +226,7 @@ public void test() throws IOException {
 				e.printStackTrace();
 			}
 
-			final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).logger(logger).build(xsts);
+			final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).initPrec(XstsConfigBuilder.InitPrec.CTRL).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).logger(logger).build(xsts);
 			final SafetyResult<?, ?> status = configuration.check();
 			if (safe) {
 				assertTrue(status.isSafe());

diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/array_constant.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/array_constant.xsts
@@ -0,0 +1,11 @@
+var arr: [integer] -> boolean = [0 <- true, 1 <- true, 2 <- true, default <- false]
+var n: integer = 0
+
+trans {
+    assume arr[n]==true;
+    n:=n+1;
+}
+
+init {}
+
+env {}
diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/array_counter.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/array_counter.xsts
@@ -0,0 +1,11 @@
+var arr: [integer] -> boolean = [<integer>default<-false]
+ctrl var n: integer = 0
+
+trans{
+    arr:=arr[n<-true];
+    n:=n+1;
+}
+
+init{}
+
+env{}
diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/array_10.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/array_10.prop
@@ -0,0 +1,3 @@
+prop {
+    arr[10]!=true
+}
diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/array_constant.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/array_constant.prop
@@ -0,0 +1,3 @@
+prop {
+    n<=3
+}
diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md
@@ -37,7 +37,13 @@ Example:
 
 ### Variable declarations
 
-The XSTS formalism contains the following built-in types: `integer`, `boolean`. Previously declared custom types can also be used in variable declarations.
+The XSTS formalism contains the following built-in types: 
+
+* `integer`: Mathematical, unbounded SMT integers.
+* `boolean`: Booleans.
+* `[K] -> V`: SMT arrays (associative maps) from a given key type `K` to a value type `V`.
+
+Previously declared custom types can also be used in variable declarations.
 Variables can be declared the following way:
 
 `var <name> : <type>`
@@ -61,6 +67,18 @@ ctrl var x : integer = 0
 
 All variable names matching the pattern `temp([0-9])+` are reserved for use by the model checker.
 
+### Expressions
+
+Expressions of the XSTS can include the following:
+
+* Identifiers (variables).
+* Literals, e.g., `true`, `false` (boolean), `0`, `123` (integer).
+    * Array literals can be given by listing the key-value pairs and the (mandatory) default element, e.g., `[0 <- 182, 1 <- 41, default <- 75]`. If there are no elements, the key type has to be given before the default element, e.g., `[<integer>default <- 75]`.
+* Comparison, e.g., `==`, `!=`, `<`, `>`, `<=`, `>=`.
+* Boolean operators, e.g., `&&`, `||`, `!`, `->`.
+* Arithmetic, e.g., `+`, `-`, `/`, `*`, `%`.
+* Array read (`a[i]`) and write (`a[i <- v]`).
+
 ### Transitions
 
 The behaviour of XSTSs can be described using transitions. A transition is an atomic sequence of statements. Statements can be:

diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XSTSVisitor.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XSTSVisitor.java
@@ -201,8 +201,13 @@ public Expr<?> visitNotExpr(XstsDslParser.NotExprContext ctx) {
 	@Override
 	public Expr<?> visitEqExpr(XstsDslParser.EqExprContext ctx) {
 		if (ctx.ops.size() > 1) {
-			if (ctx.oper.EQ() != null) return Eq(visitRelationExpr(ctx.ops.get(0)), visitRelationExpr(ctx.ops.get(1)));
-			else return Neq(visitRelationExpr(ctx.ops.get(0)), visitRelationExpr(ctx.ops.get(1)));
+			try{
+				if (ctx.oper.EQ() != null) return Eq(visitRelationExpr(ctx.ops.get(0)), visitRelationExpr(ctx.ops.get(1)));
+				else return Neq(visitRelationExpr(ctx.ops.get(0)), visitRelationExpr(ctx.ops.get(1)));
+			} catch(Exception ex){
+				throw new ParseException(ctx,ex.getMessage());
+			}
+
 		} else return visitRelationExpr(ctx.ops.get(0));
 	}
 
@@ -214,15 +219,20 @@ public Expr<?> visitEqOperator(XstsDslParser.EqOperatorContext ctx) {
 	@Override
 	public Expr<?> visitRelationExpr(XstsDslParser.RelationExprContext ctx) {
 		if (ctx.ops.size() > 1) {
-			if (ctx.oper.LEQ() != null) {
-				return Leq(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
-			} else if (ctx.oper.GEQ() != null) {
-				return Geq(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
-			} else if (ctx.oper.LT() != null) {
-				return Lt(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
-			} else if (ctx.oper.GT() != null) {
-				return Gt(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
-			} else throw new ParseException(ctx, "Unsupported operation '" + ctx.oper.getText() + "'");
+			try{
+				if (ctx.oper.LEQ() != null) {
+					return Leq(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
+				} else if (ctx.oper.GEQ() != null) {
+					return Geq(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
+				} else if (ctx.oper.LT() != null) {
+					return Lt(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
+				} else if (ctx.oper.GT() != null) {
+					return Gt(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1)));
+				} else throw new ParseException(ctx, "Unsupported operation '" + ctx.oper.getText() + "'");
+			} catch (Exception ex){
+				throw new ParseException(ctx,ex.getMessage());
+			}
+
 		} else return visitAdditiveExpr(ctx.ops.get(0));
 	}
-Original file line number
+Diff line change
@@ -0,0 +1,3 @@
+    prop {
+        n<=3
+    }