diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index c9c13f34..fd06e317 100644 --- a/language-reference-manual/lrm.trlc +++ b/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' ''' diff --git a/tests-system/rbt-existential-quantification-semantics/output b/tests-system/rbt-existential-quantification-semantics/output index f835303c..26da7f58 100644 --- a/tests-system/rbt-existential-quantification-semantics/output +++ b/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 diff --git a/tests-system/rbt-existential-quantification-semantics/output.json b/tests-system/rbt-existential-quantification-semantics/output.json index 372f1cca..fa198fd1 100644 --- a/tests-system/rbt-existential-quantification-semantics/output.json +++ b/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 diff --git a/tests-system/rbt-existential-quantification-semantics/output.smtlib b/tests-system/rbt-existential-quantification-semantics/output.smtlib index f835303c..26da7f58 100644 --- a/tests-system/rbt-existential-quantification-semantics/output.smtlib +++ b/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 diff --git a/tests-system/rbt-quantification-naming-scope/output b/tests-system/rbt-quantification-naming-scope/output index 1e81b216..2e42ad4d 100644 --- a/tests-system/rbt-quantification-naming-scope/output +++ b/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 diff --git a/tests-system/rbt-quantification-naming-scope/output.json b/tests-system/rbt-quantification-naming-scope/output.json index 1e81b216..2e42ad4d 100644 --- a/tests-system/rbt-quantification-naming-scope/output.json +++ b/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 diff --git a/tests-system/rbt-quantification-naming-scope/output.smtlib b/tests-system/rbt-quantification-naming-scope/output.smtlib index 1e81b216..2e42ad4d 100644 --- a/tests-system/rbt-quantification-naming-scope/output.smtlib +++ b/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 diff --git a/tests-system/rbt-quantification-object/foo.rsl b/tests-system/rbt-quantification-object-1/foo.rsl similarity index 100% rename from tests-system/rbt-quantification-object/foo.rsl rename to tests-system/rbt-quantification-object-1/foo.rsl diff --git a/tests-system/rbt-quantification-object-1/output b/tests-system/rbt-quantification-object-1/output new file mode 100644 index 00000000..f1014cb8 --- /dev/null +++ b/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 diff --git a/tests-system/rbt-quantification-object-1/output.brief b/tests-system/rbt-quantification-object-1/output.brief new file mode 100644 index 00000000..979f63e3 --- /dev/null +++ b/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 diff --git a/tests-system/rbt-quantification-object-1/output.json b/tests-system/rbt-quantification-object-1/output.json new file mode 100644 index 00000000..f1014cb8 --- /dev/null +++ b/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 diff --git a/tests-system/rbt-quantification-object-1/output.smtlib b/tests-system/rbt-quantification-object-1/output.smtlib new file mode 100644 index 00000000..f1014cb8 --- /dev/null +++ b/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 diff --git a/tests-system/rbt-quantification-object-2/foo.rsl b/tests-system/rbt-quantification-object-2/foo.rsl new file mode 100644 index 00000000..81ab03ec --- /dev/null +++ b/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" +} diff --git a/tests-system/rbt-quantification-object-2/output b/tests-system/rbt-quantification-object-2/output new file mode 100644 index 00000000..c9019dd7 --- /dev/null +++ b/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 diff --git a/tests-system/rbt-quantification-object-2/output.brief b/tests-system/rbt-quantification-object-2/output.brief new file mode 100644 index 00000000..5688779f --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output.brief @@ -0,0 +1 @@ +rbt-quantification-object-2/foo.rsl:8:21: trlc error: unknown symbol b diff --git a/tests-system/rbt-quantification-object-2/output.json b/tests-system/rbt-quantification-object-2/output.json new file mode 100644 index 00000000..c9019dd7 --- /dev/null +++ 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 diff --git a/tests-system/rbt-quantification-object-2/output.smtlib b/tests-system/rbt-quantification-object-2/output.smtlib new file mode 100644 index 00000000..c9019dd7 --- /dev/null +++ b/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 diff --git a/tests-system/rbt-quantification-object/output b/tests-system/rbt-quantification-object/output deleted file mode 100644 index e9276c4e..00000000 --- a/tests-system/rbt-quantification-object/output +++ /dev/null @@ -1,3 +0,0 @@ -(forall char in a => char != "a"), warning "a should not contain the letter a" - ^ rbt-quantification-object/foo.rsl:8: error: you can only quantify over arrays -Processed 1 model, 0 checks and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object/output.brief b/tests-system/rbt-quantification-object/output.brief deleted file mode 100644 index 49d16fe2..00000000 --- a/tests-system/rbt-quantification-object/output.brief +++ /dev/null @@ -1 +0,0 @@ -rbt-quantification-object/foo.rsl:8:21: trlc error: you can only quantify over arrays diff --git a/tests-system/rbt-quantification-object/output.json b/tests-system/rbt-quantification-object/output.json deleted file mode 100644 index e9276c4e..00000000 --- a/tests-system/rbt-quantification-object/output.json +++ /dev/null @@ -1,3 +0,0 @@ -(forall char in a => char != "a"), warning "a should not contain the letter a" - ^ rbt-quantification-object/foo.rsl:8: error: you can only quantify over arrays -Processed 1 model, 0 checks and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object/output.smtlib b/tests-system/rbt-quantification-object/output.smtlib deleted file mode 100644 index e9276c4e..00000000 --- a/tests-system/rbt-quantification-object/output.smtlib +++ /dev/null @@ -1,3 +0,0 @@ -(forall char in a => char != "a"), warning "a should not contain the letter a" - ^ rbt-quantification-object/foo.rsl:8: error: you can only quantify over arrays -Processed 1 model, 0 checks and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantified-expression/foo.rsl b/tests-system/rbt-quantified-expression/foo.rsl index 0415e77f..d877e168 100644 --- a/tests-system/rbt-quantified-expression/foo.rsl +++ b/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 } diff --git a/tests-system/rbt-quantified-expression/output b/tests-system/rbt-quantified-expression/output index 508ed33b..cd5ef1e1 100644 --- a/tests-system/rbt-quantified-expression/output +++ b/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 diff --git a/tests-system/rbt-quantified-expression/output.brief b/tests-system/rbt-quantified-expression/output.brief index e69de29b..d16c8133 100644 --- a/tests-system/rbt-quantified-expression/output.brief +++ b/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 diff --git a/tests-system/rbt-quantified-expression/output.json b/tests-system/rbt-quantified-expression/output.json index 72754c93..cd5ef1e1 100644 --- a/tests-system/rbt-quantified-expression/output.json +++ b/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 diff --git a/tests-system/rbt-quantified-expression/output.smtlib b/tests-system/rbt-quantified-expression/output.smtlib index 508ed33b..cd5ef1e1 100644 --- a/tests-system/rbt-quantified-expression/output.smtlib +++ b/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 diff --git a/tests-system/rbt-universal-quantification-semantics/foo.trlc b/tests-system/rbt-universal-quantification-semantics/foo.trlc index 03aef2a2..230875da 100644 --- a/tests-system/rbt-universal-quantification-semantics/foo.trlc +++ b/tests-system/rbt-universal-quantification-semantics/foo.trlc @@ -7,3 +7,7 @@ T Bar { T Kitten { a = [] } + +T Potato { + a = [-1, 1] +} diff --git a/tests-system/rbt-universal-quantification-semantics/output b/tests-system/rbt-universal-quantification-semantics/output index 70ee9851..07661ca4 100644 --- a/tests-system/rbt-universal-quantification-semantics/output +++ b/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 diff --git a/tests-system/rbt-universal-quantification-semantics/output.brief b/tests-system/rbt-universal-quantification-semantics/output.brief index b76f0b27..c4f34df9 100644 --- a/tests-system/rbt-universal-quantification-semantics/output.brief +++ b/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 diff --git a/tests-system/rbt-universal-quantification-semantics/output.json b/tests-system/rbt-universal-quantification-semantics/output.json index f5fad742..e25ab77e 100644 --- a/tests-system/rbt-universal-quantification-semantics/output.json +++ b/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 diff --git a/tests-system/rbt-universal-quantification-semantics/output.smtlib b/tests-system/rbt-universal-quantification-semantics/output.smtlib index 70ee9851..07661ca4 100644 --- a/tests-system/rbt-universal-quantification-semantics/output.smtlib +++ b/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