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
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'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.