Cool. I was waiting for it :)
Question: would you have examples of TLA+ specs that are not related to distributed algos (raft, paxos, etc.) or puzzles (die hard, etc.)?
Question: would you have examples of TLA+ specs that are not related to distributed algos (raft, paxos, etc.) or puzzles (die hard, etc.)?
There are also examples in these links:
https://learntla.com/models/example/
https://www.hillelwayne.com/post/modeling-deployments/
https://www.linkedin.com/pulse/lamports-tla-spec-testing-why...
https://github.com/tlaplus/Examples/tree/master/specificatio...
https://github.com/tlaplus/Examples/tree/master/specificatio...