[tlaplus] An issue about coverage information

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 06.11.18 05:01, Xingchen Yi wrote:
> Hello,
> 
> Recently I'm learning prophecy variables in the paper "Auxiliary
> Variables in TLA+", and I check the module SendInt1P in the Section 4.1.
> 
> Part of the module is
> 
> ---------------------MODULE SendInt1P--------------------
> 
>     EXTENDS SendInt1, TLC
> 
>     Pi == Int 
> 
>     PreSend(i) == x' = i
> 
>     VARIABLE p
>  
>     varsP == <<x, p>>
> 
>     InitP ==  Init /\ (p \in Pi)
>  
>     TypeOKP == TypeOK  /\ (p \in Pi)
> 
>     SendP ==  Send /\ PredSend(p) /\ (p' \in Pi)
> 
>     RcvP == Rcv /\ (p' = p) 
> 
>     NextP == SendP \/ RcvP
> 
>     SpecP == InitP /\ [][NextP]_varsP
> 
> ----------------------------------------------------------------------------
> 
> And the action "Send" inSendInt1 is
> 
>     Send == /\ x = NotInt
>             /\ x' \in Int
> 
> In the module check result of the module, the coverage information of
> "x' = i" in the actionPreSend(i) is 0. 
> But actually I think this expression has been executed.
>  
> Expand the Action SendP,
>      
>     SendP == /\ x = NotInt
>              /\ x' \in Int
>              /\ x' = p
>              /\ p' \in Pi
> 
> The coverage information of the second is non-zero, the coverage
> information of "x' = p" should also be non-zero.
>    
> How can I solve the issue?
> 
> Best regards,
> Xingchen Yi

Hi Xingchen,

what you describe appears to be another variant of
https://github.com/tlaplus/tlaplus/issues/92. We plan to fix #92 with
the next TLC/Toolbox release.

Thanks
Markus