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

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

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/58556ffe-17ae-81f0-6c06-9261d4a85225%40lemmster.de.