/* Mandatory boundary constants */
#define MaxInstances 2050
//#define MaxLinks 10000 //always MaxInstances^2
#define MaxSteps 13

/* Other model specific constants if required */

/* constants denoting the execution state of a p system - use the step_complete in verification formulae */
mtype = {running, step_complete}
mtype state = running;

/* The alphabet */
//mapping of symbols to integers so we can use arrays as maps with these as keys instead
#define @F 0
#define @no 1
#define @v_9 2
#define @v_3 3
#define @T 4
#define @v_4 5
#define @v_1 6
#define @v_2 7
#define @B_1 8
#define @v_7 9
#define @v_8 10
#define @B_2 11
#define @S 12
#define @v_5 13
#define @B_3 14
#define @B_4 15
#define @v_6 16
#define @B_5 17
#define @B_6 18
#define @B_7 19
#define @B_8 20
#define @B_9 21
#define @Y 22
#define @X 23
#define @A_10 24
#define @yes 25
#define @A_9 26
#define @A_8 27
#define @v 28
#define @A_7 29
#define @B_10 30
#define @A_6 31
#define @A_1 32
#define @A_5 33
#define @A_4 34
#define @A_3 35
#define @v_10 36
#define @A_2 37
#define A_LENGTH 38

int step = 0;
int instanceCount = 0;
//int linksCount = 0;

typedef MInstance {
	byte type;
	int x[A_LENGTH] = 0;
	int x_temp[A_LENGTH] = 0;
	byte isComputing = false;
	byte isDissolved = false;
}

/* A link between the indices corresponding to the membrane instances in the membrane instance array
typedef MLink {
	int m1Index;
	int m2Index;
}
*/

/* Membrane instances */
MInstance ms[MaxInstances];

/* Membrane links 
MLink ml[MaxLinks];
*/

/* For each instance we have:
	- x, the vector of symbols from the alphabet
	- n is the value (multiplicity) associated with each object
*/

/* Verification variables */
bool isPsystemStep = false;

/* Verification properties */
ltl p1 { ((ms[2].x[@yes] == 0 && ms[2].x[@no] == 0) || !isPsystemStep) U (ms[2].x[@yes] == 1 && ms[2].x[@no] == 0 && isPsystemStep) }

inline printInstanceData(instanceIndex) {
  skip;
	d_step {
		printf("\nStep: %d Instance #: %d", step, instanceIndex);

		if 
		::  ms[instanceIndex].type == 0 -> printf("type: 2");
		::  ms[instanceIndex].type == 1 -> printf("type: 1");
		::  ms[instanceIndex].type == 2 -> printf("type: 0");

		::  else -> skip;
		fi;

		if 
		::	ms[instanceIndex].x[@F] >= 1 -> printf("F:%d,", ms[instanceIndex].x[@F]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@no] >= 1 -> printf("no:%d,", ms[instanceIndex].x[@no]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_9] >= 1 -> printf("v_9:%d,", ms[instanceIndex].x[@v_9]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_3] >= 1 -> printf("v_3:%d,", ms[instanceIndex].x[@v_3]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@T] >= 1 -> printf("T:%d,", ms[instanceIndex].x[@T]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_4] >= 1 -> printf("v_4:%d,", ms[instanceIndex].x[@v_4]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_1] >= 1 -> printf("v_1:%d,", ms[instanceIndex].x[@v_1]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_2] >= 1 -> printf("v_2:%d,", ms[instanceIndex].x[@v_2]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_1] >= 1 -> printf("B_1:%d,", ms[instanceIndex].x[@B_1]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_7] >= 1 -> printf("v_7:%d,", ms[instanceIndex].x[@v_7]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_8] >= 1 -> printf("v_8:%d,", ms[instanceIndex].x[@v_8]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_2] >= 1 -> printf("B_2:%d,", ms[instanceIndex].x[@B_2]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@S] >= 1 -> printf("S:%d,", ms[instanceIndex].x[@S]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_5] >= 1 -> printf("v_5:%d,", ms[instanceIndex].x[@v_5]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_3] >= 1 -> printf("B_3:%d,", ms[instanceIndex].x[@B_3]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_4] >= 1 -> printf("B_4:%d,", ms[instanceIndex].x[@B_4]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_6] >= 1 -> printf("v_6:%d,", ms[instanceIndex].x[@v_6]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_5] >= 1 -> printf("B_5:%d,", ms[instanceIndex].x[@B_5]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_6] >= 1 -> printf("B_6:%d,", ms[instanceIndex].x[@B_6]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_7] >= 1 -> printf("B_7:%d,", ms[instanceIndex].x[@B_7]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_8] >= 1 -> printf("B_8:%d,", ms[instanceIndex].x[@B_8]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_9] >= 1 -> printf("B_9:%d,", ms[instanceIndex].x[@B_9]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@Y] >= 1 -> printf("Y:%d,", ms[instanceIndex].x[@Y]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@X] >= 1 -> printf("X:%d,", ms[instanceIndex].x[@X]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_10] >= 1 -> printf("A_10:%d,", ms[instanceIndex].x[@A_10]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@yes] >= 1 -> printf("yes:%d,", ms[instanceIndex].x[@yes]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_9] >= 1 -> printf("A_9:%d,", ms[instanceIndex].x[@A_9]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_8] >= 1 -> printf("A_8:%d,", ms[instanceIndex].x[@A_8]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v] >= 1 -> printf("v:%d,", ms[instanceIndex].x[@v]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_7] >= 1 -> printf("A_7:%d,", ms[instanceIndex].x[@A_7]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@B_10] >= 1 -> printf("B_10:%d,", ms[instanceIndex].x[@B_10]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_6] >= 1 -> printf("A_6:%d,", ms[instanceIndex].x[@A_6]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_1] >= 1 -> printf("A_1:%d,", ms[instanceIndex].x[@A_1]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_5] >= 1 -> printf("A_5:%d,", ms[instanceIndex].x[@A_5]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_4] >= 1 -> printf("A_4:%d,", ms[instanceIndex].x[@A_4]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_3] >= 1 -> printf("A_3:%d,", ms[instanceIndex].x[@A_3]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@v_10] >= 1 -> printf("v_10:%d,", ms[instanceIndex].x[@v_10]);
		::	else -> skip;
		fi;
		if 
		::	ms[instanceIndex].x[@A_2] >= 1 -> printf("A_2:%d,", ms[instanceIndex].x[@A_2]);
		::	else -> skip;
		fi;

		skip;
	}
}

proctype Log(int instanceIndex) {
  skip;
	d_step {
		/*printf("--------- configuration #%d ----------\n\n", step);*/
		int i;
		if
			:: instanceIndex >= 0 && instanceIndex < instanceCount -> printInstanceData(instanceIndex);
			:: instanceIndex == -1 ->
				for(i: 0 .. instanceCount - 1) {
					if
					::	ms[i].isDissolved == false ->
						printInstanceData(i);
					::	else -> skip;
					fi;	
				}
			:: else -> skip;
		fi;
		/*printf("\n------------------------------------\n\n");*/
		skip;
	}
}

/* Executes a rewrite operation for instance denoted by index "instanceIndex" 
 * Object communication is considered as a rewrite operation across compartments
 * OBSOLETE!!!
 */
inline doRewrite(src_instanceIndex, tar_instanceIndex, symbol1, n1, symbol2, n2) {
	ms[src_instanceIndex].x[symbol1] = ms[src_instanceIndex].x[symbol1] - n1;
	ms[tar_instanceIndex].x_temp[symbol2] = ms[tar_instanceIndex].x_temp[symbol2] + n2;
	skip;
}

inline doLhs(instanceIndex, symbol, n) {
	ms[instanceIndex].x[symbol] = ms[instanceIndex].x[symbol] - n;
}

inline doRhs(instanceIndex, symbol, n) {
	ms[instanceIndex].x_temp[symbol] = ms[instanceIndex].x_temp[symbol] + n;
}

inline doReplicate(tar_type, symbol, n) {
	int i;
	for(i: 0 .. instanceCount - 1) {
		if
			:: ms[i].type == tar_type -> doRhs(i, symbol, n);
			:: else -> skip;
		fi;

	}
}

inline create(instanceIndex, tar_type, childCount) {
	int i, j, k;
	for(i: 0 .. childCount - 1) {
		ms[instanceCount].type = tar_type;
		for(j: 0 .. A_LENGTH - 1) {
			ms[instanceCount].x[j] = ms[instanceIndex].x[j];
		}

		//all the links subject to the parent membrane are now inherited by the created membranes
		/*
		for(k: 0 .. linksCount - 1) {
			if
				:: ml[k].m1Index == instanceIndex || ml[k].m2Index == instanceIndex -> 
					ml[linksCount].m1Index = instanceCount; ml[linksCount].m2Index = k; linksCount++; 
				:: else -> skip;
			fi;
		}
		*/
		instanceCount++;
	}
}

inline divide(instanceIndex, childCount) {
	//the first membrane remains unchanged in the division process
	//additional rewriting should be done using the rewrite procedure after the division
	//for rules which do division and rewriting in one step
	int i, j, k;
	for(i: 0 .. childCount - 1) {
		ms[instanceCount].type = ms[instanceIndex].type;
		for(j: 0 .. A_LENGTH - 1) {
			ms[instanceCount].x[j] = ms[instanceIndex].x[j];
		}

		//all the links subject to the parent membrane are now inherited by the created membranes
		/*
		for(k: 0 .. linksCount - 1) {
			if
				:: ml[k].m1Index == instanceIndex || ml[k].m2Index == instanceIndex -> 
					ml[linksCount].m1Index = instanceCount; ml[linksCount].m2Index = k; linksCount++; 
				:: else -> skip;
			fi;
		}
		*/
		instanceCount++;
	}
}

inline doDissolve(instanceIndex) {
	//mark the membrane instance located at instanceIndex as dissolved
	ms[instanceIndex].isDissolved = true;
}

inline applyRulesForMembranesInRange(startInstanceIndex, endInstanceIndex) {
  int instIndex;
  for(instIndex : startInstanceIndex .. endInstanceIndex) {
    if
    :: (ms[instIndex].isDissolved == false && ms[instIndex].type == 0) -> run M0(instIndex);
    :: (ms[instIndex].isDissolved == false && ms[instIndex].type == 1) -> run M1(instIndex);
    	:: else -> skip;
    fi;
  }
  instIndex = 0;
}

inline rulesApplied(startInstanceIndex, endInstanceIndex) {
  int instIndex;
  for(instIndex: startInstanceIndex .. endInstanceIndex) {
    ms[instIndex].isComputing == false;
  }
  instIndex = 0;
}

inline completeStep() {
	for(i: 0 .. instanceCount - 1) {
		for(j: 0 .. A_LENGTH - 1) {
			ms[i].x[j] = ms[i].x[j] + ms[i].x_temp[j];
			ms[i].x_temp[j] = 0;
		}
	}
}

proctype Scheduler() {
	int i, j = 0;
	int instanceCountAux, parallelComputationCount, startInstanceIndex, 
    endInstanceIndex, currentBundleIndex, startIndex;
  parallelComputationCount = 250;

	do
	:: (step < MaxSteps) ->
		state = running;

		instanceCountAux = instanceCount - 1;
    startIndex = -1;

    for(currentBundleIndex: 1..instanceCountAux/parallelComputationCount) {
      startInstanceIndex = startIndex + 1;
      endInstanceIndex = currentBundleIndex * parallelComputationCount;

      applyRulesForMembranesInRange(startInstanceIndex, endInstanceIndex);
      rulesApplied(startInstanceIndex, endInstanceIndex);

      startIndex = currentBundleIndex * parallelComputationCount;
    }

    startInstanceIndex = startIndex + 1;
    applyRulesForMembranesInRange(startInstanceIndex, instanceCountAux);
    rulesApplied(startInstanceIndex, instanceCountAux);

    completeStep();

    /*printf("--------- Step %d complete! ----------\n\n", step);*/
    state = step_complete;
    isPsystemStep = true;
    isPsystemStep = false;
    step++;

		//run Log(-1);
	:: else -> break;
	od;

	//run Log(-1);
}

proctype M0(int instanceIndex) {

	ms[instanceIndex].isComputing = true;

	/* Guard Evaluations */
	byte r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23;
	r1 = false; r2 = true; r3 = true; r4 = false; r5 = false; r6 = true; r7 = false; r8 = false; r9 = false; r10 = true; r11 = true; r12 = false; r13 = true; r14 = true; r15 = false; r16 = false; r17 = true; r18 = false; r19 = false; r20 = true; r21 = true; r22 = false; r23 = true;
	if
	::	(ms[instanceIndex].x[@B_3] == 1 && ms[instanceIndex].x[@X] == 1) -> r1 = true;
	::	else -> skip;
	fi;
	if
	::	((ms[instanceIndex].x[@v] == 101) == 0) -> r4 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_7] == 1 && ms[instanceIndex].x[@X] == 1) -> r5 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_9] == 1 && ms[instanceIndex].x[@X] == 1) -> r7 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_6] == 1 && ms[instanceIndex].x[@X] == 1) -> r8 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_8] == 1 && ms[instanceIndex].x[@X] == 1) -> r9 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_4] == 1 && ms[instanceIndex].x[@X] == 1) -> r12 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@v] == 101) -> r15 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_5] == 1 && ms[instanceIndex].x[@X] == 1) -> r16 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_2] == 1 && ms[instanceIndex].x[@X] == 1) -> r18 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_1] == 1 && ms[instanceIndex].x[@X] == 1) -> r19 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@B_10] == 1 && ms[instanceIndex].x[@X] == 1) -> r22 = true;
	::	else -> skip;
	fi;


	/* Rewriting and Communication Rules */
	do
	:: (r1 && ms[instanceIndex].x[@v_3] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_3, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r4 && ms[instanceIndex].x[@Y] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @Y, 1);
				doReplicate(1, @F, 1);
				skip;
			}
	:: (r5 && ms[instanceIndex].x[@v_7] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_7, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r7 && ms[instanceIndex].x[@v_9] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_9, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r8 && ms[instanceIndex].x[@v_6] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_6, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r9 && ms[instanceIndex].x[@v_8] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_8, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r12 && ms[instanceIndex].x[@v_4] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_4, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r15 && ms[instanceIndex].x[@Y] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @Y, 1);
				doReplicate(1, @T, 1);
				skip;
			}
	:: (r16 && ms[instanceIndex].x[@v_5] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_5, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r17 && ms[instanceIndex].x[@X] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @X, 1);
				doRhs(instanceIndex, @Y, 1);
				skip;
			}
	:: (r18 && ms[instanceIndex].x[@v_2] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_2, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r19 && ms[instanceIndex].x[@v_1] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_1, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: (r22 && ms[instanceIndex].x[@v_10] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @v_10, 1);
				doRhs(instanceIndex, @v, 1);
				skip;
			}
	:: else -> break;
	od;

	/* Division Rules */
	if
	:: (r2 && ms[instanceIndex].x[@A_9] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_9, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @B_9, 1);
				doRhs(instanceCount - 2, @A_10, 1);
				doRhs(instanceCount - 1, @A_10, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r3 && ms[instanceIndex].x[@A_2] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_2, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @B_2, 1);
				doRhs(instanceCount - 2, @A_3, 1);
				doRhs(instanceCount - 1, @A_3, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r6 && ms[instanceIndex].x[@A_8] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_8, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @A_9, 1);
				doRhs(instanceCount - 2, @B_8, 1);
				doRhs(instanceCount - 1, @A_9, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r10 && ms[instanceIndex].x[@A_4] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_4, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @B_4, 1);
				doRhs(instanceCount - 2, @A_5, 1);
				doRhs(instanceCount - 1, @A_5, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r11 && ms[instanceIndex].x[@A_3] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_3, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @B_3, 1);
				doRhs(instanceCount - 2, @A_4, 1);
				doRhs(instanceCount - 1, @A_4, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r13 && ms[instanceIndex].x[@A_5] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_5, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @A_6, 1);
				doRhs(instanceCount - 2, @B_5, 1);
				doRhs(instanceCount - 1, @A_6, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r14 && ms[instanceIndex].x[@A_10] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_10, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @B_10, 1);
				doRhs(instanceCount - 2, @X, 1);
				doRhs(instanceCount - 1, @X, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r20 && ms[instanceIndex].x[@A_7] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_7, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @A_8, 1);
				doRhs(instanceCount - 2, @B_7, 1);
				doRhs(instanceCount - 1, @A_8, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r21 && ms[instanceIndex].x[@A_1] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_1, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @B_1, 1);
				doRhs(instanceCount - 2, @A_2, 1);
				doRhs(instanceCount - 1, @A_2, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: (r23 && ms[instanceIndex].x[@A_6] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @A_6, 1);
				divide(instanceIndex, 2);
				doRhs(instanceCount - 2, @A_7, 1);
				doRhs(instanceCount - 2, @B_6, 1);
				doRhs(instanceCount - 1, @A_7, 1);
				doDissolve(instanceIndex);
				skip;
			}
	:: else -> skip;
	fi;

	ms[instanceIndex].isComputing = false;
}

proctype M1(int instanceIndex) {

	ms[instanceIndex].isComputing = true;

	/* Guard Evaluations */
	byte r1, r2;
	r1 = false; r2 = false;
	if
	::	(ms[instanceIndex].x[@T] >= 1) -> r1 = true;
	::	else -> skip;
	fi;
	if
	::	(ms[instanceIndex].x[@F] >= 1 && ms[instanceIndex].x[@T] < 1) -> r2 = true;
	::	else -> skip;
	fi;


	/* Rewriting and Communication Rules */
	do
	:: (r1 && ms[instanceIndex].x[@S] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @S, 1);
				doReplicate(2, @yes, 1);
				skip;
			}
	:: (r2 && ms[instanceIndex].x[@S] >= 1) ->
		  skip;
			d_step {
				doLhs(instanceIndex, @S, 1);
				doReplicate(2, @no, 1);
				skip;
			}
	:: else -> break;
	od;


	ms[instanceIndex].isComputing = false;
}

init {
	/* Instance #0 */
	ms[0].type = 0;
	ms[0].x[@v_3] = 5;
	ms[0].x[@v_4] = 8;
	ms[0].x[@v_1] = 2;
	ms[0].x[@v_2] = 3;
	ms[0].x[@v_7] = 11;
	ms[0].x[@v_8] = 14;
	ms[0].x[@v_5] = 9;
	ms[0].x[@v_6] = 10;
	ms[0].x[@A_1] = 1;
	ms[0].x[@v_9] = 19;
	ms[0].x[@v_10] = 25;

	/* Instance #1 */
	ms[1].type = 1;
	ms[1].x[@S] = 1;

	/* Instance #2 */
	ms[2].type = 2;


	instanceCount = 3;

	//run Log(-1);

	run Scheduler();
}