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

[tlaplus] Video Tutorial (Request for Feedback)



Hello,

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

https://youtu.be/alyqcphUaiI

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.

Sincerely,
Jeremy

--
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.