[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Mon, 11 Jan 2016 07:27:09 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com> <20d67976-47a3-440d-942e-51f3b035554e@googlegroups.com> <393668fc-f7ac-49ad-9f04-598c39d1a771@googlegroups.com> <c6c1cac0-c5d4-46c0-b236-31b9ba2d7d0d@googlegroups.com> <8ef22b8b-cc07-431d-80e9-fa297c087b26@googlegroups.com> <5bcb7c5f-c787-4450-a8f0-efc8f5c64477@googlegroups.com>

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

**Follow-Ups**:**Re: Tagged formulas***From:*Leslie Lamport

**References**:**Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Leslie Lamport

**Re: Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Leslie Lamport

**Re: Tagged formulas***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] Re: TLA+ Toolbox 1.5.2 release** - Next by Date:
**Re: Using tlatext to typeset TLA+ Module that contain PlusCal specification** - Previous by thread:
**Re: Tagged formulas** - Next by thread:
**Re: Tagged formulas** - Index(es):