An issue about coverage information

40 views
Skip to first unread message

Xingchen Yi

unread,
Nov 6, 2018, 8:01:04 AM11/6/18
to tlaplus
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" in SendInt1 is

    Send == /\ x = NotInt
            /\ x' \in Int

In the module check result of the module, the coverage information of "x' = i" in the action PreSend(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

Markus Kuppe

unread,
Nov 6, 2018, 11:19:44 AM11/6/18
to tla...@googlegroups.com
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

Xingchen Yi

unread,
Nov 7, 2018, 6:29:19 AM11/7/18
to tlaplus
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写道:
Reply all
Reply to author
Forward
0 new messages