# [tlaplus] Launching two sets of processes from the same base set in PlusCal

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

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