/****************************************************************
* File :        system2.prom                                    *
* Author:       Gang Liu                                        *
* Date:         April 04, 1999                                  *
* Note:         Model of the traffic control system (revised)   *
****************************************************************/

/* This is the two pedestrians, two intersections version */
/* define the states of the PedestrianLight that may
   waiting for the RoadLight */
#define idle            0 
#define waitPLight      1 

/* direction */
#define E		2  
#define W	        3       
#define N 	        4
#define S	        5

/* States of TrafficLight and PedestrianLight */
#define red             6
#define green           7
#define white           8   

/* States of Button */
#define ButtonOn        9
#define ButtonOff       10

/* define the states of the Pedestrian who may
waiting for the RoadLight */   
#define waitPLight1     19
#define waitPLight2     20

/* Buttons, PedestrianLights and RoadLights positions */
typedef array {
        byte    direction[11]
};
array   pLight[3];
array   pButton[3];

byte    rLight[3];

/* channels  */
typedef channel {
	chan	pedes[3] = [1] of {byte, byte, byte}
};
channel ch[3];


proctype RoadLight(byte pid) {
do
:: rLight[pid] == green -> 
	atomic {rLight[pid] = red;
		pLight[pid].direction[E] = red;
		pLight[pid].direction[W] = red;
	}
:: rLight[pid] == red ->                         
        atomic {rLight[pid] = green;
                pLight[pid].direction[E] = red;
                pLight[pid].direction[W] = red;
	}
:: true -> skip
od
}

proctype Pedestrian(int ped) {
byte state, where, condi;

atomic { state = idle;
        }
end:
do
:: state == idle -> state = idle

:: state == idle -> atomic { pButton[1].direction[E] = ButtonOn;
                        state = waitPLight1;
                        ch[1].pedes[ped] ! E, ped, ButtonOn;
                        }
:: state == idle -> atomic { pButton[1].direction[W] = ButtonOn;
                        state = waitPLight1;
                        ch[1].pedes[ped] ! W, ped, ButtonOn;
                        }
:: state == idle -> atomic { pButton[1].direction[N] = ButtonOn;
                        state = waitPLight1;
                        ch[1].pedes[ped] ! N, ped, ButtonOn;
                        }
:: state == idle -> atomic { pButton[1].direction[S] = ButtonOn;
                        state = waitPLight1;
                        ch[1].pedes[ped] ! S, ped, ButtonOn;
                        }

:: state == idle -> atomic { pButton[2].direction[E] = ButtonOn;
                        state = waitPLight2;
                        ch[2].pedes[ped] ! E, ped, ButtonOn;
                        }
:: state == idle -> atomic { pButton[2].direction[W] = ButtonOn;
                        state = waitPLight2;
                        ch[2].pedes[ped] ! W, ped, ButtonOn;
                        }
:: state == idle -> atomic { pButton[2].direction[N] = ButtonOn;
                        state = waitPLight2;
                        ch[2].pedes[ped] ! N, ped, ButtonOn;
                        }
:: state == idle -> atomic { pButton[2].direction[S] = ButtonOn;
                        state = waitPLight2;
                        ch[2].pedes[ped] ! S, ped, ButtonOn;
                        }


:: state == waitPLight1 && ch[1].pedes[ped] ? [where, ped, white] ->
                atomic { ch[1].pedes[ped] ? where, ped, white;
                        pLight[1].direction[where] = white;
                        state = idle;
                        pButton[1].direction[where] = ButtonOff;
                        }

:: state == waitPLight2 && ch[2].pedes[ped] ? [where, ped, white] ->
                atomic { ch[2].pedes[ped] ? where, ped, white;
                        pLight[2].direction[where] = white;
                        state = idle;
                        pButton[2].direction[where] = ButtonOff;
                        }

od;
}

proctype PedestrianLight(byte pid, pid2, ped, ped2) {
byte state, where, condi;
 
atomic { state = idle;
        }
end:
        
do
:: rLight[pid] == red ->
	atomic {
		if 
		:: ch[pid].pedes[ped] ? [E, ped, ButtonOn] ->
			ch[pid].pedes[ped] ? where, ped, condi;
			ch[pid].pedes[ped] ! 	 E, ped, white;
			pLight[pid].direction[E] = white;
			state = idle
		:: else
		fi;
		if
		:: ch[pid].pedes[ped] ? [W, ped, ButtonOn] ->
			ch[pid].pedes[ped] ? where, ped, condi;
			ch[pid].pedes[ped] ! 	 W, ped, white;
			pLight[pid].direction[W] = white;
			state = idle
		:: else
		fi;
                if
                :: ch[pid].pedes[ped2] ? [E, ped2, ButtonOn] ->
                        ch[pid].pedes[ped2] ? where, ped2, condi;
                        ch[pid].pedes[ped2] ! 	  E, ped2, white;
                        pLight[pid].direction[E] = white;
                        state = idle
                :: else
                fi;
                if
                :: ch[pid].pedes[ped2] ? [W, ped2, ButtonOn] ->
                        ch[pid].pedes[ped2] ? where, ped2, condi;
                        ch[pid].pedes[ped2] ! 	  W, ped2, white;
                        pLight[pid].direction[W] = white;
                        state = idle
                :: else
                fi;             
        
                }
:: rLight[pid] == red && rLight[pid2] == green ->
		state = waitPLight
:: rLight[pid2] == red && rLight[pid] == green ->
		state = waitPLight

:: rLight[pid] == red && rLight[pid2] == green ->
	atomic {if
		:: ch[pid].pedes[ped] ? [N, ped, ButtonOn] ->
			ch[pid].pedes[ped] ? where, ped, condi;
			ch[pid].pedes[ped] !     N, ped, white;
			pLight[pid].direction[N] = white;
			state = idle
		:: else
		fi;
		if
                :: ch[pid].pedes[ped] ? [S, ped, ButtonOn] ->
                        ch[pid].pedes[ped] ? where, ped, condi;
                        ch[pid].pedes[ped] !     S, ped, white;
                        pLight[pid].direction[S] = white;
                        state = idle
                :: else
                fi;
                if
                :: ch[pid].pedes[ped2] ? [N, ped2, ButtonOn] ->
                        ch[pid].pedes[ped2] ? where, ped2, condi;
                        ch[pid].pedes[ped2] !     N, ped2, white;
                        pLight[pid].direction[N] = white;
                        state = idle
                :: else
                fi;
                if 
                :: ch[pid].pedes[ped2] ? [S, ped2, ButtonOn] ->
                        ch[pid].pedes[ped2] ? where, ped2, condi;
                        ch[pid].pedes[ped2] !     S, ped2, white;
                        pLight[pid].direction[S] = white;
                        state = idle
                :: else
                fi;
                   
                }
                        
od                      
}                      

init{
	atomic {int i = 0; int j = 0;
		do
		:: i <=1 -> j = 0; i++;
			do
			:: j <= 10 -> 	
				pLight[i].direction[j] = red;
				pButton[i].direction[j] = ButtonOff;
				j++;
			:: else -> break
			od;
			rLight[i] = green;
		::else -> break
		od;
	}

	atomic {run RoadLight(1);
		run RoadLight(2);

        	run Pedestrian(1);
        	run Pedestrian(2);

	        run PedestrianLight(1, 2, 1, 2);
		run PedestrianLight(2, 1, 1, 2);
	}
}