[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Video Tutorial (Request for Feedback)


I recorded a tutorial using TLA+ and the dump dot feature as a means to sketch simple designs.


During the iteration of the design I disable deadlock detection (with a justification), but I am suspicious of my reasoning: https://youtu.be/alyqcphUaiI?t=1260

The specification I used is here: https://github.com/JeremyLWright/specs/blob/master/algorithm/SodaMachine/SodaMachine.tla

I feel there is probably a better method to continue checking temporal properties instead of disabling deadlock detection. If someone has the time I'd appreciate any feedback.

Finally, this was a fun process sketching the spec, then recording the video. I'd like to make more. If anyone has ideas that would be interesting I'd happily considering doing a similar video tutorial.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC2JkJuGOxVzQaJEcajG33h6zv0QP%2BYbXciG%3D%3DrVettqOn2OVw%40mail.gmail.com.