-
-
Notifications
You must be signed in to change notification settings - Fork 40
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Return failure data from pass chain executions #2186
Conversation
Codecov Report
@@ Coverage Diff @@
## main #2186 +/- ##
==========================================
- Coverage 80.63% 80.62% -0.01%
==========================================
Files 423 426 +3
Lines 13898 13927 +29
Branches 1887 1840 -47
==========================================
+ Hits 11206 11229 +23
- Misses 2692 2698 +6
📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
Cannot link to a type alias I guess
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In general, this looks good to me. I can see how serialization for the server mode requires these changes. One thing I could not understand is: Why are we using upickle
now? Is it a replacement for ujson
or is it complimentary?
def apply(module: TlaModule, trace: DecodedExecution, invViolated: TlaEx): Counterexample = { | ||
// TODO(shonfeder): This conversion seems kind of senseless: we just swap the tuple and convert the transition index to | ||
// a string. Lots depends on this particular format, but it seems like a pretty pointless intermediary structure? | ||
val states = trace.path.map(p => (p._2.toString, p._1)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why do we convert an integer to a string here? Is it for the future compatibility, or is it because JSON has limitations on numbers?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't know why this conversion is done. In fact, I don't know why we transform a "tract" into this "states" structure at all. But several other structures depend on it, and i was trying to limit the scope the of this changeset. This was picked up from DumpFilesModelCheckerLIstener.scala
line 41. I was thinking to remove this conversion in a followup, but could include it in this PR if you'd prefer. WDYT?
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/DumpFilesModelCheckerListener.scala
Show resolved
Hide resolved
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Counterexample.scala
Show resolved
Hide resolved
tla-io/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the review!
I think I could use a bit more info on how to effect the reorganization you've suggested.
re: upickle
-- ujson
is a json specific library that is part of the upickle
toolkit. upickle
is a more general purpose serialization/deserialiation library, and it enables automated derivation of serializers and deserializers. It is being used here to automatically derive the converts for PassFailure
and used for the serialization implicts in CheckerResult
and Counterexample
.
I expect I could do without it tho, if you think it'd better for us to avoid the dependency. WDYT?
def apply(module: TlaModule, trace: DecodedExecution, invViolated: TlaEx): Counterexample = { | ||
// TODO(shonfeder): This conversion seems kind of senseless: we just swap the tuple and convert the transition index to | ||
// a string. Lots depends on this particular format, but it seems like a pretty pointless intermediary structure? | ||
val states = trace.path.map(p => (p._2.toString, p._1)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't know why this conversion is done. In fact, I don't know why we transform a "tract" into this "states" structure at all. But several other structures depend on it, and i was trying to limit the scope the of this changeset. This was picked up from DumpFilesModelCheckerLIstener.scala
line 41. I was thinking to remove this conversion in a followup, but could include it in this PR if you'd prefer. WDYT?
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Counterexample.scala
Show resolved
Hide resolved
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/DumpFilesModelCheckerListener.scala
Show resolved
Hide resolved
Co-authored-by: Igor Konnov <igor@informal.systems>
Thanks for the review! Definitely improved thanks to the comments. |
Welp, getting rid of that seemingly useless conversion to strings broke something in the tests, and they are proving to be quite brittle and hard to get signal from. All they'll tell me off the bat is:
And getting feedback on the comparison doesn't help much:
These errors look to me to be white space differences, due to the tests relying on hardcoded formatted JSON comparisons 😭 We talk tomorrow whether this superficial cleanup is worth the slowdown for the moment (also I guess risking breaking some quirk of the coutnerexamples?). |
aaa793d
to
6a43f7f
Compare
I've dropped the refactoring commits, and will merge this as is to unblock server-mode work. I've created a separate WIP branch to track to the refactoring to move the |
Co-authored-by: Igor Konnov <igor@informal.systems>
Closes #2185, #2170
This PR enriches the
PassResult
so that it can it can include data about the reasons for pass failures. The approach here is currently going for the shortest path to getting the needed JSON-encodable data for RPC calls.Further work could be useful to impose a more rigorous interface. In particular, it could be helpful to reorganize the package dependencies so that the failure data returned by different passes could be enumerated in a case class, allowing static specification of the supported data structures. This is apposed to he approach taken here, which just converts the pass data into ujson. The latter approach is expedient given the current motivating need, but won't be nice to work with if we decide we want to use this data for purposes other than returning RPC results.
make fmt-fix
(or had formatting run automatically on all files edited)./unreleased/
for any new functionality