Extend bazel rule for trlc

  - the stakeholder requirements could be listed as dependency
  - add trlc_specification_test

Author: Melody Ma

trlc.bzl

@@ -18,21 +18,42 @@ _trlc_specification = rule(
 def trlc_specification(**kwargs):
     _trlc_specification(**kwargs)
 
+def trlc_specification_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc.py", **kwargs):
+    native.py_test(
+        name = name,
+        srcs = srcs,
+        args = ["--use-cvc5-binary $(location @trlc//:cvc5)", "--verify", "--skip-trlc-files"],
+        main = main,
+        deps = ["@trlc//trlc:trlc"],
+        data = ["@trlc//:cvc5"] + reqs,
+    )
+
 def _trlc_requirement_impl(ctx):
-    depending_files = []
-    for spec in ctx.attr.spec:
-        depending_files.append(spec[DefaultInfo].files)
+    transitive_spec = []
+    transitive_reqs = []
+    for dep in ctx.attr.deps:
+        trlc_provider = dep[TrlcProviderInfo]
+        transitive_spec.append(trlc_provider.spec)
+        transitive_reqs.append(trlc_provider.reqs)
+
+    own_specs = ctx.files.spec if hasattr(ctx.files, "spec") else []
 
     return [
-        DefaultInfo(files = depset(ctx.files.srcs, transitive = depending_files)),
-        TrlcProviderInfo(spec = depset([], transitive = depending_files), reqs = depset(ctx.files.srcs)),
+        DefaultInfo(
+            files = depset(ctx.files.srcs, transitive = transitive_reqs + transitive_spec + [depset(own_specs)])
+        ),
+        TrlcProviderInfo(
+            spec = depset(own_specs, transitive = transitive_spec),
+            reqs = depset(ctx.files.srcs, transitive = transitive_reqs),
+        ),
     ]
 
 _trlc_requirement = rule(
     implementation = _trlc_requirement_impl,
     attrs = {
         "srcs": attr.label_list(allow_files = [".trlc"]),
-        "spec": attr.label_list(allow_empty = False, providers = [DefaultInfo]),
+        "deps": attr.label_list(allow_files = False, allow_empty = True, providers = [TrlcProviderInfo]),
+        "spec": attr.label_list(allow_empty = True, providers = [DefaultInfo]),
     },
 )