Dear Lyle,
I finally got some time to look at the semantics of the Erlang receive
when the time-out is zero (pg. 394), and I think you are right. The
book's translation only checks for the first message in the mailbox. I
think it is a case of overzealous simplification.
As I see it now, we can do just one simplification. We can prove that:
Cancel={Alarm 0}
{WaitTwo S Cancel}==1 % Assume WaitTwo favors the first argument
is equivalent to:
{IsDet S}
This gives the following semantics for the receive:
T(receive ... end Sin Sout) ==
local
fun {Loop S T#E Sout}
if {IsDet S} then
case S of M|S1 then
case M
of T(Pattern1) then E=S1 T(Body1 T Sout)
…
[] T(PatternN) then E=S1 T(BodyN T Sout)
else E1 in E=M|E1 {Loop S1 T#E1 Sout} end
end
else E=S T(BodyT T Sout) end
end T
in
{Loop Sin T#T Sout}
end
The translation in Fig. 5.23 is wrong since it only looks at the first
message to see whether it matches. We need the loop since the message
removed from the mailbox is not necessarily the first. Thanks much for
finding this mistake!
Peter
_________________________________________________________________________________
mozart-users mailing list
[email protected]
http://www.mozart-oz.org/mailman/listinfo/mozart-users
