I'm use TLA+ model single producer dispatch to multiple queue and consume by multiple consumer
but at any time for some queue, at most one consumer consume it.
this model use two type of queue:
1. schedule Queue : only one, notify and schedule consume consume some data Queue
2. data Queue(s) : contains the data need consume by consumer
there are one producer thread produce data to data Queue(s) (dispatch by data's catalog)
and many consumer thread will consume data Queue(s).
in this model, producer / consumer will schedule consume next batch when they need.
for consumer it will consume a batch and test if queue not empty, then schedule next round of consume by put a msg to schedule Queue.
for producer it will test if the data Queue change from empty to not empty, if this was true, it will schedule consume by put a msg to schedule Queue.
in this model, how many state will be ?
for model contains queue(s) , can we convert it to FSM ?
I use TLC check, will run long time and seemly can't terminated, it producer 17GB's data on my laptop (macbook pro).