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

[tlaplus] [Q on multiple agent update in step]

Hello all
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.

Attachment: two_changes_step.tla
Description: Binary data