Can someone please explain what this program generally does?

and especially, what is the connection between the array 'strarray' 
and value of 'rsult' upon termination?

Thanks :)

#define     MAXIMUM          6
#define MAXIMUMINDEX      MAXIMUM-1

bool rsult;
byte strarray[MAXIMUM];

proctype prducer( chan out )
{     int i;
     do
     :: (i <= MAXIMUMINDEX) -> out!strarray[i]; i++;
     :: (i > MAXIMUMINDEX) -> break;
     od;
}

proctype anonymous( chan in; chan out )
{     bit x,y;
     bool r;
     chan chld = [1] of { bit };
     chan c = [1] of { bool };

     out!1;
     if
     :: in?x -> out!1;
             run anonymous( chld, c );
             do
             :: in?y -> chld!y; c?r; out!(r && (x==y));
             :: timeout -> break;
             od
     :: timeout -> skip
     fi
}

proctype cnsumer ( chan in )
{      bool r;
     int i=0;
     do
     :: (i <= MAXIMUM) -> in?r; i++;
     :: (i > MAXIMUM) -> break;
     od;
     rsult = r;
}
     
init
{      
     /* array strarray */
     strarray[0] = 1;
     strarray[1] = 1;
     strarray[2] = 0;
     strarray[3] = 0;
     strarray[4] = 1;
     strarray[5] = 0;

     chan chld = [1] of { bit };
     chan c = [1] of { bool };

     run prducer(chld);
     run anonymous(chld, c);
     run cnsumer(c);
}

---

Request for Question Clarification by efn-ga on 18 Feb 2006 20:47 PST

In what language is the program written?  It looks like Promela, but
it would be helpful if you could confirm this.

---

Clarification of Question by pink_snickers-ga on 19 Feb 2006 00:05 PST

yes, it is Promela.
Sorry for forgetting to mention that and hope you can help out :)
Thanks