New blog series: TLA+ for startups

[Neil O'Connor]

Hey folks,

I've started a new blog series that attempts to advocate for using TLA+ in smaller teams and startup environments. I am, in fact, trying to demystify TLA+ for my own team, and in the process help others in a similar position do the same.

As I'm new to TLA+ myself, I decided to try to illustrate my point by walking through a superficially simple system concept (elevator control software), which I think will actually get fiendishly complex quite quickly as it is expanded. Elevator control software is not what we do as a team, but I wanted to use an example that anyone could relate to.

I've done two posts so far, starting here: https://medium.com/koodoo/tla-for-startups-part-1-8b162863824b

I'd very much welcome feedback from the community on a) whether you think I'm onto something with my core hypothesis, or on a complete hiding to nothing; and b) how it could be improved. In particular, as a relative newcomer, I'm quite sure I will have used some of the wrong terminology, made some dumb choices, or explained something incorrectly. I would be very much open to corrections and suggestions!

Next up in the series, I'm going to attempt to create a useful temporal formula for my elevator's behaviours. Wish me luck...

Thanks,

Neil

[Andy Dwelly]

It’s a very nice example - I went through part 2 with my study group (Worthing UK fwiw) and we tried a few tweaks. The only change I’d suggest is putting the enabling conditions at the beginning of each formula rather than mixed up with the primed terms. I’ve got a feeling that this makes things a bit easier for TLC, and I certainly find it a bit easier to read since I can tell at once whether or not a formula is relevant to in a particular situation.

[Neil O'Connor]

That’s great, Andy, and thanks for the suggestion - I will certainly make that change.

Interesting to hear you have a study group. I was thinking of starting a Nottingham meetup along the same lines, so would be interested to compare notes.

Neil

On Sat, 7 Dec 2019 at 11:58, Andy Dwelly <andyd...@gmail.com> wrote:

It’s a very nice example - I went through part 2 with my study group (Worthing UK fwiw) and we tried a few tweaks. The only change I’d suggest is putting the enabling conditions at the beginning of each formula rather than mixed up with the primed terms. I’ve got a feeling that this makes things a bit easier for TLC, and I certainly find it a bit easier to read since I can tell at once whether or not a formula is relevant to in a particular situation.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/537f91ed-4ffa-4efd-8f41-af4a6f5030d5%40googlegroups.com.

--

Neil O'Connor

Chief Technology Officer

07791 182916

[Stephan Merz]

Hi,

nice work! Here are a few comments.

1. I suggest replacing the initial condition

carLocation = CHOOSE s \in Storeys : TRUE

with

carLocation \in Storeys

The former leaves the initial floor of the elevator unspecified, but fixed. In fact, TLC will explore only one initial state (either 1 or 2), and this might just happen to mask an error. The latter expresses non-determinism: initially the elevator can be at either floor, and TLC will explore all (here both) possible initial states.

2. I'm a bit surprised that the action ECNextCall(s) is enabled even when the elevator is at floor s and records the call (so the elevator will later travel back to that floor). I would have expected the precondition

carLocation # s

– that is, pressing the call button has no effect when the elevator is at floor s. Well, perhaps this is one of the gotchas that you mention at the end. 

3. On terminology: in TLA+, a "state" is an assignment of values to variables, and a "state formula" is an expression that can be evaluated in a single state (it cannot contain primed variables because you need two states for evaluating them). You sometimes write "state" or "state formula" when you really mean "action", i.e. a formula with primed and unprimed variables.

4. An elevator that serves just two floors is really simple, and your spec takes advantage of that simplicity (when the elevator has to move, there is only one possible direction). I would have found it more natural to start off with N floors, but presumably that will be the subject of a subsequent post.

Keep up the good work!

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3bbbb414-b1c5-427b-b1a4-7e5929dd69dd%40googlegroups.com.

[Neil O'Connor]

That's extremely helpful, thanks Stephan. I'll make some updates for points 1 and 3 in the next couple of days.

Regarding points 2 and 4, yes they were deliberate choices. For the anomaly you highlight in point 2, I am planning to demonstrate how TLC can help catch little oversights like this and lead to better system designs, even when you are operating at startup development team pace.

Thanks for taking the time to read and feed back - I really appreciate it.

Neil

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/E541E1B4-7546-47C1-A086-0F4051EF51B3%40gmail.com.

[Karolis Petrauskas]

Nice work!

I would suggest to add L Lamport's "Specifying systems" to the list of important links (https://lamport.azurewebsites.net/tla/book-02-08-08.pdf or https://www.amazon.com/Specifying-Systems-Language-Hardware-Engineers/dp/032114306X).

For me that was very convenient to start from.

Best regards

Karolis

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CADqF4ttcNSXQmU583uuMPF3%3DVctEs3TdrVPsqhCUAfDy-eOXkQ%40mail.gmail.com.

[Neil O'Connor]

Great point, I will do that! Thanks.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFteovKrLndPMybPUvOUT_iA1jj-698A1vJ_ua0SLY16jMK0jg%40mail.gmail.com.