[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: TLA+ toolbox Translate plusCalc result Parse failed
在 2019年11月19日星期二 UTC+8上午12:57:43，陈云星写道：
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:
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
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/69544eee-eb44-42de-bee7-fe086c315b39%40googlegroups.com.