[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS



Hi Markus,
Thanks for pointing that out. I redefined Seq with MySeq. Now I am getting, a different error: 

-------------------------------------------

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.

Regarding removing the TLAPS pragmas from the  BlockingQueue proof, I am trying out the proof for the above simplified spec without pragmas.

Best,
Smruti
On Wednesday, November 4, 2020 at 11:13:14 PM UTC-6 Markus Alexander Kuppe wrote:
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

--
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/7039e237-bf47-4c72-9941-6edd25188ee8n%40googlegroups.com.