Hi, Markus,
Thanks for your reply, I hope you can solve the issue soon.
Thanks
在 2018年11月7日星期三 UTC+8上午12:19:44，Markus Alexander Kuppe写道：
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