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