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

[Lev Broido <lev.broido@xxxxxxxxx>]

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 

Thanks

-- 
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