Re: [tlaplus] how to determine total states of model

It sounds like you have unbounded queues: the producer can always append an item to some queue. In that case, the state space will be infinite and TLC will never finish. You can bound the number of states that TLC considers by imposing a state constraint (cf. tab "Spec Options", click on "Additional Spec Options" if that tab is not present), for example "Len(queue) <= 3" and gain confidence through incomplete verification. Add similar constraints for other potential sources of infinite state spaces, for example if you have a counter to number the products.

Stephan

On 11 Dec 2019, at 18:45, 陈云星 <chen.yack@xxxxxxxxx> wrote:

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

--
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/7b15017b-bf39-41b9-8d32-b5baea4b98a8%40googlegroups.com.

--
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/9D9886EA-0C4A-47BF-80D1-EFB786CB5AF7%40gmail.com.