[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

An issue about coverage information


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

    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