## Software from the book "Inferno Programming with Limbo"# published by John Wiley & Sons, January 2003.## p. Stanley-Marbell <pip@gemusehaken.org>#implement PromelaLimbo; include "sys.m";include "draw.m"; PromelaLimbo : module{ init : fn(nil : ref Draw->Context, nil : list of string);}; sys : Sys; NUMCHANS : con 6;NUMSLAVES : con 5;SAMPLEDCHAN : con 5;SAMPLE, SAMPLED : con 1 << iota; # Synchronous Communication Medium:netseg := array [NUMCHANS] of chan of int; slave(my_id : int){ got_sample := 0; sys->print("Node %d startup\n", my_id); while () alt { # Wait for message type 'SAMPLE' msg := <-netseg[my_id] => { if (msg == SAMPLE) got_sample = 1; } * => { if (got_sample) { # Send a 'SAMPLED' message netseg[SAMPLEDCHAN] <-= SAMPLED; got_sample = 0; } } }} master(){ nreceipts, nsent, nperiods : int = 0; sys->print("Master started up\n"); while () alt { * => if ((nreceipts % NUMSLAVES) == 0) { nreceipts = 0; nsent = 0; while () { if (nsent < NUMSLAVES) { netseg[nsent] <-= SAMPLE; nsent++; } if (nsent == NUMSLAVES) { nperiods++; break; } } } msg := <-netseg[SAMPLEDCHAN] => { if (msg == SAMPLED) nreceipts++; } }} # Initial process creates processesinit (nil : ref Draw->Context, nil : list of string){ sys = load Sys Sys->PATH; for (i := 0; i <= SAMPLEDCHAN; i++) { netseg[i] = chan of int; } spawn slave(0); spawn slave(1); spawn slave(2); spawn slave(3); spawn slave(4); spawn master();}
#
# Software from the book "Inferno Programming with Limbo"
# published by John Wiley & Sons, January 2003.
#
# p. Stanley-Marbell <pip@gemusehaken.org>
#
implement PromelaLimbo;
include "sys.m";
include "draw.m";
PromelaLimbo : module
{
init : fn(nil : ref Draw->Context, nil : list of string);
};
sys : Sys;
NUMCHANS : con 6;
NUMSLAVES : con 5;
SAMPLEDCHAN : con 5;
SAMPLE, SAMPLED : con 1 << iota;
# Synchronous Communication Medium:
netseg := array [NUMCHANS] of chan of int;
slave(my_id : int)
{
got_sample := 0;
sys->print("Node %d startup\n", my_id);
while ()
alt
{
# Wait for message type 'SAMPLE'
msg := <-netseg[my_id] =>
{
if (msg == SAMPLE)
got_sample = 1;
}
* =>
{
if (got_sample)
{
# Send a 'SAMPLED' message
netseg[SAMPLEDCHAN] <-= SAMPLED;
got_sample = 0;
}
}
}
}
master()
{
nreceipts, nsent, nperiods : int = 0;
sys->print("Master started up\n");
while ()
alt
{
* =>
if ((nreceipts % NUMSLAVES) == 0)
{
nreceipts = 0;
nsent = 0;
while ()
{
if (nsent < NUMSLAVES)
{
netseg[nsent] <-= SAMPLE;
nsent++;
}
if (nsent == NUMSLAVES)
{
nperiods++;
break;
}
}
}
msg := <-netseg[SAMPLEDCHAN] =>
{
if (msg == SAMPLED)
nreceipts++;
}
}
}
# Initial process creates processes
init (nil : ref Draw->Context, nil : list of string)
{
sys = load Sys Sys->PATH;
for (i := 0; i <= SAMPLEDCHAN; i++)
{
netseg[i] = chan of int;
}
spawn slave(0);
spawn slave(1);
spawn slave(2);
spawn slave(3);
spawn slave(4);
spawn master();
}