Add JSON support for VerificationResults#93
Add JSON support for VerificationResults#93TrisCC wants to merge 3 commits intoADA-research:mainfrom
Conversation
| res_d = result.unwrap_err() | ||
| success = "ERR" | ||
|
|
||
| inst_d = { |
There was a problem hiding this comment.
I think these abbrevations like inst_d and vdr are not so readable. I would rather put the full names for readability
| class VerificationDataResult: | ||
| """_summary_.""" | ||
|
|
||
| # TODO: Convert files to path objects |
There was a problem hiding this comment.
I would not put todos in the code. I would rather create an issue from this
| "success": self.success, | ||
| "result": self.result, | ||
| "took": str(self.took), | ||
| # "counter_example": self.counter_example or "", |
There was a problem hiding this comment.
I would not publish commented code
| "network": str(self.network), | ||
| "property": str(self.property), | ||
| "timeout": str(self.timeout), | ||
| "verifier": self.verifier, |
There was a problem hiding this comment.
Why are the verifier, success and result not wrapped into str()?
| def json_write_verification_result( | ||
| verification_result: VerificationDataResult, json_path: Path | ||
| ): | ||
| """_summary_.""" |
There was a problem hiding this comment.
Shouldn't this summary be changed to contain some information?
| file_data = {"instances": []} | ||
|
|
||
| file_data["instances"].append(verification_result.as_json_row()) | ||
| json_file.seek(0) |
| json_path: Path, | ||
| ) -> list[VerificationDataResult]: | ||
| """Reads a verification results json to a list of its dataclass.""" | ||
| results = pd.read_json(json_path)["instances"].tolist() |
There was a problem hiding this comment.
Shouldn't we maybe use the json package for parsing the json here? Pandas can quite easily break for parsing jsons. Also were will an error occuring here be catched?
|
|
||
| def as_json_row(self) -> dict[str, Any]: | ||
| """Convert data to a json item.""" | ||
| if isinstance(self.counter_example, tuple): |
There was a problem hiding this comment.
do we still need this, if the counter example is not returned?
2 participants
Changes: