Promela SPIN example, http://spinroot.com/spin/Doc/SpinTutorial.pdf

abp0.pr

mtype {MSG, ACK};

chan toS = [2] of {mtype, bit};
chan toR = [2] of {mtype, bit};

proctype Sender(chan inp, out)
{
	bit sendbit, recvbit;
	do
	:: out ! MSG, sendbit ->
		inp ? ACK, recvbit;
		if
		:: recvbit == sendbit ->
			sendbit = 1-sendbit
		:: else
		fi
	od
}

proctype Receiver(chan inp, out)
{
	bit recvbit;
	do
	:: inp ? MSG(recvbit) ->
		out ! ACK(recvbit);
	od
}

init
{
	run Sender(toS, toR);
	run Receiver(toR, toS);
}

do.pr

mtype = { RED, YELLOW, GREEN } ; /* mtype (message type) models enumerations in Promela */
active proctype TrafficLight() {
	byte state = GREEN;
	do
	:: (state == GREEN) -> state = YELLOW;
	:: (state == YELLOW) -> state = RED;
	:: (state == RED) -> state = GREEN;
	od;
}

/* run on ispin and view automata view */

hello.pr

active proctype Hello() {
	printf("Hello process, my pid is: %d\n", _pid);
}
init {
	int lastpid;
	printf("init process, my pid is: %d\n", _pid);
	lastpid = run Hello();
	printf("last pid was: %d\n", lastpid);
}

muex1.pr

bit flag; /* signal entering/leaving the section */
byte mutex; /* # procs in the critical section. */
proctype P(bit i) {
	flag != 1;
	flag = 1;
	mutex++;
	printf("MSC: P(%d) has entered section.\n", i);
	mutex--;
	flag = 0;
}
proctype monitor() {
	assert(mutex != 2);
}
init {
	atomic { run P(0); run P(1); run monitor(); }
}

muex2.pr

bit x, y; /* signal entering/leaving the section */
byte mutex; /* # of procs in the critical section. */
active proctype A() {
	x = 1;
	y == 0;
	mutex++;
	printf("MSC: P(A) has entered section.\n");
	mutex--;
	x = 0;
}
active proctype B() {
	y = 1;
	x == 0;
	mutex++;
	printf("MSC: P(B) has entered section.\n");
	mutex--;
	y = 0;
}
active proctype monitor() {
	assert(mutex != 2);
}

muex3.pr

bit x, y; /* signal entering/leaving the section */
byte mutex; /* # of procs in the critical section. */
byte turn; /* who's turn is it? */
#define A_TURN 0
#define B_TURN 1
active proctype A() {
	x = 1;
	turn = B_TURN;
	y == 0 ||
	  (turn == A_TURN);
	mutex++;
	printf("MSC: P(A) has entered section.\n");
	mutex--;
	x = 0;
}

active proctype B() {
	y = 1;
	turn = A_TURN;
	x == 0 ||
	  (turn == B_TURN);
	mutex++;
	printf("MSC: P(B) has entered section.\n");
	mutex--;
	y = 0;
}

active proctype monitor() {
	assert(mutex != 2);
}

muex4.pr

byte turn[2]; /* who’s turn is it? */
byte mutex; /* # procs in critical section */
proctype P(bit i) {
	do
	:: turn[i] = 1;
	   turn[i] = turn[1-i] + 1;
	   (turn[1-i] == 0) || (turn[i] < turn[1-i]);
	   mutex++;
	   printf("MSC: P(%d) has entered section.\n", i);
	   mutex--;
	   turn[i] = 0;
	od;
}
proctype monitor() { assert(mutex != 2); }
init { atomic {run P(0); run P(1); run monitor() } }

/* run on ispin and view automata view */

please provide the explanation/working of "do.pr" program i-e traffic light. And can you provide us any other example of promela code with complete explanation of complete process.