3 ms·
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 har
by couac 9y ago
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.)?
- pron 9y agoPart 3 has examples of two sorting algorithms. There are also examples in these links: https://learntla.com/models/example/ https://learntla.com/models/example/ https://www.hillelwayne.com/post/modeling-deployments/ https://www.hillelwayne.com/post/modeling-deployments/ https://www.linkedin.com/pulse/lamports-tla-spec-testing-why-youre-using-nira-amit https://www.linkedin.com/pulse/lamports-tla-spec-testing-why... https://github.com/tlaplus/Examples/tree/master/specifications/allocator https://github.com/tlaplus/Examples/tree/master/specificatio... https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/CachingMemory https://github.com/tlaplus/Examples/tree/master/specificatio...
- Jach 9y agoThis link hit HN not too long ago: https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f https://medium.com/espark-engineering-blog/formal-methods-in... (https://news.ycombinator.com/item?id=14221848 https://news.ycombinator.com/item?id=14221848) (Edit: Ah, already linked within pron's second link... Oh well.)