Launching two sets of processes from the same base set in PlusCal

[Andrew Helwer]

Consider a protocol similar to Paxos, where each node in the cluster runs multiple processes concurrently - Proposer and Acceptor. The two processes access shared memory, maybe a local database. We might write this as follows:

----------------------------- MODULE Example -----------------------------

CONSTANTS Node, Value

NoValue == CHOOSE v : v \notin Value

(*--algorithm Example

variables

    sharedMemory = [n \in Node |-> NoValue]

process Acceptor \in Node
begin
    RunAcceptor:
        \* Do something with sharedMemory[self] here

        skip;

end process;

process Proposer \in Node
begin
    RunProposer:
        \* Do something with sharedMemory[self] here

        skip;

end process;

end algorithm;*)

=============================================================================

PlusCal doesn't allow this, because its PC function maps elements of Node to only one value so the two processes cannot run concurrently. What is the best way to accomplish what I'm trying to do?

Andrew

[Catalin Marinas]

On Mon, 12 Aug 2019 at 17:13, Andrew Helwer <andrew...@gmail.com> wrote:
> Consider a protocol similar to Paxos, where each node in the cluster runs multiple processes concurrently - Proposer and Acceptor. The two processes access shared memory, maybe a local database. We might write this as follows:

[...]
> process Acceptor \in Node
[...]
> process Proposer \in Node
[...]

> PlusCal doesn't allow this, because its PC function maps elements of Node to only one value so the two processes cannot run concurrently. What is the best way to accomplish what I'm trying to do?

I used a tuple on a few occasions, e.g.:

process Acceptor \in Node \X {0}
...
process Proposer \in Node \X {1}

but you'd need to be aware of this bug:

https://github.com/tlaplus/tlaplus/issues/164

--
Catalin