5 ms·

Genuine question: how does this compare versus something like modelling in primitive python? what benefits are there, or is it just a case of age and that this

Genuine question: how does this compare versus something like modelling in primitive python? what benefits are there, or is it just a case of age and that this is language / system agnostic? I'm just finishing cosmic python[0], which talks about making a primitive model of your system first, that you can run business logic tests on, then all the other code depends upon that (domain driven design / onion layers, etc). To me it seems like this is the same thing. The only aspect that stuck out was the "two transfers at the same time" which to me, seems like it would depend on how you're implementing the model, rather than the model itself? For instance, the example in [1] could also be done in primitive python, (arguably easier to read in my opinion but I'm not used to TLA syntax :) @dataclass class Person: balance: int def wire(a: Person, b: Person, amount: int): if a.balance >= amount: a.balance -= amount b.balance += amount @pytest.mark.parametrize( "a_amount, b_amount, transfer, a_remaining, b_remaining", [ (10, 10, 10, 0, 20), # matching amount (6, 10, 10, 6, 10), # has less (0, 10, 10, 0, 10), # has nothing (10, 0, 10, 0, 10), # to empty account ], ) def test_wire(a_amount, b_amount, transfer, a_remaining, b_remaining): a = Person(balance=a_amount) b = Person(balance=b_amount) wire(a, b, transfer) assert a.balance == a_remaining assert b.balance == b_remaining The author did mention "... could be done in python" as well, so I doubt it's a case of not knowing about python, but perhaps my question is "why TLA over python?" [0]https://www.cosmicpython.com/ https://www.cosmicpython.com/ [1]https://www.learntla.com/intro/conceptual-overview.html https://www.learntla.com/intro/conceptual-overview.html

pron 4y ago
There are two parts to the answer: the expressivity of the language, and the available tools. TLA+ is not a programming language, and so cannot "run," but it is more expressive than any programming language could ever be, and can describe any discrete system at any arbitrary level of detail. This is particularly useful when the described system has some or a lot of nondeterminism, as is the case in distributed and concurrent systems. It is very easy in TLA+ to say "one of these things could happen at any time", or "the value of a variable can only grow monotonically over the system's lifetime", and it is easy to describe assertions of arbitrary complexity about a system, such as "every order that's received more than once will eventually be flagged." As for tooling, while you cannot efficiently "run" TLA+ specifications, you can check your assertions in two ways: either with the proof assistant (although that requires a lot of effort), or with a model checker, that is places more limitations on what it is that you can check but is completely automatic.
xtagon 4y ago
TLA+ is for writing specifications of models, and programming languages are for implementing the models. Sometimes there is very little difference, and sometimes there is more. It's subtle in simpler examples like yours but becomes a little more obvious if you watch Leslie Lamport's video course: https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html The magic comes into play when you do things like using solvers (built into the TLA+ toolkit) to check invariants. This wouldn't be possible do with a code implementation alone, except for if you were to write property tests using a property testing framework or scenario generator using knowledge of all states the domain could be in. Your TLA+ specification is a mathematical formula of the states it can be in (even over time) while the Python implementation is more like a state machine that takes one input and results in an output. Of course, in your example, you do something akin to property testing with pytest where you enumerate known states, I'm just using this to help describe the spec/implementation difference. In more complex models, testing property invariants may require enumerating more examples than you think to write tests for, and the important cases may not be what you expect. And as your property testing parameters get more complex in the search space, what your Python code ends up being is both an implementation (the runtime code) and a de-coupled model of the states it can be in (the test code) when conceptually it is one model. And in TLA+, you can specify it as a model and use the invariant checker as both a way to test your assumptions and a way to explore important states or state transitions.
- fijiaarone 4y ago
  If it takes a programmer in a specific (unused) programming language to write a specification, why not just write it in a working programming language? As we can see from the comment above, we need to write a compiler and tests to check the specification anyway.
  - Jtsummers 4y ago
    Python (and most languages) and testing likely won't detect the concurrency bug in the above program, unless you get lucky. TLA+ and model checking will. You use TLA+ to examine a spec or design without the extraneous details and do V&V on it. Then you go back to your code and you can be more confident that what you are making will work as intended. It is complementary, not a full alternative. You'll still want tests for your code.
Jtsummers 4y ago
TLA+'s model checker will verify (NB: this has scaling limits, but that isn't a problem for many practical circumstances) that two concurrent wires (when the system is properly specified) won't stomp on each other. Conversely, it will detect when they could stomp on each other. So take that definition for the wire function and let two processes run it simultaneously: alice.balance = 100 spawn(wire(alice, bob, 100)) spawn(wire(alice, bob, 100)) Only one of these should succeed, but since the function isn't guaranteed to be atomic we can get to this state: p1: if a.balance >= amount: -- true, so continues into the condition body a.balance -= amount -- process paused here b.balance += amount p2: if a.balance >= amount: -- true, so continues into the condition body a.balance -= amount -- alice's balance now 0 b.balance += amount -- bob gets 100 When p1 resumes after p2 finishes, Alice will end up with a balance of -100 and Bob will get 200. Assuming overdrafts aren't allowed (per the spec they aren't) then the system has reached an invalid state. When testing concurrent programs it is a non-trivial thing to force these states, so bugs like this are hard to detect because they may only occur occasionally. And because they occur rarely, even when detected the actual source of the bug can be hard to reliably discern. TLA+'s model checker will check each possible interleaving of the two processes (in this case) and will discover the invalid execution path I showed above. Then you can go back to the spec and address the issue and rerun the checker, if your invariants hold (no sequence of actions lead to overdraft, in this case) then you can have confidence that, at least with regard to the properties you've specified, the system is correct.
avgcorrection 4y ago
Why do articles about OOP articles always use employee/payment/inventory management systems as examples… just feels like I’m right back at work.
brabel 4y ago
This seems to have been copied straight from the Spock Framework[1] (which I've been using for comprehensive tests for several years), but worse. Here's what it looks like in Spock: @Canonical class Person { int balance def wire(Person other, int amount) { if (balance >= amount) { balance -= amount other.balance += amount } } } class PersonSpec extends Specification { def 'transferring #amount amount'() { given: 'two people' def pa = new Person(balance = a), pb = new Person(balance = b) when: 'an amount is transferred from a to b' pa.wire(pb, amount) then: 'the transfer succeeds if possible, or nothing happens otherwise' pa.balance == expectedA && pb.balance == expectedB where: amount | a | b || expectedA | expectedB 0 | 0 | 0 || 0 | 0 10 | 20 | 0 || 10 | 10 10 | 10 | 10 || 0 | 20 10 | 9 | 10 || 9 | 10 } } [1] https://spockframework.org/spock/docs/2.1/spock_primer.html https://spockframework.org/spock/docs/2.1/spock_primer.html
- jleahy 4y ago
  Spock is not a system for formal (ie. exhaustive) verification.
  - brabel 4y ago
    I did not say it is. I just said the Python code the parent commenter posted was just like Spock, but for Python. Also: tests like that can be provably comprehensive in the cases they handle (which can be generated, you don't need to manually list them all), but that was not my point.

pron 4y ago

There are two parts to the answer: the expressivity of the language, and the available tools. TLA+ is not a programming language, and so cannot "run," but it is more expressive than any programming language could ever be, and can describe any discrete system at any arbitrary level of detail. This is particularly useful when the described system has some or a lot of nondeterminism, as is the case in distributed and concurrent systems. It is very easy in TLA+ to say "one of these things could happen at any time", or "the value of a variable can only grow monotonically over the system's lifetime", and it is easy to describe assertions of arbitrary complexity about a system, such as "every order that's received more than once will eventually be flagged." As for tooling, while you cannot efficiently "run" TLA+ specifications, you can check your assertions in two ways: either with the proof assistant (although that requires a lot of effort), or with a model checker, that is places more limitations on what it is that you can check but is completely automatic.

xtagon 4y ago

TLA+ is for writing specifications of models, and programming languages are for implementing the models. Sometimes there is very little difference, and sometimes there is more. It's subtle in simpler examples like yours but becomes a little more obvious if you watch Leslie Lamport's video course: https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html The magic comes into play when you do things like using solvers (built into the TLA+ toolkit) to check invariants. This wouldn't be possible do with a code implementation alone, except for if you were to write property tests using a property testing framework or scenario generator using knowledge of all states the domain could be in. Your TLA+ specification is a mathematical formula of the states it can be in (even over time) while the Python implementation is more like a state machine that takes one input and results in an output. Of course, in your example, you do something akin to property testing with pytest where you enumerate known states, I'm just using this to help describe the spec/implementation difference. In more complex models, testing property invariants may require enumerating more examples than you think to write tests for, and the important cases may not be what you expect. And as your property testing parameters get more complex in the search space, what your Python code ends up being is both an implementation (the runtime code) and a de-coupled model of the states it can be in (the test code) when conceptually it is one model. And in TLA+, you can specify it as a model and use the invariant checker as both a way to test your assumptions and a way to explore important states or state transitions.

fijiaarone 4y ago
If it takes a programmer in a specific (unused) programming language to write a specification, why not just write it in a working programming language? As we can see from the comment above, we need to write a compiler and tests to check the specification anyway.
- Jtsummers 4y ago
  Python (and most languages) and testing likely won't detect the concurrency bug in the above program, unless you get lucky. TLA+ and model checking will. You use TLA+ to examine a spec or design without the extraneous details and do V&V on it. Then you go back to your code and you can be more confident that what you are making will work as intended. It is complementary, not a full alternative. You'll still want tests for your code.

Jtsummers 4y ago

TLA+'s model checker will verify (NB: this has scaling limits, but that isn't a problem for many practical circumstances) that two concurrent wires (when the system is properly specified) won't stomp on each other. Conversely, it will detect when they could stomp on each other. So take that definition for the wire function and let two processes run it simultaneously: alice.balance = 100 spawn(wire(alice, bob, 100)) spawn(wire(alice, bob, 100)) Only one of these should succeed, but since the function isn't guaranteed to be atomic we can get to this state: p1: if a.balance >= amount: -- true, so continues into the condition body a.balance -= amount -- process paused here b.balance += amount p2: if a.balance >= amount: -- true, so continues into the condition body a.balance -= amount -- alice's balance now 0 b.balance += amount -- bob gets 100 When p1 resumes after p2 finishes, Alice will end up with a balance of -100 and Bob will get 200. Assuming overdrafts aren't allowed (per the spec they aren't) then the system has reached an invalid state. When testing concurrent programs it is a non-trivial thing to force these states, so bugs like this are hard to detect because they may only occur occasionally. And because they occur rarely, even when detected the actual source of the bug can be hard to reliably discern. TLA+'s model checker will check each possible interleaving of the two processes (in this case) and will discover the invalid execution path I showed above. Then you can go back to the spec and address the issue and rerun the checker, if your invariants hold (no sequence of actions lead to overdraft, in this case) then you can have confidence that, at least with regard to the properties you've specified, the system is correct.

avgcorrection 4y ago

Why do articles about OOP articles always use employee/payment/inventory management systems as examples… just feels like I’m right back at work.

brabel 4y ago

This seems to have been copied straight from the Spock Framework[1] (which I've been using for comprehensive tests for several years), but worse. Here's what it looks like in Spock: @Canonical class Person { int balance def wire(Person other, int amount) { if (balance >= amount) { balance -= amount other.balance += amount } } } class PersonSpec extends Specification { def 'transferring #amount amount'() { given: 'two people' def pa = new Person(balance = a), pb = new Person(balance = b) when: 'an amount is transferred from a to b' pa.wire(pb, amount) then: 'the transfer succeeds if possible, or nothing happens otherwise' pa.balance == expectedA && pb.balance == expectedB where: amount | a | b || expectedA | expectedB 0 | 0 | 0 || 0 | 0 10 | 20 | 0 || 10 | 10 10 | 10 | 10 || 0 | 20 10 | 9 | 10 || 9 | 10 } } [1] https://spockframework.org/spock/docs/2.1/spock_primer.html https://spockframework.org/spock/docs/2.1/spock_primer.html

jleahy 4y ago
Spock is not a system for formal (ie. exhaustive) verification.
- brabel 4y ago
  I did not say it is. I just said the Python code the parent commenter posted was just like Spock, but for Python. Also: tests like that can be provably comprehensive in the cases they handle (which can be generated, you don't need to manually list them all), but that was not my point.