#define N  6	/* The number of vertices */ 
#define NN 36	/* N^2 */
#define N1 15	/* 2 * N + 3 */
#define CELL_COUNT 300

typedef Compartment1 {
	int a = 0;
	int T = 0;
	int X[N1] = 0;
	int isDissolved;
	int isComputing;
}

typedef Compartment2 {
	int A[N] = 0;
	int Aij[NN] = 0;
	int B[N] = 0;
	int G[N] = 0;
	int R[N] = 0;
	int T[N] = 0;
	int X = 0;
	int S = 0;
	int Y = 0;
	int isDissolved = false;
	int isComputing = false;
	int createdAtStepNo = -1;
}

typedef Environment {
	int yes = 0;
	int no = 0;
}

int totalCell1Count;
Compartment1 c1Cells[CELL_COUNT];

int totalCell2Count;
Compartment2 c2Cells[CELL_COUNT];

Compartment1 c1PendingSymbols;

Environment environment;

int schedulerStep, schedulerFinished;


/* Verification variables */
int totalActiveC2Cells = 0;
int totalRedVertices = 0;
int totalGreenVertices = 0;
int totalBlueVertices = 0;
int Solutions = 0;
bool computationStepFinished;
bool isPsystemStep = false;

/* check if all rule executions have stopped for Compartment 1 */
inline isC1StepComplete(cellCount1) {
	int index;
	for(index: 0..cellCount1 - 1)  {
		c1Cells[index].isComputing == false;
	}
	index = 0;
}

inline isC2StepComplete(startIndex, endIndex) {
	int indexC2;
	for(indexC2: startIndex..endIndex)  {
		c2Cells[indexC2].isComputing == false;
	}
	indexC2 = 0;
}

/* apply membranes' rules for Compartment 1 */
inline computeC1Step(cellCount1) {
	int indexC1;
	for(indexC1: 0..cellCount1 - 1)  {
		if
		::	c1Cells[indexC1].isDissolved == false -> run C1(indexC1);
		::	else -> skip;
		fi;
	}
	indexC1 = 0;
}

int runningC2;

inline computeC2Step(startIndex, endIndex) {
	
	int indexC2;
	bool runningCondition;
	for(indexC2: startIndex..endIndex)  {
		
		if
		::	c2Cells[indexC2].isDissolved == false && c2Cells[indexC2].createdAtStepNo < schedulerStep
			&& c2Cells[indexC2].S >= 1 -> runningC2++; run C2(indexC2);
		::	else -> skip;
		fi;
	}
	indexC2 = 0;
	runningCondition = false;
}

inline computeTotalSCells() {
	d_step {
		totalSCells = 0;
		int indexC2;
		for(indexC2: 0..totalCell2Count - 1)  {
			if
			::	c2Cells[indexC2].isDissolved == false && c2Cells[indexC2].S >= 1 -> totalSCells++;
			::	else -> skip;
			fi;
		}
		indexC2 = 0;
	}
}

inline integrateCell(src, cell2Index) {
	int destCellIndex1, it1;
	destCellIndex1 = -1;
	
	for(it1:0..totalCell2Count - 1) {
		if
		::	c2Cells[it1].isDissolved && c2Cells[it1].isComputing == false  ->
			destCellIndex1 = it1;
			//cannot break at the first execution because this macro is intended to be
			//applied inside a d_step instruction, where jumping is not allowed
		::	else -> skip;
		fi;
	}

	if
	::	destCellIndex1 == -1 ->
		destCellIndex1 = totalCell2Count;
		totalCell2Count++;
	::	else -> skip;
	fi;
	
	c2Cells[destCellIndex1].createdAtStepNo = schedulerStep;
	c2Cells[destCellIndex1].isDissolved = false;
	c2Cells[destCellIndex1].isComputing = false;
	copyCell(src, c2Cells[destCellIndex1]);
}

inline copyCell(src, dest) {
	
	int elmIndex;
	for(elmIndex: 0..NN-1) {
		dest.Aij[elmIndex] = src.Aij[elmIndex];
	}

	for(elmIndex: 0..N-1) {
		dest.A[elmIndex] = src.A[elmIndex];
	}

	for(elmIndex: 0..N-1) {
		dest.B[elmIndex] = src.B[elmIndex];
	}

	for(elmIndex: 0..N-1) {
		dest.G[elmIndex] = src.G[elmIndex];
	}

	for(elmIndex: 0..N-1) {
		dest.R[elmIndex] = src.R[elmIndex];
	}
	
	for(elmIndex: 0..N-1) {
		dest.T[elmIndex] = src.T[elmIndex];
	}
	
	dest.X = src.X;
	dest.S = src.S;
	dest.Y = src.Y;

	elmIndex = 0;
}

/* transfer symbols to Compartment 1 */
inline transferToC1(from, to) {
	d_step {
		to.a = to.a + from.a;
		to.T = to.T + from.T;
	
		from.a = 0;
		from.T = 0;
	}
}

inline computeTotalActiveC2Cells() {
	d_step {
		totalActiveC2Cells = 0;
		int indexC2;
		for(indexC2: 0..totalCell2Count - 1)  {
			if
			::	c2Cells[indexC2].isDissolved == false -> totalActiveC2Cells++;
			::	else -> skip;
			fi;
		}
		indexC2 = 0;
	}
}

inline computeTotalRedVertices() {
	d_step {
		totalRedVertices = 0;
		int indexC2, ind;
		ind = 0;
		for(indexC2: 0..totalCell2Count - 1)  {
			if
			::	c2Cells[indexC2].isDissolved == false -> 
					for(ind: 0..N-1) {
						if
						::	c2Cells[indexC2].R[ind] >= 1 -> totalRedVertices++;
						::	else -> skip;
						fi;
					}
			::	else -> skip;
			fi;
		}
		indexC2 = 0;
	}
}

inline computeTotalGreenVertices() {
	d_step {
		totalGreenVertices = 0;
		int indexC2, ind;
		ind = 0;
		for(indexC2: 0..totalCell2Count - 1)  {
			if
			::	c2Cells[indexC2].isDissolved == false -> 
					for(ind: 0..N-1) {
						if
						::	c2Cells[indexC2].G[ind] >= 1 -> totalGreenVertices++;
						::	else -> skip;
						fi;
					}
			::	else -> skip;
			fi;
		}
		indexC2 = 0;
	}
}

inline computeTotalBlueVertices() {
	d_step {
		totalBlueVertices = 0;
		int indexC2, ind;
		ind = 0;
		for(indexC2: 0..totalCell2Count - 1)  {
			if
			::	c2Cells[indexC2].isDissolved == false -> 
					for(ind: 0..N-1) {
						if
						::	c2Cells[indexC2].B[ind] >= 1 -> totalBlueVertices++;
						::	else -> skip;
						fi;
					}
			::	else -> skip;
			fi;
		}
		indexC2 = 0;
	}
}

inline computeNoOfSolutions() {
	d_step {
		Solutions = 0;
		if
		::	environment.yes >= 1 -> 
			int arrIndex;
			for(arrIndex: 0..totalCell2Count-1) {
				if
				::	c2Cells[arrIndex].Y >= 1 && c2Cells[arrIndex].S >= 1 -> 
						Solutions++;
				::	else -> skip;
				fi;
			}
		::	else -> skip;
		fi;
	}
}

proctype Scheduler() {
	int currentCell1Count, currentCell2Count;
	do
	::	schedulerStep == N1 -> break;
		//environment.yes >= 1 || environment.no >= 1 -> break;
	::	else ->

		runningC2 = 0;
		currentCell1Count = totalCell1Count;
		currentCell2Count = totalCell2Count;
				
		computeC1Step(currentCell1Count);

		int chunkAmount, membraneStartIndex, chunkIndex;
		chunkAmount = 250;
		membraneStartIndex = -1;
		for(chunkIndex: 1..currentCell2Count/chunkAmount) {
			computeC2Step(membraneStartIndex + 1, chunkIndex * chunkAmount);
			isC2StepComplete(membraneStartIndex + 1, chunkIndex * chunkAmount);
			membraneStartIndex = chunkIndex * chunkAmount;
		}
		
		computeC2Step(membraneStartIndex + 1, currentCell2Count - 1);
		isC2StepComplete(membraneStartIndex + 1, currentCell2Count - 1);
		
		isC1StepComplete(currentCell1Count);
		
		transferToC1(c1PendingSymbols, c1Cells[0]);
		
		schedulerStep++;
		computeTotalActiveC2Cells();
		computeTotalRedVertices();
		computeTotalGreenVertices();
		computeTotalBlueVertices();
		computeNoOfSolutions();
		
		isPsystemStep = true;
		isPsystemStep = false;
		
		printf("Step: %d\n", schedulerStep);	
		printf("Total Active C2 Cells: %d\n", totalActiveC2Cells);
		printf("Total Red Vertices in all Cells: %d\n", totalRedVertices);
		printf("Total Green Vertices in all Cells: %d\n", totalGreenVertices);
		printf("Total Blue Vertices in all Cells: %d\n", totalBlueVertices);
		printf("Objects in C1: a: %d, T: %d\n", c1Cells[0].a, c1Cells[0].T); 
	od;
	
	printf("Computation Stops after %d Steps!\n", schedulerStep);
	schedulerFinished = true;
}

proctype C1(int cellIndex) {

	//printf("Started C1 process for compartment #%d\n", cellIndex);
	c1Cells[cellIndex].isComputing = true;
	int i;
	
	/* rewriting and communication rules */
	for(i: 0..N1-2) {
		if
		::	c1Cells[cellIndex].X[i] >= 1 -> 
				c1Cells[cellIndex].X[i]--; c1Cells[cellIndex].X[i+1]++; goto Wormhole;
		::	else -> skip;
		fi;
	}

	Wormhole:
	
	do
	::	c1Cells[cellIndex].a >= 1 && c1Cells[cellIndex].T >= 1->
			c1Cells[cellIndex].a--; c1Cells[cellIndex].T--; environment.yes++; 
			printf("C1: trasfer yes to the environment\n"); /* trasfer "yes" to the environment */
	::	c1Cells[cellIndex].a >= 1 && c1Cells[cellIndex].X[N1 -1] >= 1 && c1Cells[cellIndex].T == 0 -> 
			c1Cells[cellIndex].a--; c1Cells[cellIndex].X[N1 -1]--; environment.no++; 
			printf("C1: trasfer no to the environment\n"); /* transfer "no" to the environment */
	::	else -> break;
	od;
	
	c1Cells[cellIndex].isComputing = false;
	//printf("Finished C1 process for compartment #%d\n", cellIndex);
}

proctype C2(int cellIndex) {
	
	//printf("Started C2 process for compartment #%d\n", cellIndex);
	c2Cells[cellIndex].isComputing = true;
	int i, j;

	/* rewriting rules */
	if
	::	c2Cells[cellIndex].S >= 1 -> 
		for(i: 0..N-2) {
			for(j: i+1..N-1) {
				if
				::	 c2Cells[cellIndex].Aij[i*N + j] >= 1 && 
					(
					(c2Cells[cellIndex].B[i] >= 1 && c2Cells[cellIndex].B[j] >= 1) ||
					(c2Cells[cellIndex].G[i] >= 1 && c2Cells[cellIndex].G[j] >= 1) ||
					(c2Cells[cellIndex].R[i] >= 1 && c2Cells[cellIndex].R[j] >= 1) 
					)
					-> c2Cells[cellIndex].S--; /*c2Cells[cellIndex].isDissolved = true;*/ goto Wormhole;
				::	else -> skip;
				fi;
			}
		}
	::	else -> skip;
	fi;
	
	Wormhole:
	
	if
	::	c2Cells[cellIndex].X >= 1 -> c2Cells[cellIndex].X--; c2Cells[cellIndex].Y++;
	::	else -> skip;
	fi;
	
	/* communication rules */
	if
	::	c2Cells[cellIndex].Y >= 1 && c2Cells[cellIndex].S >= 1 ->
			/*Commented for Testing Purposes Only: c2Cells[cellIndex].Y--; */ 
			c1PendingSymbols.T++; /* trasfer T to compartment 1 */
	::	else -> skip;
	fi;
	
	/* membrane division rules */
	for(i: 0..N-2) {
		if
		::	c2Cells[cellIndex].S >= 1 && c2Cells[cellIndex].A[i] >= 1 ->
				c2Cells[cellIndex].A[i]--;
	
				Compartment2 divisionCells[2];
				d_step {
					copyCell(c2Cells[cellIndex], divisionCells[0]);
					copyCell(c2Cells[cellIndex], divisionCells[1]);
				}
			
				divisionCells[0].R[i]++; divisionCells[0].A[i+1]++;
				divisionCells[1].T[i]++;
		
				d_step {
					integrateCell(divisionCells[0], cellIndex)
					integrateCell(divisionCells[1], cellIndex);
				}
		
				c2Cells[cellIndex].isDissolved = true;	
		::	c2Cells[cellIndex].T[i] >= 1 ->
				c2Cells[cellIndex].T[i]--;
	
				d_step {
					copyCell(c2Cells[cellIndex], divisionCells[0]);
					copyCell(c2Cells[cellIndex], divisionCells[1]);
				}
			
				divisionCells[0].B[i]++; divisionCells[0].A[i+1]++;
				divisionCells[1].G[i]++; divisionCells[1].A[i+1]++;
		
				d_step {
					integrateCell(divisionCells[0], cellIndex)
					integrateCell(divisionCells[1], cellIndex);
				}
		
				c2Cells[cellIndex].isDissolved = true;
		::	else -> skip;
		fi;
	}
	
	if
	::	c2Cells[cellIndex].S >= 1 && c2Cells[cellIndex].A[N-1] >= 1 -> 
			c2Cells[cellIndex].A[N-1]--;
	
			Compartment2 divisionCells[2];
			d_step {
				copyCell(c2Cells[cellIndex], divisionCells[0]);
				copyCell(c2Cells[cellIndex], divisionCells[1]);
			}
		
			divisionCells[0].R[N-1]++; divisionCells[0].X++;
			divisionCells[1].T[N-1]++;
	
			d_step {
				integrateCell(divisionCells[0], cellIndex)
				integrateCell(divisionCells[1], cellIndex);
			}
	
			c2Cells[cellIndex].isDissolved = true;
	::	c2Cells[cellIndex].T[N-1] >= 1 -> 
			c2Cells[cellIndex].T[N-1]--;
	
			d_step {
				copyCell(c2Cells[cellIndex], divisionCells[0]);
				copyCell(c2Cells[cellIndex], divisionCells[1]);
			}
		
			divisionCells[0].B[N-1]++; divisionCells[0].X++;
			divisionCells[1].G[N-1]++; divisionCells[1].X++;
	
			d_step {
				integrateCell(divisionCells[0], cellIndex)
				integrateCell(divisionCells[1], cellIndex);
			}
	
			c2Cells[cellIndex].isDissolved = true;
	::	else -> skip;
	fi;
	
	c2Cells[cellIndex].isComputing = false;
	//printf("Finished C2 process for compartment #%d\n", cellIndex);
}

init {
	printf("Start Init Process\n");
	
	d_step	{
		/* build initial configuration for Compartment 1 */
		totalCell1Count = 1;
		c1Cells[0].a = 1;
		c1Cells[0].X[0] = 1;

		/* build initial configuration for Compartment 2 */
		totalCell2Count = 1;
		c2Cells[0].S = 1;
		c2Cells[0].A[0] = 1;
		
		/*
		N = 6, NN = 36, N1 = 15
		
             [0]  [5]---
                \/  |   |
           [1]-[4]-[2]  |
             \  |       |
               [3]------
		*/ 
		c2Cells[0].Aij[0*N + 4] = 1;
		c2Cells[0].Aij[1*N + 3] = 1;
		c2Cells[0].Aij[1*N + 4] = 1;
		c2Cells[0].Aij[2*N + 4] = 1;
		c2Cells[0].Aij[2*N + 5] = 1;
		c2Cells[0].Aij[3*N + 4] = 1;
		c2Cells[0].Aij[3*N + 5] = 1;
		c2Cells[0].Aij[4*N + 5] = 1;
	}
	
	printf("Finished building the initial configuration\n");
	
	run Scheduler();
	schedulerFinished;
	printf("scheduler Finished!");
	
	d_step {
		/*printf("\n\n\n");*/
		if
		::	environment.yes >= 1 -> printf("=== The problem has at least one solution! ===\n");
		::	environment.no >= 1 -> printf("=== The problem has no solution! ===\n");
		::	else -> printf("=== Something bad happened :( ! ===\n");
		fi;
	
		if
		::	environment.yes >= 1 -> 
			int arrIndex, innerArrIndex;
			Solutions = 0;
			for(arrIndex: 0..totalCell2Count-1) {
				if
				::	c2Cells[arrIndex].Y >= 1 && c2Cells[arrIndex].S >= 1 -> 
					printf("\n-------------------------------Solution at C2 cell #%d:------------------------------\n", arrIndex);
					Solutions++;
					printf("\nRed vertices: ");
					for(innerArrIndex: 0..N-1) {
						if
						::	c2Cells[arrIndex].R[innerArrIndex] >= 1 -> printf("%d, ", innerArrIndex);
						::	else ->	skip;
						fi;
					}
					printf("\nGreen vertices: ");
					for(innerArrIndex: 0..N-1) {
						if
						::	c2Cells[arrIndex].G[innerArrIndex] >= 1 -> printf("%d, ", innerArrIndex);
						::	else ->	skip;
						fi;
					}
					printf("\nBlue vertices: ");
					for(innerArrIndex: 0..N-1) {
						if
						::	c2Cells[arrIndex].B[innerArrIndex] >= 1 -> printf("%d, ", innerArrIndex);
						::	else ->	skip;
						fi;
					}
					printf("\n------------------------------------------------------------------------------------\n");
				::	else -> skip;
				fi;
			}
		::	else -> skip;
		fi;
	}
	
	printf("\n Total C2 cells count: %d \n", totalCell2Count);
	printf("\n The problem has %d solutions \n", Solutions);
}