rebase main and review comments

language-reference-manual/lrm.trlc

@@ -1520,7 +1520,7 @@ section "Quantification" {
     bnf = '''
       quantified_expression ::=
         '(' quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>'
-        expression_PREDICATE ')'ma
+        expression_PREDICATE ')'
 
       quantifier ::= 'forall' | 'exists'
     '''

tests-system/rbt-existential-quantification-semantics/output

@@ -1,5 +1,3 @@
-(exists item in a => item == 7), warning "there is no 7 in a"
- ^^^^^^ rbt-existential-quantification-semantics/foo.rsl:8: issue: expression is always true [vcg-always-true]
 T Kitten {
   ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a
-Processed 1 model, 0 checks and 1 requirement file and found 2 warnings
+Processed 1 model and 1 requirement file and found 1 warning

tests-system/rbt-existential-quantification-semantics/output.json

@@ -10,4 +10,4 @@ T Kitten {
     "a": []
   }
 }
-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/rbt-existential-quantification-semantics/output.smtlib

@@ -1,5 +1,3 @@
-(exists item in a => item == 7), warning "there is no 7 in a"
- ^^^^^^ rbt-existential-quantification-semantics/foo.rsl:8: issue: expression is always true [vcg-always-true]
 T Kitten {
   ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a
-Processed 1 model, 0 checks and 1 requirement file and found 2 warnings
+Processed 1 model and 1 requirement file and found 1 warning

tests-system/rbt-quantification-naming-scope/output

@@ -1,3 +1,3 @@
 (forall a in a => a != 7), warning "No sevens allowed"
         ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4
-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/rbt-quantification-naming-scope/output.json

@@ -1,3 +1,3 @@
 (forall a in a => a != 7), warning "No sevens allowed"
         ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4
-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/rbt-quantification-naming-scope/output.smtlib

@@ -1,3 +1,3 @@
 (forall a in a => a != 7), warning "No sevens allowed"
         ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4
-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/rbt-quantification-object-1/output

@@ -0,0 +1,3 @@
+(forall char in a => char != "a"), warning "a should not contain the letter a"
+                ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-1/output.brief

@@ -0,0 +1 @@
+rbt-quantification-object-1/foo.rsl:8:21: trlc error: you can only quantify over arrays

tests-system/rbt-quantification-object-1/output.json

@@ -0,0 +1,3 @@
+(forall char in a => char != "a"), warning "a should not contain the letter a"
+                ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-1/output.smtlib

@@ -0,0 +1,3 @@
+(forall char in a => char != "a"), warning "a should not contain the letter a"
+                ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-2/foo.rsl

@@ -0,0 +1,9 @@
+package Foo
+
+type Potato {
+    a String
+}
+
+checks Potato {
+    (forall char in b => char != "a"), warning "b should not contain the letter a"
+}

tests-system/rbt-quantification-object-2/output

@@ -0,0 +1,3 @@
+(forall char in b => char != "a"), warning "b should not contain the letter a"
+                ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-2/output.brief

@@ -0,0 +1 @@
+rbt-quantification-object-2/foo.rsl:8:21: trlc error: unknown symbol b

tests-system/rbt-quantification-object-2/output.json

@@ -0,0 +1,3 @@
+(forall char in b => char != "a"), warning "b should not contain the letter a"
+                ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-2/output.smtlib

@@ -0,0 +1,3 @@
+(forall char in b => char != "a"), warning "b should not contain the letter a"
+                ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantified-expression/foo.rsl

@@ -7,4 +7,5 @@ type T {
 checks T {
     (forall item in a => item > 0), warning "All items must be positive", a
     (exists item in a => item == 7), warning "7 is a lucky number", a
+    (forall item in a => 42), warning "All items must be positive", a
 }

tests-system/rbt-quantified-expression/output

@@ -1,3 +1,3 @@
-(exists item in a => item == 7), warning "7 is a lucky number", a
- ^^^^^^ rbt-quantified-expression/foo.rsl:9: issue: expression is always true [vcg-always-true]
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+(forall item in a => 42), warning "All items must be positive", a
+                     ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-quantified-expression/output.brief

@@ -0,0 +1 @@
+rbt-quantified-expression/foo.rsl:10:26: trlc error: expected expression of type Builtin_Boolean, got Builtin_Integer instead

tests-system/rbt-quantified-expression/output.json

@@ -1,11 +1,3 @@
-{
-  "Bar": {
-    "a": [
-      1,
-      2,
-      3,
-      7
-    ]
-  }
-}
-Processed 1 model, 0 checks and 1 requirement file and found no issues
+(forall item in a => 42), warning "All items must be positive", a
+                     ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-quantified-expression/output.smtlib

@@ -1,3 +1,3 @@
-(exists item in a => item == 7), warning "7 is a lucky number", a
- ^^^^^^ rbt-quantified-expression/foo.rsl:9: issue: expression is always true [vcg-always-true]
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+(forall item in a => 42), warning "All items must be positive", a
+                     ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-universal-quantification-semantics/foo.trlc

@@ -7,3 +7,7 @@ T Bar {
 T Kitten {
     a = []
 }
+
+T Potato {
+    a = [-1, 1]
+}

tests-system/rbt-universal-quantification-semantics/output

@@ -1,3 +1,5 @@
 T Bar {
   ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+T Potato {
+  ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive
+Processed 1 model and 1 requirement file and found 2 warnings

tests-system/rbt-universal-quantification-semantics/output.brief

@@ -1 +1,2 @@
 rbt-universal-quantification-semantics/foo.trlc:3:3: trlc check warning: All items must be positive
+rbt-universal-quantification-semantics/foo.trlc:11:3: trlc check warning: All items must be positive

tests-system/rbt-universal-quantification-semantics/output.json

@@ -1,5 +1,7 @@
 T Bar {
   ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive
+T Potato {
+  ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive
 {
   "Bar": {
     "a": [
@@ -8,6 +10,12 @@ T Bar {
   },
   "Kitten": {
     "a": []
+  },
+  "Potato": {
+    "a": [
+      -1,
+      1
+    ]
   }
 }
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+Processed 1 model and 1 requirement file and found 2 warnings

tests-system/rbt-universal-quantification-semantics/output.smtlib

@@ -1,3 +1,5 @@
 T Bar {
   ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive
-Processed 1 model, 0 checks and 1 requirement file and found 1 warning
+T Potato {
+  ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive
+Processed 1 model and 1 requirement file and found 2 warnings