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

[Catalin Marinas <catalin.marinas@xxxxxxxxx>]

On Mon, 12 Aug 2019 at 17:13, Andrew Helwer <andrew.helwer@xxxxxxxxx> 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

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHkRjk4xJ%3Dx55aGY5tyHk_hyO5HabtBDK2Qm6Fx8s0OMU2NMig%40mail.gmail.com.