Support access to type instance

documentation/TUTORIAL-ADVANCED-TYPES.md

@@ -52,3 +52,40 @@ type ACME_Requirement extends Supplier_Requirement {
 This makes sure that any and all supplier requirements are completely
 uniform, and nobody adds new fields that may be confusing or
 unexpected to the suppliers.
+
+### Type Checks
+
+A field within a type can also reference another type. 
+You can access fields of a referenced type using the `.` notation:
+
+```
+type BaseType {
+   name  String
+}
+
+type MyType {
+   name  String
+   link  BaseType
+}
+
+checks MyType {
+   link.name != name, "cannot link the type with the same name."
+}
+```
+
+Self-referencing (recursive) type definitions are also supported.
+To prevent infinite recursion, any recursive field must be declared as `optional`:
+
+```
+type MyType {
+   name String
+   link optional MyType
+}
+
+checks MyType {
+   link != null implies link.name != name, 
+      "link status must be the same as status"
+}
+```
+Excessive recursion may lead to performance degradation,
+so complex recursive designs are not recommended.

language-reference-manual/lrm.trlc

@@ -1084,8 +1084,13 @@ section "Names" {
               a valid literal of that type. If the prefix of
               a dot (`.`) access resolves to a tuple, then
               the identifier must be a valid field of the
-              type of that tuple. Any other prefix is an
-              error.
+              type of that tuple. If the prefix of a dot (`.`)
+              access resolves to a record object, then the identifier
+              must be the name of a component declared inside
+              that record. Optional components are represented as a
+              pair `(valid, value)`, and may be accessed using
+              `record.field.valid` and `record.field.value`. Nested
+              field access is allowed. Any other prefix is an error.
            '''
   }
 
@@ -1101,7 +1106,6 @@ section "Names" {
            '''
   }
 
-
   Static_Semantics Signature_Len {
     text = '''The builtin function `len` is of arity 1. Its parameter must
               be of type `String` or an array type. Its
@@ -1197,14 +1201,16 @@ section "Names" {
         separator @
         version optional Integer
       }
+      type Name_Base {
+        description string
+      }
       type Name_Examples {
-         foo Boolean
-         bar Name_Examples
-         asil ASIL
-         potato Integer [0 .. *]
-         wibble Decimal
-         field String
-         cb_link Codebeamer_Item
+        foo Boolean
+        bar Name_Base
+        asil ASIL
+        potato Integer [0 .. *]
+        field String
+        cb_link Codebeamer_Item
       }
     '''
     rsl = '''
@@ -1223,6 +1229,9 @@ section "Names" {
 
         cb_link.item >= 50000, warning "cb item value is oddly low"
         // you can obtain a tuple's values
+
+        bar.description, "foo"
+        // you can obtain a record's component
       }
     '''
   }

requirements.txt

@@ -1,2 +1,2 @@
-pyvcg==1.0.8
+pyvcg==1.0.9
 cvc5>=1.2.0

setup.py

@@ -42,7 +42,7 @@
     project_urls=project_urls,
     license="GNU General Public License v3",
     packages=setuptools.find_packages(),
-    install_requires="PyVCG[api]==1.0.8",
+    install_requires="PyVCG[api]==1.0.9",
     python_requires=">=3.8, <3.14",
     classifiers=[
         "Development Status :: 5 - Production/Stable",

tests-system/Makefile

@@ -1,4 +1,4 @@
-RAW_TARGETS=$(filter-out bulk, $(subst ./,,$(shell find . -mindepth 1 -maxdepth 1 -type d)))
+RAW_TARGETS=$(if $(TARGET),$(TARGET),$(filter-out bulk, $(subst ./,,$(shell find . -mindepth 1 -maxdepth 1 -type d))))
 
 TARGETS=\
 	$(addsuffix /output, $(RAW_TARGETS)) \

tests-system/checks-5/output

@@ -1,6 +1,3 @@
-Requirement Potato {
-            ^^^^^^ checks-5/foo.trlc:3: check error: linkage incorrect
-                 | You must either link this requirement to other requirements
-                 | using the derived_from attribute, or you need to set
-                 | top_level to true.
+type Requirement {
+     ^^^^^^^^^^^ checks-5/foo.rsl:3: error: Complex recursive is not supported.
 Processed 1 model and 1 requirement file and found 1 error

tests-system/checks-5/output.smtlib

@@ -1,6 +1,3 @@
-Requirement Potato {
-            ^^^^^^ checks-5/foo.trlc:3: check error: linkage incorrect
-                 | You must either link this requirement to other requirements
-                 | using the derived_from attribute, or you need to set
-                 | top_level to true.
+type Requirement {
+     ^^^^^^^^^^^ checks-5/foo.rsl:3: error: Complex recursive is not supported.
 Processed 1 model and 1 requirement file and found 1 error

tests-system/lint-record-refs/output

@@ -10,32 +10,32 @@ a != b implies x, "potato"
                ^ lint-record-refs/test2.rsl:10: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = T_instance_1
-               |     b = T_instance_0
+               |     a = None
+               |     b = None
                |     /* x is null */
                |   }
 a == b implies x, "potato"
                ^ lint-record-refs/test2.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = T_instance_0
-               |     b = T_instance_0
+               |     a = None
+               |     b = None
                |     /* x is null */
                |   }
 a != b implies x, "potato"
                ^ lint-record-refs/test3.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = Other.T_instance_1
-               |     b = Other.T_instance_0
+               |     a = ("")
+               |     b = ("A")
                |     /* x is null */
                |   }
 a == b implies x, "potato"
                ^ lint-record-refs/test3.rsl:12: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = Other.T_instance_0
-               |     b = Other.T_instance_0
+               |     a = ("")
+               |     b = ("")
                |     /* x is null */
                |   }
 Processed 4 models and 0 requirement files and found 5 warnings

tests-system/lint-record-refs/output.smtlib

@@ -10,32 +10,32 @@ a != b implies x, "potato"
                ^ lint-record-refs/test2.rsl:10: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = T_instance_1
-               |     b = T_instance_0
+               |     a = None
+               |     b = None
                |     /* x is null */
                |   }
 a == b implies x, "potato"
                ^ lint-record-refs/test2.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = T_instance_0
-               |     b = T_instance_0
+               |     a = None
+               |     b = None
                |     /* x is null */
                |   }
 a != b implies x, "potato"
                ^ lint-record-refs/test3.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = Other.T_instance_1
-               |     b = Other.T_instance_0
+               |     a = ("")
+               |     b = ("A")
                |     /* x is null */
                |   }
 a == b implies x, "potato"
                ^ lint-record-refs/test3.rsl:12: issue: expression could be null [vcg-evaluation-of-null]
                | example record_type triggering error:
                |   T bad_potato {
-               |     a = Other.T_instance_0
-               |     b = Other.T_instance_0
+               |     a = ("")
+               |     b = ("")
                |     /* x is null */
                |   }
 Processed 4 models and 0 requirement files and found 5 warnings

tests-system/tuples-4/output

@@ -2,7 +2,7 @@ f2 >= 0, warning "potato2", f2
 ^^ tuples-4/foo.rsl:12: issue: expression could be null [vcg-evaluation-of-null]
  | example tuple_type triggering error:
  |   T bad_potato {
- |     f1 = R1_instance_0
+ |     f1 = None
  |     /* f2 is null */
  |   }
 t = potato

tests-system/tuples-4/output.smtlib

@@ -2,7 +2,7 @@ f2 >= 0, warning "potato2", f2
 ^^ tuples-4/foo.rsl:12: issue: expression could be null [vcg-evaluation-of-null]
  | example tuple_type triggering error:
  |   T bad_potato {
- |     f1 = R1_instance_0
+ |     f1 = None
  |     /* f2 is null */
  |   }
 t = potato

tests-system/tuples-use-type/bar.rsl

@@ -0,0 +1,29 @@
+package bar
+
+enum Status {
+  NEW
+  OLD
+  DEPRECATED
+}
+
+type BaseType {
+  name String
+  status  Status
+}
+
+tuple LinkMy2Base {
+  link_type BaseType
+  separator @
+  version Integer
+}
+
+type MyType {
+  name String
+  status  Status
+  derived_from optional LinkMy2Base[0 .. *]
+}
+
+checks MyType {
+  derived_from != null implies (forall elem in derived_from => elem.link_type.status == status), 
+    error "link status must be the same as status"
+}

tests-system/tuples-use-type/instances.trlc

@@ -0,0 +1,14 @@
+package instances
+
+import bar
+
+bar.BaseType DeprecatedR {
+  name = "base" // does start with Q
+  status = bar.Status.NEW
+}
+
+bar.MyType NewXR {
+  name = "new"
+  status = bar.Status.NEW
+  derived_from = [ DeprecatedR@1 ]
+}

tests-system/tuples-use-type/output

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

tests-system/tuples-use-type/output.brief

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

tests-system/tuples-use-type/output.json

@@ -0,0 +1,17 @@
+{
+  "DeprecatedR": {
+    "name": "base",
+    "status": "NEW"
+  },
+  "NewXR": {
+    "derived_from": [
+      {
+        "link_type": "instances.DeprecatedR",
+        "version": 1
+      }
+    ],
+    "name": "new",
+    "status": "NEW"
+  }
+}
+Processed 1 model and 1 requirement file and found no issues

tests-system/tuples-use-type/output.smtlib

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

tests-system/xref-expressions/f1.trlc

@@ -7,4 +7,4 @@ A.L L1 {
 
 A.L Localref {
 	l = L1
-}
+}

tests-system/xref-no-recursion/bar.rsl

@@ -0,0 +1,22 @@
+package bar
+
+enum Status {
+  NEW
+  OLD
+  DEPRECATED
+}
+
+type BaseType {
+  name String
+  status  Status
+}
+
+type MyType {
+  name String
+  status  Status
+  link optional BaseType
+}
+
+checks MyType {
+  link != null implies link.status == status, "link status must be the same as status"
+}