Notice that the elapsed time increases linearly over time so it is a continuous variable whose time derivative is constant 1. However, the lifetime is not changing continuously but it is determined discretely at the time of executing either or .
In other word, suppose that there is at time , there is another at time and . If there is no event between and , it implies that the only difference between and is that their elapsed time such that .
Formally we can rewrite this player as
where
={?receive
};
={!send
};
={Send
,
Wait
};
=Send
;
(Send
)
[0.1,
1.2],
(Wait
)=
;
(Send
,
,[0,
],?receive
)
=(Send
,1),
(Send
,[0.1,
1.2],[0,
],?receive
)=(Send
,0);
(Send
)=(!send
,Wait
);