5 ms·

I haven't watched the videos yet but I have been keeping my eye on TLA+ ever since seeing the whitepaper from Amazon and how they use TLA+ to spec out their dis

I haven't watched the videos yet but I have been keeping my eye on TLA+ ever since seeing the whitepaper from Amazon and how they use TLA+ to spec out their distributed systems. As someone that works on distributed systems that could use some formality I think TLA+ could help, however, I have a hard time really understanding it. Do you know of any straight forward non-trivial examples? Something a little more complex than "hello world" and something that isn't abstract?

ahelwer 10y ago
There's a few I can think of! First, the TLA+ GitHub repo has a bunch of examples[0]. The best one to start with is the Die Hard puzzle[1], where the heroes must obtain four gallons of water given only three and five gallon jugs. In the spec[2] we set up the system and specify all possible actions; then we model-check the system to see whether it can spit out an execution trace of actions to reach a state where we have four gallons of water in a jug. The Wikipedia article also has some good example specs[3]. For your own first specification, I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep. [0] https://github.com/tlaplus/Examples/tree/master/specifications https://github.com/tlaplus/Examples/tree/master/specificatio... [1] https://www.youtube.com/watch?v=6cAbgAaEOVE https://www.youtube.com/watch?v=6cAbgAaEOVE [2] https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla https://github.com/tlaplus/Examples/blob/master/specificatio... [3]https://en.wikipedia.org/wiki/TLA+ https://en.wikipedia.org/wiki/TLA+
hwayne 10y ago
I wrote an essay[0] about a non-trivial example I did at my company. We had to work with several finicky APIs and the TLA+ spec caught several critical bugs with it. Plus, it's purely a business logic system, so it's pretty concrete. If you're interested in learning more, I also wrote a beginner's guide[1] to the language, which contains concrete examples and exercises. [0] https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f#.u3grkd2i3 https://medium.com/espark-engineering-blog/formal-methods-in... [1] https://learntla.com/introduction/ https://learntla.com/introduction/
- chillitom 10y ago
  Following your introduction now, it is a great quick-start tutorial, thanks for creating it.
agentultra 10y ago
As someone who worked with distributed systems for many years before using TLA+ to find bugs and validate work: It's possible to understand it. I think it would help to have a good mentor, as I did, or a lecture series from the language inventor. I ran through the trial version of these videos when Lamport was developing them and it's quite approachable even for someone who's more of a liberal arts kind of person.
colanderman 10y ago
I work on distributed systems and have started pushing for us to use TLA+/PlusCal to model them. I have a simple PlusCal model of a system with two threads which juggles network and disk I/O which I can e-mail you if you like. It's not at all a complex system, but I think it captures the basics of modeling concurrency and I/O well.
jdubray 10y ago
I have created the SAM Pattern [1] (State/Action/Model) based on my interpretation of TLA+. The goal is to make the semantics available to developers. Why not writing code as close as possible to the way it would be specified? SAM can also be used for stateful API/Microservice orchestrations [2] If you want a slightly more formal introduction to SAM and its relationship to TLA+ (again, based on my own interpretation) I gave this lecture last month [3]. [1] http://sam.js.org http://sam.js.org [2] http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api-call-component-with-sam/ http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api... [3] http://cloudsentinel.com/sam-state-machines-and-computation.pptx http://cloudsentinel.com/sam-state-machines-and-computation....
- foxaal 10y ago
  You wonder if there are code generation possibilities...
  - jdubray 10y ago
    Actually, TLA+ (again the way I understand it), after nearly 20 years of MDSE, convinced me that I would very rarely need to generate code. It's a much better value proposition to write correctly factored code. TLA+ is one of the most amazing element of Computer Science. Everyone who writes code should have at least a basic understanding of it.

ahelwer 10y ago

There's a few I can think of! First, the TLA+ GitHub repo has a bunch of examples[0]. The best one to start with is the Die Hard puzzle[1], where the heroes must obtain four gallons of water given only three and five gallon jugs. In the spec[2] we set up the system and specify all possible actions; then we model-check the system to see whether it can spit out an execution trace of actions to reach a state where we have four gallons of water in a jug. The Wikipedia article also has some good example specs[3]. For your own first specification, I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep. [0] https://github.com/tlaplus/Examples/tree/master/specifications https://github.com/tlaplus/Examples/tree/master/specificatio... [1] https://www.youtube.com/watch?v=6cAbgAaEOVE https://www.youtube.com/watch?v=6cAbgAaEOVE [2] https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla https://github.com/tlaplus/Examples/blob/master/specificatio... [3]https://en.wikipedia.org/wiki/TLA+ https://en.wikipedia.org/wiki/TLA+

hwayne 10y ago

I wrote an essay[0] about a non-trivial example I did at my company. We had to work with several finicky APIs and the TLA+ spec caught several critical bugs with it. Plus, it's purely a business logic system, so it's pretty concrete. If you're interested in learning more, I also wrote a beginner's guide[1] to the language, which contains concrete examples and exercises. [0] https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f#.u3grkd2i3 https://medium.com/espark-engineering-blog/formal-methods-in... [1] https://learntla.com/introduction/ https://learntla.com/introduction/

chillitom 10y ago
Following your introduction now, it is a great quick-start tutorial, thanks for creating it.

agentultra 10y ago

As someone who worked with distributed systems for many years before using TLA+ to find bugs and validate work: It's possible to understand it. I think it would help to have a good mentor, as I did, or a lecture series from the language inventor. I ran through the trial version of these videos when Lamport was developing them and it's quite approachable even for someone who's more of a liberal arts kind of person.

colanderman 10y ago

I work on distributed systems and have started pushing for us to use TLA+/PlusCal to model them. I have a simple PlusCal model of a system with two threads which juggles network and disk I/O which I can e-mail you if you like. It's not at all a complex system, but I think it captures the basics of modeling concurrency and I/O well.

jdubray 10y ago

I have created the SAM Pattern [1] (State/Action/Model) based on my interpretation of TLA+. The goal is to make the semantics available to developers. Why not writing code as close as possible to the way it would be specified? SAM can also be used for stateful API/Microservice orchestrations [2] If you want a slightly more formal introduction to SAM and its relationship to TLA+ (again, based on my own interpretation) I gave this lecture last month [3]. [1] http://sam.js.org http://sam.js.org [2] http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api-call-component-with-sam/ http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api... [3] http://cloudsentinel.com/sam-state-machines-and-computation.pptx http://cloudsentinel.com/sam-state-machines-and-computation....

foxaal 10y ago
You wonder if there are code generation possibilities...
- jdubray 10y ago
  Actually, TLA+ (again the way I understand it), after nearly 20 years of MDSE, convinced me that I would very rarely need to generate code. It's a much better value proposition to write correctly factored code. TLA+ is one of the most amazing element of Computer Science. Everyone who writes code should have at least a basic understanding of it.