So, the Capture operator works well, except that it introduces a very significant performance hit when model-checking, so I can’t use it…
I’d like to pursue this point just a bit further, and explain the motivation. One of my specs is for a reliable multicast protocol (similar to Skeen’s algorithm) in a virtual synchrony environment. My variables include communication queues, the set of live machines, the state of the replicated state machine `st[m]` (where m is the machine), and each machine’s view, `view[m]` which is the set of machines m believes to be alive.
I have the concept of a node, which is an abstract machine, which at any point in time is mapped to a single physical machine. Also, I have an operator, let’s call it Address(m, n), which given a machine and a node, is equal to the address (i.e. physical machine) that machine m believes to be that of node n according to view[m]. I could explicitly pass view[m] to Address, but that would make things less convenient.
Now, a step may install a new view, view’, in machine m, in which case the protocol dictates that some messages be re-sent. Therefore, I tried to use Address(m, n)', so that the newly installed view be used. That didn’t work because it turns out that the node n in this case is computed from one of the state’s (`st`) fields, and st' has not yet been computed (as TLC requires).
I can’t set st' yet because of the problem I mentioned in an earlier email in this conversation, which is that in order to make things composable, the operator handling the change of view works on one message at a time (it is possible that multiple messages are being multicast concurrently), and so my `HandleNewView` operator returns a tuple containing the new value of st for that particular machine and that particular messages, as well as a sequence of messages to be sent (all because I can’t set a variable’s next value one domain point at a time).
So, perhaps there should be an operator, CAPTURE e, which would be a level-0 value equal to the value of _expression_ e in the current state, so that I could write:
Address(m, CAPTURE n)'
I thought that having such an operator wouldn’t make much sense because semantically it would be a constant, yet its value would change with the state; now I think it’s just a matter of interpretation. (CAPTURE e) can be interpreted as a syntactic construct that simply says "this subexpression is protected from priming".
Ron