[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA+ toolbox Translate plusCalc result Parse failed
On 18.11.19 08:57, 陈云星 wrote:
> |I'm 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
> 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
> Residual stack trace follows:
> 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.
> Junction Item starting at line 229, column 18.
Pluscal/TLA+ doesn't have a "==" operator.
Hope this helps,
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/2f9447e3-b6a6-d8e2-02ba-97cc1e525309%40lemmster.de.