Re: [tlaplus] TLA+ toolbox Translate plusCalc result Parse failed

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

Hi,

Pluscal/TLA+ doesn't have a "==" operator.

Hope this helps,
Markus

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