Here, in order to group calls to multiple clients that correspond to the same proof, along with bug_report, an additional optional argument bug_report_id is passed. If the argument is missing, a default value is calculated from the object id.
This means the class that produces bug report content is responsible for defining where to write data within the tar file. A more flexible design would be to let the caller define bug report structure by abstracting the target directory for the producer using a handle:
# BugReport defines which file to write
bug_report = BugReport('bug-report')
# BugReporter is a handle for writing in a certain directory within the file
bug_reporter = bug_report.reporter('AssertTest.test_assert_true')
# The handle is passed to the class that produces bug report content
client = JsonRpcClient(..., bug_reporter=bug_reporter)
Then the producer is no longer concerned about where to write things:
class JsonRpcClient(...):
def request(self, ...):
# The producer can use the handle to create artifacts
self.bug_reporter.add_command(...)
The private interface between BugReport and BugReporter should implement locking to prevent race conditions.
Related: https://github.com/runtimeverification/pyk/pull/693#discussion_r1366651514
Consider https://github.com/runtimeverification/pyk/blob/41706ef5081585a4c71f7fccb4dea2d7a3796421/src/pyk/kore/rpc.py#L250
Here, in order to group calls to multiple clients that correspond to the same proof, along with
bug_report
, an additional optional argumentbug_report_id
is passed. If the argument is missing, a default value is calculated from the objectid
.This means the class that produces bug report content is responsible for defining where to write data within the
tar
file. A more flexible design would be to let the caller define bug report structure by abstracting the target directory for the producer using a handle:Then the producer is no longer concerned about where to write things:
The private interface between
BugReport
andBugReporter
should implement locking to prevent race conditions.