-------------------------------------------
In evaluation, the identifier buffer is either undefined or not an operator.
line 64, col 19 to line 64, col 24 of module BlockingQueue
-------------------------------------------
I am not sure what I am missing here.On 04.11.20 13:51, Smruti Padhy wrote:
>
> [...]
> ---------------------------------------------------------------------------------------------------------
>
> In computing initial states, the right side of \IN is not enumerable.
>
> line 26, col 21 to line 26, col 40 of module producer_consumer
>
> The error occurred when TLC was evaluating the nested
>
> expressions at the following positions:
>
> 0. Line 74, column 11 to line 75, column 27 in producer_consumer
>
> 1. Line 74, column 14 to line 74, column 26 in producer_consumer
>
> 2. Line 26, column 18 to line 29, column 79 in producer_consumer
>
> 3. Line 26, column 21 to line 26, column 40 in producer_consumer
>
> ------------------------------------------------------------------------------------------------------------
>
> I also checked the BlockingQueue spec for TypeInv. The same error is
> shown in the TLC.
>
> So, I couldn't check IInv is an invariant for IInv /\ [Next]_vars using TLC.
-------------------------------------------------
>
> [...]
>
> Also,
> looked into BlockingQueue proof. It used SMT in its proof. I saw some
> other examples which used zenon, SMT both. I am new to using the proving
> system so do not understand when to use SMT or Zenon in the proof.
Hi Smurti,
to check IInv, you have to redefine the operator Seq with MySeq [1] in
the TLC model.
Removing the TLAPS pragmas [2] from the BlockingQueue proof shouldn't
make a difference, except that TLAPS will take slightly longer.
Markus
[1]
https://github.com/lemmy/BlockingQueue/commit/03fe04a9d63d0c92c77547bc10063e83e39a1878#diff-5877227013c88b4577157a9f744287c55b7ca75fa0401c21f49851bffb4f8affR71
[2]
https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Practical_hints.html