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