remove deprecated feature: check files

tests-large-partial/partial-1.output

@@ -1,4 +1,4 @@
-Processed 2 (of 50) models, 0 checks and 5 (of 159) requirement files and found no issues
+Processed 2 (of 50) models, and 5 (of 159) requirement files and found no issues
 > [Included] Model large/generic.rsl (Package generic)
 > [Included] Model large/package_1.rsl (Package package_1)
 > [Excluded] Model large/package_10.rsl (Package package_10)

tests-large-partial/partial-2.output

@@ -1,4 +1,4 @@
-Processed 4 (of 50) models, 0 checks and 10 (of 159) requirement files and found no issues
+Processed 4 (of 50) models, and 10 (of 159) requirement files and found no issues
 > [Included] Model large/generic.rsl (Package generic)
 > [Excluded] Model large/package_1.rsl (Package package_1)
 > [Excluded] Model large/package_10.rsl (Package package_10)

tests-system/array-length/output

@@ -2,4 +2,4 @@ values = ["one", "two", "three"]
                         ^^^^^^^ array-length/foo.trlc:4: error: this array requires at most 2 elements (3 provided)
 values = ["one"]
                ^ array-length/foo.trlc:8: error: this array requires at least 2 elements (only 1 provided)
-Processed 1 model, 0 checks and 1 requirement file and found 2 errors
+Processed 1 model, and 1 requirement file and found 2 errors

tests-system/array-length/output.json

@@ -16,4 +16,4 @@ values = ["one"]
     ]
   }
 }
-Processed 1 model, 0 checks and 1 requirement file and found 2 errors
+Processed 1 model, and 1 requirement file and found 2 errors

tests-system/array-length/output.smtlib

@@ -2,4 +2,4 @@ values = ["one", "two", "three"]
                         ^^^^^^^ array-length/foo.trlc:4: error: this array requires at most 2 elements (3 provided)
 values = ["one"]
                ^ array-length/foo.trlc:8: error: this array requires at least 2 elements (only 1 provided)
-Processed 1 model, 0 checks and 1 requirement file and found 2 errors
+Processed 1 model, and 1 requirement file and found 2 errors

tests-system/array-membership-1/output

@@ -10,4 +10,4 @@ arr    = []
          ^ array-membership-1/foo.trlc:34: check warning: 42 is not in array
 arr    = []
          ^ array-membership-1/foo.trlc:34: check warning: 42 is in array
-Processed 1 model, 0 checks and 1 requirement file and found 6 warnings
+Processed 1 model, and 1 requirement file and found 6 warnings

tests-system/array-membership-1/output.json

@@ -64,4 +64,4 @@ arr    = []
     "is_not": true
   }
 }
-Processed 1 model, 0 checks and 1 requirement file and found 6 warnings
+Processed 1 model, and 1 requirement file and found 6 warnings

tests-system/array-membership-1/output.smtlib

@@ -10,4 +10,4 @@ arr    = []
          ^ array-membership-1/foo.trlc:34: check warning: 42 is not in array
 arr    = []
          ^ array-membership-1/foo.trlc:34: check warning: 42 is in array
-Processed 1 model, 0 checks and 1 requirement file and found 6 warnings
+Processed 1 model, and 1 requirement file and found 6 warnings

tests-system/array-membership-2/output

@@ -1,3 +1,3 @@
 ival in arr, warning "potato"
 ^^^^ array-membership-2/foo.rsl:9: error: expected expression of type Builtin_String, got Builtin_Integer instead
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/array-membership-2/output.json

@@ -1,3 +1,3 @@
 ival in arr, warning "potato"
 ^^^^ array-membership-2/foo.rsl:9: error: expected expression of type Builtin_String, got Builtin_Integer instead
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/array-membership-2/output.smtlib

@@ -1,3 +1,3 @@
 ival in arr, warning "potato"
 ^^^^ array-membership-2/foo.rsl:9: error: expected expression of type Builtin_String, got Builtin_Integer instead
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/array-membership-3/output

@@ -1,3 +1,3 @@
 kitten in arr, warning "does not reference kitten"
 ^^^^^^ array-membership-3/foo.rsl:10: error: unknown symbol kitten
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/array-membership-3/output.json

@@ -1,3 +1,3 @@
 kitten in arr, warning "does not reference kitten"
 ^^^^^^ array-membership-3/foo.rsl:10: error: unknown symbol kitten
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/array-membership-3/output.smtlib

@@ -1,3 +1,3 @@
 kitten in arr, warning "does not reference kitten"
 ^^^^^^ array-membership-3/foo.rsl:10: error: unknown symbol kitten
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/arrays-1/output

@@ -1,3 +1,3 @@
 arr = [1, 2, 3]
       ^ arrays-1/example.trlc:8: check error: potato
-Processed 1 model, 0 checks and 1 requirement file and found 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/arrays-1/output.json

@@ -1,3 +1,3 @@
 arr = [1, 2, 3]
       ^ arrays-1/example.trlc:8: check error: potato
-Processed 1 model, 0 checks and 1 requirement file and found 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/arrays-1/output.smtlib

@@ -1,3 +1,3 @@
 arr = [1, 2, 3]
       ^ arrays-1/example.trlc:8: check error: potato
-Processed 1 model, 0 checks and 1 requirement file and found 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/arrays-2/output

@@ -1,3 +1,3 @@
 arr[0] == len(arr), "potato", arr
 ^^^ arrays-2/example.rsl:8: error: expression 'arr' has type Integer, which is not an array
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/arrays-2/output.json

@@ -1,3 +1,3 @@
 arr[0] == len(arr), "potato", arr
 ^^^ arrays-2/example.rsl:8: error: expression 'arr' has type Integer, which is not an array
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/arrays-2/output.smtlib

@@ -1,3 +1,3 @@
 arr[0] == len(arr), "potato", arr
 ^^^ arrays-2/example.rsl:8: error: expression 'arr' has type Integer, which is not an array
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/base-types/bar.rsl

@@ -13,3 +13,13 @@
 
 
             }
+
+             checks MyType {
+
+
+               int_ok == 42, error "int must be 42", int_ok
+               int_nok == 42, error "int must be 42", int_nok
+               int_null == null, error "int must be null", int_null
+
+
+               }

tests-system/base-types/output

@@ -1,5 +1,3 @@
-checks MyType {
-       ^^^^^^ base-types/checks.check:4: issue: move this check block into bar.rsl:1 [deprecated_feature]
 int_nok = 24
           ^^ base-types/instances.trlc:10: check error: int must be 42
-Processed 1 model, 1 check and 1 requirement file and found 1 warning and 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/base-types/output.json

@@ -1,3 +1,3 @@
 int_nok = 24
           ^^ base-types/instances.trlc:10: check error: int must be 42
-Processed 1 model, 1 check and 1 requirement file and found 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/base-types/output.smtlib

@@ -1,5 +1,3 @@
-checks MyType {
-       ^^^^^^ base-types/checks.check:4: issue: move this check block into bar.rsl:1 [deprecated_feature]
 int_nok = 24
           ^^ base-types/instances.trlc:10: check error: int must be 42
-Processed 1 model, 1 check and 1 requirement file and found 1 warning and 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/bazel-dirs/output

@@ -1 +1 @@
-Processed 1 model, 0 checks and 0 requirement files and found no issues
+Processed 1 model, and 0 requirement files and found no issues

tests-system/bazel-dirs/output.json

@@ -1,2 +1,2 @@
 {}
-Processed 1 model, 0 checks and 0 requirement files and found no issues
+Processed 1 model, and 0 requirement files and found no issues

tests-system/bazel-dirs/output.smtlib

@@ -1 +1 @@
-Processed 1 model, 0 checks and 0 requirement files and found no issues
+Processed 1 model, and 0 requirement files and found no issues

tests-system/builtin-1/output

@@ -1,3 +1,3 @@
 len = 2
       ^ builtin-1/example.trlc:10: check warning: potato
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+Processed 1 model, and 1 requirement file and found 1 warning

tests-system/builtin-1/output.json

@@ -10,4 +10,4 @@ len = 2
     "str": "bar"
   }
 }
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+Processed 1 model, and 1 requirement file and found 1 warning

tests-system/builtin-1/output.smtlib

@@ -1,3 +1,3 @@
 len = 2
       ^ builtin-1/example.trlc:10: check warning: potato
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+Processed 1 model, and 1 requirement file and found 1 warning

tests-system/builtin-2/output

@@ -1,3 +1,3 @@
 len == trlc:len(str), warning "potato", len
        ^^^^ builtin-2/legacy.rsl:9: error: unknown symbol trlc
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/builtin-2/output.json

@@ -1,3 +1,3 @@
 len == trlc:len(str), warning "potato", len
        ^^^^ builtin-2/legacy.rsl:9: error: unknown symbol trlc
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/builtin-2/output.smtlib

@@ -1,3 +1,3 @@
 len == trlc:len(str), warning "potato", len
        ^^^^ builtin-2/legacy.rsl:9: error: unknown symbol trlc
-Processed 1 model, 0 checks and 0 requirement files and found 1 error
+Processed 1 model, and 0 requirement files and found 1 error

tests-system/check-wo-type/bar.rsl

@@ -11,3 +11,7 @@ type MyType {
    status  Status
 
  }
+  checks {
+      status == bar.Status.NEW , error "Status must be NEW"
+  }
+

tests-system/check-wo-type/output

@@ -1,3 +1,3 @@
 checks {
-       ^ check-wo-type/checks.check:3: error: expected identifier, encountered opening brace '{' instead
-Processed 1 model, 1 check and 1 requirement file and found 1 error
+       ^ check-wo-type/bar.rsl:14: error: expected identifier, encountered opening brace '{' instead
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/check-wo-type/output.brief

@@ -1 +1 @@
-check-wo-type/checks.check:3:9: trlc error: expected identifier, encountered opening brace '{' instead
+check-wo-type/bar.rsl:14:10: trlc error: expected identifier, encountered opening brace '{' instead

tests-system/check-wo-type/output.json

@@ -1,3 +1,3 @@
 checks {
-       ^ check-wo-type/checks.check:3: error: expected identifier, encountered opening brace '{' instead
-Processed 1 model, 1 check and 1 requirement file and found 1 error
+       ^ check-wo-type/bar.rsl:14: error: expected identifier, encountered opening brace '{' instead
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/check-wo-type/output.smtlib

@@ -1,3 +1,3 @@
 checks {
-       ^ check-wo-type/checks.check:3: error: expected identifier, encountered opening brace '{' instead
-Processed 1 model, 1 check and 1 requirement file and found 1 error
+       ^ check-wo-type/bar.rsl:14: error: expected identifier, encountered opening brace '{' instead
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/checks-1/foo.rsl

@@ -4,3 +4,7 @@ type T {
    a          Integer
    b optional Integer
 }
+checks T {
+   a < b, "a must be less than b"
+}
+

tests-system/checks-1/output

@@ -1,14 +1,12 @@
-checks T {
-       ^ checks-1/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
 a < b, "a must be less than b"
-    ^ checks-1/foo.check:4: issue: expression could be null [vcg-evaluation-of-null]
+    ^ checks-1/foo.rsl:8: issue: expression could be null [vcg-evaluation-of-null]
     | example record_type triggering error:
     |   T bad_potato {
     |     a = 0
     |     /* b is null */
     |   }
 T Test_1 {
-  ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.check:4) must not be null
+  ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.rsl:8) must not be null
 T Test_2 {
   ^^^^^^ checks-1/foo.trlc:7: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 2 warnings and 2 errors
+Processed 1 model, and 1 requirement file and found 1 warning and 2 errors

tests-system/checks-1/output.brief

@@ -1,2 +1,2 @@
-checks-1/foo.trlc:3:3: trlc error: rhs of check a < b (foo.check:4) must not be null
+checks-1/foo.trlc:3:3: trlc error: rhs of check a < b (foo.rsl:8) must not be null
 checks-1/foo.trlc:7:3: trlc check error: a must be less than b

tests-system/checks-1/output.json

@@ -1,5 +1,5 @@
 T Test_1 {
-  ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.check:4) must not be null
+  ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.rsl:8) must not be null
 T Test_2 {
   ^^^^^^ checks-1/foo.trlc:7: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 2 errors
+Processed 1 model, and 1 requirement file and found 2 errors

tests-system/checks-1/output.smtlib

@@ -1,14 +1,12 @@
-checks T {
-       ^ checks-1/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
 a < b, "a must be less than b"
-    ^ checks-1/foo.check:4: issue: expression could be null [vcg-evaluation-of-null]
+    ^ checks-1/foo.rsl:8: issue: expression could be null [vcg-evaluation-of-null]
     | example record_type triggering error:
     |   T bad_potato {
     |     a = 0
     |     /* b is null */
     |   }
 T Test_1 {
-  ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.check:4) must not be null
+  ^^^^^^ checks-1/foo.trlc:3: error: rhs of check a < b (foo.rsl:8) must not be null
 T Test_2 {
   ^^^^^^ checks-1/foo.trlc:7: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 2 warnings and 2 errors
+Processed 1 model, and 1 requirement file and found 1 warning and 2 errors

tests-system/checks-2/foo.rsl

@@ -4,3 +4,8 @@ type T {
    a          Integer
    b optional Integer
 }
+
+checks T {
+   b != null, fatal "please define b", b
+   a < b, "a must be less than b", a
+}

tests-system/checks-2/output

@@ -1,7 +1,5 @@
-checks T {
-       ^ checks-2/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
 T Test_1 {
   ^^^^^^ checks-2/foo.trlc:3: check error: please define b
 a = 5
     ^ checks-2/foo.trlc:8: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 1 warning and 2 errors
+Processed 1 model, and 1 requirement file and found 2 errors

tests-system/checks-2/output.json

@@ -2,4 +2,4 @@ T Test_1 {
   ^^^^^^ checks-2/foo.trlc:3: check error: please define b
 a = 5
     ^ checks-2/foo.trlc:8: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 2 errors
+Processed 1 model, and 1 requirement file and found 2 errors

tests-system/checks-2/output.smtlib

@@ -1,7 +1,5 @@
-checks T {
-       ^ checks-2/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
 T Test_1 {
   ^^^^^^ checks-2/foo.trlc:3: check error: please define b
 a = 5
     ^ checks-2/foo.trlc:8: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 1 warning and 2 errors
+Processed 1 model, and 1 requirement file and found 2 errors

tests-system/checks-3/foo.rsl

@@ -4,3 +4,7 @@ type T {
    a          Integer
    b optional Integer
 }
+
+checks T {
+   b != null implies a < b, "a must be less than b", a
+}

tests-system/checks-3/output

@@ -1,5 +1,3 @@
-checks T {
-       ^ checks-3/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
 a = 5
     ^ checks-3/foo.trlc:8: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 1 warning and 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/checks-3/output.json

@@ -1,3 +1,3 @@
 a = 5
     ^ checks-3/foo.trlc:8: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/checks-3/output.smtlib

@@ -1,5 +1,3 @@
-checks T {
-       ^ checks-3/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
 a = 5
     ^ checks-3/foo.trlc:8: check error: a must be less than b
-Processed 1 model, 1 check and 1 requirement file and found 1 warning and 1 error
+Processed 1 model, and 1 requirement file and found 1 error

tests-system/checks-4/foo.rsl

@@ -4,3 +4,6 @@ type T {
    foo optional String
    values optional String [2 .. 5]
 }
+checks T {
+   (forall v in values => v != foo), "value cannot be same as value of foo", values
+}

tests-system/checks-4/output

@@ -1,14 +1,12 @@
-checks T {
-       ^ checks-4/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature]
 (forall v in values => v != foo), "value cannot be same as value of foo", values
-             ^^^^^^ checks-4/foo.check:4: issue: expression could be null [vcg-evaluation-of-null]
+             ^^^^^^ checks-4/foo.rsl:8: issue: expression could be null [vcg-evaluation-of-null]
                   | example record_type triggering error:
                   |   T bad_potato {
                   |     /* foo is null */
                   |     /* values is null */
                   |   }
 T Test_1 {
-  ^^^^^^ checks-4/foo.trlc:3: error: values in quantified expression (forall v in values => v != foo) (foo.check:4) must not be null
+  ^^^^^^ checks-4/foo.trlc:3: error: values in quantified expression (forall v in values => v != foo) (foo.rsl:8) must not be null
 values = ["x", "kitten", "z"]
          ^ checks-4/foo.trlc:9: check error: value cannot be same as value of foo
-Processed 1 model, 1 check and 1 requirement file and found 2 warnings and 2 errors
+Processed 1 model, and 1 requirement file and found 1 warning and 2 errors