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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 21 Dec 2022 08:38:02 +0100*References*: <d5726e3d-1761-4bac-be66-dbb788f7b42cn@googlegroups.com> <EF2E36DD-EB82-4CF4-9383-34E258045780@gmail.com> <3fb78eb2-9d83-4e1b-b747-29a683469f7an@googlegroups.com>

In PlusCal, "with x \in S do ..." expresses non-deterministic choice, not a loop. The body of the "with" instruction is executed for some peer, then TLC backtracks and explores the remaining choices. Remember that TLC is a model checker that explores all runs of an algorithm, not an interpreter that generates one run. Therefore, "print" instructions are often hard to interpret. I am not sure what exactly you are trying to achieve. The end result can of course be obtained by writing msgs := [pid \in peers |-> [t |-> "PROPOSE"]]
-- Stephan
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/D2B7A8E7-AE47-41CB-8696-1E4378B8E348%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**References**:**[tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Stephan Merz

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

- Prev by Date:
**Re: [tlaplus] Unknown error in my model** - Next by Date:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Previous by thread:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Next by thread:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Index(es):