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 total_max = 100; //maximum number of vehicles that can pass through the system
byte n = 10; //maximum number of vehicles simultaneously in the system
byte total_counter_v = 0; //total counter of vehicles

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

proctype RoadsideUnit () {
	do // update sem1 , sem2 and sem3 according to s0 , s1 , s2 and s3
	:: 1 == 1 ->
		printf("TOTAL_MAX %d\n",total_counter_v);
		printf("sem1 %e sem2 %e sem3 %e\n",sem1,sem2,sem3);
		printf("s0 %d s1 %d s2 %d s3 %d\n",s0,s1,s2,s3);
		printf("countZ0 %d countZ1 %d countZ2 %d countZ3 %d\n",countZ0,countZ1,countZ2,countZ3);
	:: 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;
	:: total_counter_v >= total_max -> break;
	od;
}

proctype Vehicles () {
	do // non - deterministically move vehicles through zones Z0 , Z1 , Z2 , and Z3
	:: (countZ0 + countZ1 + countZ2 + countZ3) < n ->		// handle arrivals - can any car arrive?
		printf("---1 soma: %d\n", (countZ0 + countZ1 + countZ2 + countZ3));
		atomic{
		printf("############ATOMIC#########\n");
		if
		:: countZ1++ ->
			total_counter_v++;
		:: countZ2++ ->
			total_counter_v++;
		:: countZ3++ ->
			total_counter_v++;
		fi;
		}
	:: (countZ0 + countZ1 + countZ2 + countZ3) > 0 ->
		printf("---2 soma: %d\n", (countZ0 + countZ1 + countZ2 + countZ3));

		if //handle zone departures
		:: s0 ->
			printf("---teste s0 CountZ0 %d\n", countZ0);
			atomic{countZ0--;}
		:: s1 ->
			printf("---teste s1 sem1 %e\n",sem1);
			if
			:: sem1 == green ->
				atomic{countZ1--; countZ0++;}
			fi;
		:: s2 ->
			printf("---teste s2 sem2 %e\n",sem2);
			if
			:: sem2 == green ->
				atomic{countZ2--; countZ0++;}
			fi;
		:: s3 ->
			printf("---teste s3 sem3 %e\n",sem3);
			if
			:: sem3 == green ->
				atomic{countZ3--; countZ0++;}
			fi;
		fi;
	:: total_counter_v >= total_max -> break;
	:: else -> printf("TESTE ELSE\n");
	od ;
}

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