From 707f11a8dccd15e73540159d188629da4d2e0235 Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 8 Feb 2021 10:06:20 +0100 Subject: [PATCH 1/6] Rethrowing exceptions with line numbers --- .../bme/mit/theta/xsts/dsl/XSTSVisitor.java | 32 ++++++++++++------- 1 file changed, 21 insertions(+), 11 deletions(-) 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 index 0fcc6bc9e1..1397f02535 100644 --- 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)); } From b3594a40167ddd05f8902da743d53ef7090f8347 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 11 Feb 2021 16:54:31 +0100 Subject: [PATCH 2/6] Added test cases for arrays --- .../hu/bme/mit/theta/xsts/analysis/XstsTest.java | 12 +++++++++--- .../src/test/resources/model/array_counter.xsts | 11 +++++++++++ .../src/test/resources/property/array_10.prop | 3 +++ 3 files changed, 23 insertions(+), 3 deletions(-) create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/array_counter.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/array_10.prop 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 index 739612b8fc..6968b2f3a9 100644 --- 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 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,7 +184,7 @@ public static Collection 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}, @@ -192,6 +192,12 @@ public static Collection data() { // { "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} + }); } @@ -210,7 +216,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_counter.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/array_counter.xsts new file mode 100644 index 0000000000..abedee00cf --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/array_counter.xsts @@ -0,0 +1,11 @@ +var arr: [integer] -> boolean = [default<-false] +ctrl var n: integer = 0 + +trans{ + n:=n+1; + arr:=arr[n<-true]; +} + +init{} + +env{} \ No newline at end of file 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 new file mode 100644 index 0000000000..f7dc16fe06 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/array_10.prop @@ -0,0 +1,3 @@ +prop { + arr[10]!=true +} \ No newline at end of file From 87b46aeb5d60a828e465715455468c8331eb343b Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 11 Feb 2021 18:03:56 +0100 Subject: [PATCH 3/6] Added test cases for arrays, updated readme --- .../bme/mit/theta/xsts/analysis/XstsTest.java | 12 ++++++++++- .../test/resources/model/array_constant.xsts | 11 ++++++++++ .../test/resources/model/array_counter.xsts | 2 +- .../resources/property/array_constant.prop | 3 +++ subprojects/xsts/xsts/README.md | 20 ++++++++++++++++++- 5 files changed, 45 insertions(+), 3 deletions(-) create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/array_constant.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/array_constant.prop 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 index 6968b2f3a9..0007e6c480 100644 --- 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 @@ -196,7 +196,17 @@ public static Collection data() { { "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}, + + { "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} }); } 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 new file mode 100644 index 0000000000..f2810872ff --- /dev/null +++ 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 {} \ No newline at end of file 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 index abedee00cf..c344f0b38e 100644 --- a/subprojects/xsts/xsts-analysis/src/test/resources/model/array_counter.xsts +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/array_counter.xsts @@ -2,8 +2,8 @@ var arr: [integer] -> boolean = [default<-false] ctrl var n: integer = 0 trans{ - n:=n+1; arr:=arr[n<-true]; + n:=n+1; } init{} 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 new file mode 100644 index 0000000000..dbf7e69fe5 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/array_constant.prop @@ -0,0 +1,3 @@ +prop { + n<=3 +} \ No newline at end of file diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md index 5fd204f362..66e01b2217 100644 --- 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 : ` @@ -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., `[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: From 016be2cb962d52a49585b8ff64b41dd0e1a452a8 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 11 Feb 2021 18:19:02 +0100 Subject: [PATCH 4/6] Fixed codacy warnings for readme --- subprojects/xsts/xsts/README.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md index 66e01b2217..765742f26c 100644 --- a/subprojects/xsts/xsts/README.md +++ b/subprojects/xsts/xsts/README.md @@ -71,13 +71,13 @@ All variable names matching the pattern `temp([0-9])+` are reserved for use by t 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., `[default <- 75]`. -- Comparison, e.g., `==`, `!=`, `<`, `>`, `<=`, `>=`. -- Boolean operators, e.g., `&&`, `||`, `!`, `->`. -- Arithmetic, e.g., `+`, `-`, `/`, `*`, `%`. -- Array read (`a[i]`) and write (`a[i <- v]`). +* 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., `[default <- 75]`. +* Comparison, e.g., `==`, `!=`, `<`, `>`, `<=`, `>=`. +* Boolean operators, e.g., `&&`, `||`, `!`, `->`. +* Arithmetic, e.g., `+`, `-`, `/`, `*`, `%`. +* Array read (`a[i]`) and write (`a[i <- v]`). ### Transitions From ddd2151d244f2379b6821044077b3aadf6ac00f5 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 11 Feb 2021 18:27:43 +0100 Subject: [PATCH 5/6] Fixed codacy warnings for readme --- subprojects/xsts/xsts/README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md index 765742f26c..0b717b02ef 100644 --- a/subprojects/xsts/xsts/README.md +++ b/subprojects/xsts/xsts/README.md @@ -39,9 +39,9 @@ Example: 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`. +* `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: From 0201ae385a6b37d46bd40af73a0efb9bb711b5f0 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 11 Feb 2021 18:58:37 +0100 Subject: [PATCH 6/6] Bump version --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 01f54307f9..72f3562b4e 100644 --- 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")) }