Great talk! The example with a pool of messages and workers that read from it to start long-running tasks, sounds a lot like a system I've been working with. I hope to try modeling it with TLA+ -- I'm sure it'll find a number of surprises!
It is completely independent from the code you've written. It is your job to keep the two in sync as needed. There are approaches that can modelcheck your actual code... there are advantages and disadvantages to doing either.
you need to transform the TLA+ spec to your code. TLA+ spec ensures (using invariants etc.) that the logic you have is correct and statisfies the requirements.
Great talk! The example with a pool of messages and workers that read from it to start long-running tasks, sounds a lot like a system I've been working with. I hope to try modeling it with TLA+ -- I'm sure it'll find a number of surprises!
Excellent talk with great pacing!
TLA+ part starts at 11:16
*Awesome!!!*
Excellent talk
I came across the TLA+ definition: Temporal Logic of Actions - th-cam.com/video/-4Yp3j_jk8Q/w-d-xo.html
I still don't understand how the TLA+ spec work with your code that you've written.
It is completely independent from the code you've written. It is your job to keep the two in sync as needed. There are approaches that can modelcheck your actual code... there are advantages and disadvantages to doing either.
you need to transform the TLA+ spec to your code. TLA+ spec ensures (using invariants etc.) that the logic you have is correct and statisfies the requirements.