Please also note that SAM is “my” interpresentation of TLA+ as a programming model. I exchanged several emails with Dr. Lamport last year, as I was laying SAM’s foundation, but by no means he has validated SAM, or SAM would be the only way to translate TLA+ semantics into a programming model.
I can certainly share more specific references inside Dr. Lamport’s book to explain how I created SAM from TLA+.
The key to understand (which most people find unusual) is that TLA+ describes state machines, but not with the semantics we are all accustomed to. I try to explain it here: http://sam.js.org/#sm
Then of course the next step is to decide how TLA+ semantics apply to Front-End architectures. The traditional semantics of State Machines (Petri nets) are not a good fit, but TLA+ is very different. That’s why I believe it is applicable.
