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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 19 Dec 2022 07:30:15 +0100*References*: <d5726e3d-1761-4bac-be66-dbb788f7b42cn@googlegroups.com>

Hello, TLA+ is more general than PlusCal, and a systematic conversion to PlusCal is unlikely to yield idiomatic results, if it is possible at all: you will probably end up with a single while loop containing all possible actions. It is a bit like the normal form theorem in computability theory.
--
In PlusCal you could represent this as with (n \in CN, p \in BOOLEAN) { await (predicate[n] => p); predicate[n] := p }
You could perhaps write variables bcNode \in CN \union FN, bcValue \in (CASE bcNode \in CN -> Value [] bcNode \in FN -> {NotValue}); 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/EF2E36DD-EB82-4CF4-9383-34E258045780%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

- Prev by Date:
**Re: [tlaplus] Functions in the standard libraries** - Next by Date:
**Re: [tlaplus] Functions in the standard libraries** - Previous by thread:
**[tlaplus] Converting TLA+ spec to PlusCal** - Next by thread:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Index(es):