Repository navigation
tla: check.sh resolves a relative jar path; TODO: spurious wake-ups done - #232
Conversation
…DO: spurious wake-ups done CodeRabbit on #231: a relative jar path broke the two mutant checks, which run in a directory of their own; check.sh now resolves it as trace.sh does (tested with a relative path). TODO.md: the done steps and the run prompt of the spurious wake-ups removed, the result and its known limits kept; the A6 open point and the A16 wording follow. Co-Authored-By: Claude Opus 5.5 <[email protected]> Claude-Session: https://claude.ai/code/session_01S8cAMbADd1y9p36iFrVkAd
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 35 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
|
|
Coverage is 100.0% — fix/check-jar-path into main. No base build found for |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #232 +/- ##
=========================================
Coverage 99.20% 99.20%
Complexity 165 165
=========================================
Files 1 1
Lines 376 376
Branches 51 51
=========================================
Hits 373 373
Partials 3 3 ☔ View full report in Codecov by Harness. |
Summary
check.shresolves its jar path before it changes directories, astrace.shdoes. With a relative path, the two mutant checks ran in a directory of their own and could not load TLC. CodeRabbit found this on TLA+: spurious wake-ups of Condition.await() in the models and proofs #231. CI passes an absolute path, so CI was not affected.TODO.md: the steps and the run prompt for the spurious wake-ups are done, so I removed them and kept the result with its known limits. The A6 open point is removed, the open-items row is gone, and the A16 wording now treats spurious wake-ups as a model assumption.Test plan
check.shrun with a relative jar path:WaitAlone1clean,mutant-WaitAlone1clean,mutant-SpuriousWaitAlone1violatesWaitEnoughOrClosedbash -n src/test/tla/check.shTODO.md)Related issues / PRs
Follow-up to #231.
Checklist
CONTRIBUTING.mdandCODE_OF_CONDUCT.mdSECURITY.md)🤖 Generated with Claude Code
https://claude.ai/code/session_01S8cAMbADd1y9p36iFrVkAd