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