TLA+ toolbox Translate plusCalc result Parse failed

[陈云星]

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

[Markus Kuppe]

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

[陈云星]

Thanks. 

在 2019年11月19日星期二 UTC+8上午12:57:43，陈云星写道：