Re: [tlaplus] New blog series: TLA+ for startups

On Sun, 8 Dec 2019 at 21:43, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote:

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

On Sun, Dec 8, 2019 at 8:51 PM Neil O'Connor <neil.oconnor@xxxxxxxxx> wrote:
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

On Sun, 8 Dec 2019 at 18:27, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
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

On 6 Dec 2019, at 12:16, Neil O'Connor <neil.oconnor@xxxxxxxxx> wrote:

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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3bbbb414-b1c5-427b-b1a4-7e5929dd69dd%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/E541E1B4-7546-47C1-A086-0F4051EF51B3%40gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CADqF4ttcNSXQmU583uuMPF3%3DVctEs3TdrVPsqhCUAfDy-eOXkQ%40mail.gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFteovKrLndPMybPUvOUT_iA1jj-698A1vJ_ua0SLY16jMK0jg%40mail.gmail.com.