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

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.



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.