adds tracing for checks (#34)

adds tracing for chapter 10

---------

Co-authored-by: Florian Schanda <[email protected]>

language-reference-manual/lrm.trlc

@@ -886,7 +886,7 @@ section "Checks" {
               order.'''
   }
 
-  Dynamic_Semantics Check_Evaluation_Order_Across_Blocks {
+  Note Check_Evaluation_Order_Across_Blocks {
     text = '''If multiple check blocks are declared for the same type,
               then the order of evaluation of each check
               block is unspecified.'''

tests-system/rbt-applicable-components/foo.rsl

@@ -0,0 +1,10 @@
+package Foo
+
+type T {
+    a String
+    b String
+}
+
+checks T {
+    len(c) > 10, "c is too short", c
+}

tests-system/rbt-applicable-components/output

@@ -0,0 +1,3 @@
+len(c) > 10, "c is too short", c
+    ^ rbt-applicable-components/foo.rsl:9: error: unknown symbol c
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-applicable-components/output.brief

@@ -0,0 +1 @@
+rbt-applicable-components/foo.rsl:9:9: trlc error: unknown symbol c

tests-system/rbt-applicable-components/output.json

@@ -0,0 +1,3 @@
+len(c) > 10, "c is too short", c
+    ^ rbt-applicable-components/foo.rsl:9: error: unknown symbol c
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-applicable-components/output.smtlib

@@ -0,0 +1,3 @@
+len(c) > 10, "c is too short", c
+    ^ rbt-applicable-components/foo.rsl:9: error: unknown symbol c
+Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-applicable-types/bar.rsl

@@ -0,0 +1,5 @@
+package Bar
+
+type B {
+    a String
+}

tests-system/rbt-applicable-types/foo.rsl

@@ -0,0 +1,10 @@
+package Foo
+import Bar
+
+type T {
+    a String
+}
+
+checks B {
+    len(a) > 10, "a is too short", a
+}

tests-system/rbt-applicable-types/output

@@ -0,0 +1,3 @@
+checks B {
+       ^ rbt-applicable-types/foo.rsl:8: error: unknown symbol B
+Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-applicable-types/output.brief

@@ -0,0 +1 @@
+rbt-applicable-types/foo.rsl:8:8: trlc error: unknown symbol B

tests-system/rbt-applicable-types/output.json

@@ -0,0 +1,3 @@
+checks B {
+       ^ rbt-applicable-types/foo.rsl:8: error: unknown symbol B
+Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-applicable-types/output.smtlib

@@ -0,0 +1,3 @@
+checks B {
+       ^ rbt-applicable-types/foo.rsl:8: error: unknown symbol B
+Processed 2 model(s), 0 check(s) and 0 requirement file(s) and found 1 error(s)

tests-system/rbt-check-evaluation-order-for-extensions/bar.rsl

@@ -0,0 +1,11 @@
+package Bar
+import Foo
+
+type T extends Foo.T {
+    b String
+}
+
+checks T {
+    len(a) > 10, "a has to be more than 10 chars", a
+    len(b) > 10, "b has to be more than 10 chars", b
+}

tests-system/rbt-check-evaluation-order-for-extensions/bar.trlc

@@ -0,0 +1,6 @@
+package Bar
+
+T Test {
+    a = "potato"
+    b = "more potatoes"
+}

tests-system/rbt-check-evaluation-order-for-extensions/foo.rsl

@@ -0,0 +1,9 @@
+package Foo
+
+type T {
+    a String
+}
+
+checks T {
+    len(a) > 10, warning "a has to be more than 7 chars", a
+}

tests-system/rbt-check-evaluation-order-for-extensions/output

@@ -0,0 +1,5 @@
+a = "potato"
+    ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check warning: a has to be more than 7 chars
+a = "potato"
+    ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check error: a has to be more than 10 chars
+Processed 2 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/rbt-check-evaluation-order-for-extensions/output.brief

@@ -0,0 +1,2 @@
+rbt-check-evaluation-order-for-extensions/bar.trlc:4:9: trlc check warning: a has to be more than 7 chars
+rbt-check-evaluation-order-for-extensions/bar.trlc:4:9: trlc check error: a has to be more than 10 chars

tests-system/rbt-check-evaluation-order-for-extensions/output.json

@@ -0,0 +1,5 @@
+a = "potato"
+    ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check warning: a has to be more than 7 chars
+a = "potato"
+    ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check error: a has to be more than 10 chars
+Processed 2 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/rbt-check-evaluation-order-for-extensions/output.smtlib

@@ -0,0 +1,5 @@
+a = "potato"
+    ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check warning: a has to be more than 7 chars
+a = "potato"
+    ^^^^^^^^ rbt-check-evaluation-order-for-extensions/bar.trlc:4: check error: a has to be more than 10 chars
+Processed 2 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s)

tests-system/rbt-check-evaluation-order-for-extensions/tracing

@@ -0,0 +1 @@
+LRM.Check_Messages

tests-system/rbt-check-evaluation-order/foo.rsl

@@ -0,0 +1,12 @@
+package Foo
+
+type T {
+    a Integer
+    b Integer
+}
+
+checks T {
+    a < 0, warning "First warning: a is positive", a
+    b > 0, warning "Second warning: b is negative", b
+    a < b, warning "Third warning: a is greater than b"
+}

tests-system/rbt-check-evaluation-order/foo.trlc

@@ -0,0 +1,6 @@
+package Foo
+
+T Bar {
+  a = 1
+  b = -1
+}

tests-system/rbt-check-evaluation-order/output

@@ -0,0 +1,7 @@
+a = 1
+    ^ rbt-check-evaluation-order/foo.trlc:4: check warning: First warning: a is positive
+b = -1
+    ^ rbt-check-evaluation-order/foo.trlc:5: check warning: Second warning: b is negative
+T Bar {
+  ^^^ rbt-check-evaluation-order/foo.trlc:3: check warning: Third warning: a is greater than b
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s)

tests-system/rbt-check-evaluation-order/output.brief

@@ -0,0 +1,3 @@
+rbt-check-evaluation-order/foo.trlc:4:7: trlc check warning: First warning: a is positive
+rbt-check-evaluation-order/foo.trlc:5:7: trlc check warning: Second warning: b is negative
+rbt-check-evaluation-order/foo.trlc:3:3: trlc check warning: Third warning: a is greater than b

tests-system/rbt-check-evaluation-order/output.json

@@ -0,0 +1,13 @@
+a = 1
+    ^ rbt-check-evaluation-order/foo.trlc:4: check warning: First warning: a is positive
+b = -1
+    ^ rbt-check-evaluation-order/foo.trlc:5: check warning: Second warning: b is negative
+T Bar {
+  ^^^ rbt-check-evaluation-order/foo.trlc:3: check warning: Third warning: a is greater than b
+{
+  "Bar": {
+    "a": 1,
+    "b": -1
+  }
+}
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s)

tests-system/rbt-check-evaluation-order/output.smtlib

@@ -0,0 +1,7 @@
+a = 1
+    ^ rbt-check-evaluation-order/foo.trlc:4: check warning: First warning: a is positive
+b = -1
+    ^ rbt-check-evaluation-order/foo.trlc:5: check warning: Second warning: b is negative
+T Bar {
+  ^^^ rbt-check-evaluation-order/foo.trlc:3: check warning: Third warning: a is greater than b
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s)

tests-system/rbt-check-severity-1/foo.rsl

@@ -0,0 +1,13 @@
+package Foo
+
+type T {
+    a String
+    b String
+    c String
+}
+
+checks T {
+    len(a) > 3, error "a must be longer than 3", a
+    len(b) > 7, "b must be longer than 7", b
+    len(c) > 10, "c must be longer than 10", c
+}

tests-system/rbt-check-severity-1/foo.trlc

@@ -0,0 +1,7 @@
+package Foo
+
+T Test {
+    a = "po"
+    b = "potato"
+    c = "potatoes"
+}

tests-system/rbt-check-severity-1/output

@@ -0,0 +1,7 @@
+a = "po"
+    ^^^^ rbt-check-severity-1/foo.trlc:4: check error: a must be longer than 3
+b = "potato"
+    ^^^^^^^^ rbt-check-severity-1/foo.trlc:5: check error: b must be longer than 7
+c = "potatoes"
+    ^^^^^^^^^^ rbt-check-severity-1/foo.trlc:6: check error: c must be longer than 10
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s)

tests-system/rbt-check-severity-1/output.brief

@@ -0,0 +1,3 @@
+rbt-check-severity-1/foo.trlc:4:9: trlc check error: a must be longer than 3
+rbt-check-severity-1/foo.trlc:5:9: trlc check error: b must be longer than 7
+rbt-check-severity-1/foo.trlc:6:9: trlc check error: c must be longer than 10

tests-system/rbt-check-severity-1/output.json

@@ -0,0 +1,7 @@
+a = "po"
+    ^^^^ rbt-check-severity-1/foo.trlc:4: check error: a must be longer than 3
+b = "potato"
+    ^^^^^^^^ rbt-check-severity-1/foo.trlc:5: check error: b must be longer than 7
+c = "potatoes"
+    ^^^^^^^^^^ rbt-check-severity-1/foo.trlc:6: check error: c must be longer than 10
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s)

tests-system/rbt-check-severity-1/output.smtlib

@@ -0,0 +1,7 @@
+a = "po"
+    ^^^^ rbt-check-severity-1/foo.trlc:4: check error: a must be longer than 3
+b = "potato"
+    ^^^^^^^^ rbt-check-severity-1/foo.trlc:5: check error: b must be longer than 7
+c = "potatoes"
+    ^^^^^^^^^^ rbt-check-severity-1/foo.trlc:6: check error: c must be longer than 10
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 error(s)

tests-system/rbt-check-severity-2/foo.rsl

@@ -0,0 +1,13 @@
+package Foo
+
+type T {
+    a String
+    b String
+    c String
+}
+
+checks T {
+    len(a) > 3, fatal "a must be longer than 3", a
+    len(b) > 7, "b must be longer than 7", b
+    len(c) > 10, "c must be longer than 10", c
+}

tests-system/rbt-check-severity-2/foo.trlc

@@ -0,0 +1,7 @@
+package Foo
+
+T Test {
+    a = "po"
+    b = "potato"
+    c = "potatoes"
+}

tests-system/rbt-check-severity-2/output

@@ -0,0 +1,3 @@
+a = "po"
+    ^^^^ rbt-check-severity-2/foo.trlc:4: check error: a must be longer than 3
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/rbt-check-severity-2/output.brief

@@ -0,0 +1 @@
+rbt-check-severity-2/foo.trlc:4:9: trlc check error: a must be longer than 3

tests-system/rbt-check-severity-2/output.json

@@ -0,0 +1,3 @@
+a = "po"
+    ^^^^ rbt-check-severity-2/foo.trlc:4: check error: a must be longer than 3
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/rbt-check-severity-2/output.smtlib

@@ -0,0 +1,3 @@
+a = "po"
+    ^^^^ rbt-check-severity-2/foo.trlc:4: check error: a must be longer than 3
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/rbt-check-severity-3/foo.rsl

@@ -0,0 +1,13 @@
+package Foo
+
+type T {
+    a String
+    b String
+    c String
+}
+
+checks T {
+    len(a) > 3, warning "a must be longer than 3", a
+    len(b) > 7, warning "b must be longer than 7", b
+    len(c) > 10, warning "c must be longer than 10", c
+}

tests-system/rbt-check-severity-3/foo.trlc

@@ -0,0 +1,7 @@
+package Foo
+
+T Test {
+    a = "po"
+    b = "potato"
+    c = "potatoes"
+}

tests-system/rbt-check-severity-3/output

@@ -0,0 +1,7 @@
+a = "po"
+    ^^^^ rbt-check-severity-3/foo.trlc:4: check warning: a must be longer than 3
+b = "potato"
+    ^^^^^^^^ rbt-check-severity-3/foo.trlc:5: check warning: b must be longer than 7
+c = "potatoes"
+    ^^^^^^^^^^ rbt-check-severity-3/foo.trlc:6: check warning: c must be longer than 10
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s)

tests-system/rbt-check-severity-3/output.brief

@@ -0,0 +1,3 @@
+rbt-check-severity-3/foo.trlc:4:9: trlc check warning: a must be longer than 3
+rbt-check-severity-3/foo.trlc:5:9: trlc check warning: b must be longer than 7
+rbt-check-severity-3/foo.trlc:6:9: trlc check warning: c must be longer than 10

tests-system/rbt-check-severity-3/output.json

@@ -0,0 +1,14 @@
+a = "po"
+    ^^^^ rbt-check-severity-3/foo.trlc:4: check warning: a must be longer than 3
+b = "potato"
+    ^^^^^^^^ rbt-check-severity-3/foo.trlc:5: check warning: b must be longer than 7
+c = "potatoes"
+    ^^^^^^^^^^ rbt-check-severity-3/foo.trlc:6: check warning: c must be longer than 10
+{
+  "Test": {
+    "a": "po",
+    "b": "potato",
+    "c": "potatoes"
+  }
+}
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s)

tests-system/rbt-check-severity-3/output.smtlib

@@ -0,0 +1,7 @@
+a = "po"
+    ^^^^ rbt-check-severity-3/foo.trlc:4: check warning: a must be longer than 3
+b = "potato"
+    ^^^^^^^^ rbt-check-severity-3/foo.trlc:5: check warning: b must be longer than 7
+c = "potatoes"
+    ^^^^^^^^^^ rbt-check-severity-3/foo.trlc:6: check warning: c must be longer than 10
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 3 warning(s)

tests-system/simple/foo.rsl

@@ -0,0 +1,9 @@
+package foo
+
+type MyType {
+  name String
+}
+
+checks MyType {
+  len(name) > 10, warning "name is too short", name
+}

tests-system/simple/instances.trlc

@@ -1,6 +1,11 @@
 package instances
 import bar
+import foo
 
 bar.MyType SomeThing {
   name = "Qbert" // does start with Q
 }
+
+foo.MyType OtherThing {
+  name = "long enough"
+}

tests-system/simple/output

@@ -1,3 +1,3 @@
 checks MyType {
        ^^^^^^ simple/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature]
-Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s)
+Processed 2 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s)

tests-system/simple/output.json

@@ -1,6 +1,9 @@
 {
+  "OtherThing": {
+    "name": "long enough"
+  },
   "SomeThing": {
     "name": "Qbert"
   }
 }
-Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found no issues
+Processed 2 model(s), 1 check(s) and 1 requirement file(s) and found no issues

tests-system/simple/output.smtlib

@@ -1,3 +1,3 @@
 checks MyType {
        ^^^^^^ simple/checks.check:3: issue: move this check block into bar.rsl:1 [deprecated_feature]
-Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s)
+Processed 2 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s)

tests-system/simple/tracing

@@ -4,3 +4,4 @@ LRM.Preamble
 LRM.RSL_File
 LRM.Check_File
 LRM.Deprecated_Check_Files
+LRM.Check_Block