[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] [Q on multiple agent update in step]
In attached example , I tried to define toy spec that allows producer / consumer protocol with multiple agents .
The main question is what is the canonical way to specify multiple changes in a single step
Additional questions are in the body of spec in comments
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/CAB%3D60u7mNcxUmMKEiQSM9%2Brjan4hJnAz4bQwKTcRKTHzVB4P9w%40mail.gmail.com.
Description: Binary data