badabadabada

mtype = { red , green }
mtype sem1 = red , sem2 = red , sem3 = red ; // three semaphores
bool s0 , s1 , s2 , s3 ; // four presence sensors
byte countZ0 , countZ1 , countZ2 , countZ3 ; // count the vehicles in each zone
byte n = 5; //maximum number of vehicles
byte total_v = 0; //counter of vehicles

proctype Sensors () {
do
	:: s0 = ( countZ0 > 0)
	:: s1 = ( countZ1 > 0)
	:: s2 = ( countZ2 > 0)
	:: s3 = ( countZ3 > 0)
od ;
}

proctype RoadsideUnit () {
	do // update sem1 , sem2 and sem3 according to s0 , s1 , s2 and s3
	:: s0 -> skip;
	:: !s0 && (sem1 == red && sem2 == red && sem3 == red) && (s1 || s2 || s3) -> //all sem are red
		if
		:: s1 && !s2 && !s3 -> sem1 = green;
		:: !s1 && s2 && !s3 -> sem2 = green;
		:: !s1 && !s2 && s3 -> sem3 = green;
		:: s1 && s2 && !s3 -> sem1 = green;
		:: s1 && !s2 && s3 -> sem1 = green;
		:: !s1 && s2 && s3 -> sem2 = green;
		:: else -> skip;
		fi;
	:: !s0 && sem1 == green && !s1  -> //sem1 is green with no cars:
		sem1 = red;
	:: !s0 && sem2 == green && !s2  -> //sem2 is green with no cars:
		sem2 = red;
	:: !s0 && sem3 == green && !s3  -> //sem3 is green with no cars:
		sem3 = red;
	:: else -> skip;
	od;
}

proctype Vehicles () {
	byte temp_v, temp_dif, temp_zone, do_counter;
	byte max_v = 3; //maximum number of vehicles that can arrive/depart at a time
	do // non - deterministically move vehicles through zones Z0 , Z1 , Z2 , and Z3
	:: total_v < n ->		// handle arrivals
		temp_zone = 0;
		temp_dif = n - total_v;
		if
		:: max_v < temp_dif ->
			select(temp_v : 0..max_v); // how many vehicles arrive
		:: else ->
			select(temp_v : 0..temp_dif); // how many vehicles arrive
		fi;
		total_v = total_v + temp_v;

		do_counter = 0;
		do
		:: temp_v > 0 ->
			select(temp_zone : 0..temp_v);  // temp_zone saves the amount of cars that will arrive in a zone
			if
			:: do_counter == 0 ->
				countZ1 = countZ1+temp_zone;
			:: do_counter == 1 ->
				countZ2 = countZ2+temp_zone;
			:: do_counter == 2 ->
				countZ3 = countZ3+temp_zone;
			:: else -> skip;
			fi;

			temp_v = temp_v - temp_zone;
			do_counter++;
		:: else -> skip;
		od;
	//handle zone departures
	:: s0 ->
		countZ0 = countZ0 - max_v;
		if
		:: countZ0 < 0 ->
			countZ0 = 0;
		fi;
	:: s1 ->
		if
		:: sem1 == green && countZ1 > max_v ->
			countZ1 = countZ1 - max_v;
			countZ0 = countZ0 + max_v;
		:: sem1 == green && countZ1 <= max_v ->
			countZ0 = countZ0 + countZ1;
			countZ1 = 0;
		:: else -> skip;
		fi;
	:: s2 ->
		if
		:: sem2 == green && countZ2 > max_v ->
			countZ2 = countZ2 - max_v;
			countZ0 = countZ0 + max_v;
		:: sem2 == green && countZ2 <= max_v ->
			countZ0 = countZ0 + countZ1;
			countZ2 = 0;
		:: else -> skip;
		fi;
	:: s3 ->
		if
		:: sem3 == green && countZ3 > max_v ->
			countZ3 = countZ3 - max_v;
			countZ0 = countZ0 + max_v;
		:: sem3 == green && countZ3 <= max_v ->
			countZ0 = countZ0 + countZ3;
			countZ3 = 0;
		:: else -> skip;
		fi;
	:: else ->
		temp_v = 0;
	od ;
}

init {
	run Sensors ();
	run RoadsideUnit ();
	run Vehicles ();
}