With multiple TLC workers, assigning TLCGet value to spec variable results in non-determinism
Nobody has claimed this yet.
- Dominant language
- Java
- Stars
- 3.1k
- Forks
- 264
- Avg merge
- 3d 4h
- Merged PRs (30d)
- 16
Description
See (currently ignored) test introduced in https://github.com/tlaplus/tlaplus/commit/867adc9e6715a5e3a876c92b755319a35e80a23b for details.
Running the Toolbox's Trace Explorer with an expression such as: TLCGet("diameter") internally causes an NPE in TLC. With a liveness property the NPE doesn't get handled gracefully resulting in a bogus:
@!@!@STARTMSG 1000:1 @!@!@
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
The error occurred when TLC was checking liveness.
The exception was a java.util.concurrent.ExecutionException
: tlc2.tool.EvalException: @!@!@STARTMSG 2123:0 @!@!@
Failed to recover the initial state from its fingerprint.
@!@!@ENDMSG 2123 @!@!@
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the currently ignored test introduced in commit 867adc9e6715a5e3a876c92b755319a35e80a23f and reproduce the TLCGet("diameter") case with multiple TLC workers. Trace the failure through the Trace Explorer and liveness-checking path. Done means the test no longer observes nondeterminism or an internal NPE, and the liveness error is reported correctly.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- java
- Domain
- devtools
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100