I am trying to use TLA+ write spec to verify concurrency correctness of my production problem:
one producer produce msg to Q a,
if it found no more consumer was scheduled. it schedule one consumer by send a notifyMsg to nofityQ b,
multiple consumers poll the notifyQ and consume the Q a to consume the msg.
each consumer will consume batch of msgs, then sleep and retry to pull notifyQ b.
to promise only one consumer process the Q a at any time point. the producer and consumer must make sure exactly one NotifyMsg send to notifyQ b.
there are third type Thread, IdleHandler, check the Q a is empty more than some time, it try to release the Q for release memory hold by this Queue.
thesis three type of thread concurrently working:
1. one producer thread
2. many consumer thread
3. one idleHandler thread
the following spec will translated, but after translated, parse failed with error Msg:***Parse Error***
Encountered "Beginning of definition" at line 229, column 38 in module TableQueueVerify
ExtendableExpr starting at line 229, column 24.
_expression_ starting at line 229, column 24.
IF THEN ELSE starting at line 229, column 21.
_expression_ starting at line 229, column 21.
SPEC FILE is : https://justpaste.it/39pru