#define rand	pan_rand
#if defined(HAS_CODE) && defined(VERBOSE)
	cpu_printf("Pr: %d Tr: %d\n", II, t->forw);
#endif
	switch (t->forw) {
	default: Uerror("bad forward move");
	case 0:	/* if without executable clauses */
		continue;
	case 1: /* generic 'goto' or 'skip' */
		IfNotBlocked
		_m = 3; goto P999;
	case 2: /* generic 'else' */
		IfNotBlocked
		if (trpt->o_pm&1) continue;
		_m = 3; goto P999;

		 /* PROC pcbit_receive */
	case 3: /* STATE 2 - line 39 "task3.pml" - [channel!_pid,FROM_P,GIMME] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][2] = 1;
		if (q_len(now.channel))
			continue;
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d!", now.channel);
		sprintf(simtmp, "%d", ((int)((P1 *)this)->_pid)); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 5); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 2); strcat(simvals, simtmp);		}
#endif
		
		qsend(now.channel, 0, ((int)((P1 *)this)->_pid), 5, 2, 3);
		{ boq = now.channel; };
		_m = 2; goto P999; /* 0 */
	case 4: /* STATE 3 - line 40 "task3.pml" - [channel?_pid,FROM_M,result] (0:0:2 - 1) */
		reached[1][3] = 1;
		if (boq != now.channel) continue;
		if (q_len(now.channel) == 0) continue;

		XX=1;
		if (6 != qrecv(now.channel, 0, 1, 0)) continue;
		(trpt+1)->bup.ovals = grab_ints(2);
		(trpt+1)->bup.ovals[0] = ((int)((P1 *)this)->_pid);
		(trpt+1)->bup.ovals[1] = ((P1 *)this)->result;
		;
		((P1 *)this)->_pid = qrecv(now.channel, XX-1, 0, 0);
#ifdef VAR_RANGES
		logval("_pid", ((int)((P1 *)this)->_pid));
#endif
		;
		((P1 *)this)->result = qrecv(now.channel, XX-1, 2, 1);
#ifdef VAR_RANGES
		logval("pcbit_receive:result", ((P1 *)this)->result);
#endif
		;
		
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d?", now.channel);
		sprintf(simtmp, "%d", ((int)((P1 *)this)->_pid)); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 6); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", ((P1 *)this)->result); strcat(simvals, simtmp);		}
#endif
		if (q_zero(now.channel))
		{	boq = -1;
#ifndef NOFAIR
			if (fairness
			&& !(trpt->o_pm&32)
			&& (now._a_t&2)
			&&  now._cnt[now._a_t&1] == II+2)
			{	now._cnt[now._a_t&1] -= 1;
#ifdef VERI
				if (II == 1)
					now._cnt[now._a_t&1] = 1;
#endif
#ifdef DEBUG
			printf("%3d: proc %d fairness ", depth, II);
			printf("Rule 2: --cnt to %d (%d)\n",
				now._cnt[now._a_t&1], now._a_t);
#endif
				trpt->o_pm |= (32|64);
			}
#endif

		};
		_m = 4; goto P999; /* 0 */
	case 5: /* STATE 4 - line 42 "task3.pml" - [((result==EPIC_FAIL))] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][4] = 1;
		if (!((((P1 *)this)->result==3)))
			continue;
		/* dead 1: result */  (trpt+1)->bup.oval = ((P1 *)this)->result;
#ifdef HAS_CODE
		if (!readtrail)
#endif
			((P1 *)this)->result = 0;
		_m = 3; goto P999; /* 0 */
	case 6: /* STATE 11 - line 50 "task3.pml" - [channel!_pid,FROM_P,FREE] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][11] = 1;
		if (q_len(now.channel))
			continue;
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d!", now.channel);
		sprintf(simtmp, "%d", ((int)((P1 *)this)->_pid)); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 5); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 1); strcat(simvals, simtmp);		}
#endif
		
		qsend(now.channel, 0, ((int)((P1 *)this)->_pid), 5, 1, 3);
		{ boq = now.channel; };
		_m = 2; goto P999; /* 0 */
	case 7: /* STATE 12 - line 51 "task3.pml" - [channel?_pid,FROM_M,result] (0:0:3 - 1) */
		reached[1][12] = 1;
		if (boq != now.channel) continue;
		if (q_len(now.channel) == 0) continue;

		XX=1;
		if (6 != qrecv(now.channel, 0, 1, 0)) continue;
		(trpt+1)->bup.ovals = grab_ints(3);
		(trpt+1)->bup.ovals[0] = ((int)((P1 *)this)->_pid);
		(trpt+1)->bup.ovals[1] = ((P1 *)this)->result;
		;
		((P1 *)this)->_pid = qrecv(now.channel, XX-1, 0, 0);
#ifdef VAR_RANGES
		logval("_pid", ((int)((P1 *)this)->_pid));
#endif
		;
		((P1 *)this)->result = qrecv(now.channel, XX-1, 2, 1);
#ifdef VAR_RANGES
		logval("pcbit_receive:result", ((P1 *)this)->result);
#endif
		;
		
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d?", now.channel);
		sprintf(simtmp, "%d", ((int)((P1 *)this)->_pid)); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 6); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", ((P1 *)this)->result); strcat(simvals, simtmp);		}
#endif
		if (q_zero(now.channel))
		{	boq = -1;
#ifndef NOFAIR
			if (fairness
			&& !(trpt->o_pm&32)
			&& (now._a_t&2)
			&&  now._cnt[now._a_t&1] == II+2)
			{	now._cnt[now._a_t&1] -= 1;
#ifdef VERI
				if (II == 1)
					now._cnt[now._a_t&1] = 1;
#endif
#ifdef DEBUG
			printf("%3d: proc %d fairness ", depth, II);
			printf("Rule 2: --cnt to %d (%d)\n",
				now._cnt[now._a_t&1], now._a_t);
#endif
				trpt->o_pm |= (32|64);
			}
#endif

		};
		/* dead 2: result */  (trpt+1)->bup.ovals[2] = ((P1 *)this)->result;
#ifdef HAS_CODE
		if (!readtrail)
#endif
			((P1 *)this)->result = 0;
		_m = 4; goto P999; /* 0 */
	case 8: /* STATE 21 - line 9 "task3.pml" - [flag[_pid] = 1] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][21] = 1;
		(trpt+1)->bup.oval = ((int)now.flag[ Index(((int)((P1 *)this)->_pid), 2) ]);
		now.flag[ Index(((P1 *)this)->_pid, 2) ] = 1;
#ifdef VAR_RANGES
		logval("flag[_pid]", ((int)now.flag[ Index(((int)((P1 *)this)->_pid), 2) ]));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 9: /* STATE 22 - line 10 "task3.pml" - [turn = _pid] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][22] = 1;
		(trpt+1)->bup.oval = ((int)now.turn);
		now.turn = ((int)((P1 *)this)->_pid);
#ifdef VAR_RANGES
		logval("turn", ((int)now.turn));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 10: /* STATE 23 - line 10 "task3.pml" - [(((flag[(1-_pid)]==0)||(turn==(1-_pid))))] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][23] = 1;
		if (!(((((int)now.flag[ Index((1-((int)((P1 *)this)->_pid)), 2) ])==0)||(((int)now.turn)==(1-((int)((P1 *)this)->_pid))))))
			continue;
		_m = 3; goto P999; /* 0 */
	case 11: /* STATE 29 - line 16 "task3.pml" - [flag[(_pid-2)] = 0] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][29] = 1;
		(trpt+1)->bup.oval = ((int)now.flag[ Index((((int)((P1 *)this)->_pid)-2), 2) ]);
		now.flag[ Index((((P1 *)this)->_pid-2), 2) ] = 0;
#ifdef VAR_RANGES
		logval("flag[(_pid-2)]", ((int)now.flag[ Index((((int)((P1 *)this)->_pid)-2), 2) ]));
#endif
		;
		_m = 3; goto P999; /* 0 */

		 /* PROC memory_manager */
	case 12: /* STATE 1 - line 23 "task3.pml" - [channel?who,FROM_P,GIMME] (0:0:1 - 1) */
		reached[0][1] = 1;
		if (boq != now.channel) continue;
		if (q_len(now.channel) == 0) continue;

		XX=1;
		if (5 != qrecv(now.channel, 0, 1, 0)) continue;
		if (2 != qrecv(now.channel, 0, 2, 0)) continue;
		(trpt+1)->bup.oval = ((P0 *)this)->who;
		;
		((P0 *)this)->who = qrecv(now.channel, XX-1, 0, 0);
#ifdef VAR_RANGES
		logval("memory_manager:who", ((P0 *)this)->who);
#endif
		;
		qrecv(now.channel, XX-1, 2, 1);
		
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d?", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 5); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 2); strcat(simvals, simtmp);		}
#endif
		if (q_zero(now.channel))
		{	boq = -1;
#ifndef NOFAIR
			if (fairness
			&& !(trpt->o_pm&32)
			&& (now._a_t&2)
			&&  now._cnt[now._a_t&1] == II+2)
			{	now._cnt[now._a_t&1] -= 1;
#ifdef VERI
				if (II == 1)
					now._cnt[now._a_t&1] = 1;
#endif
#ifdef DEBUG
			printf("%3d: proc %d fairness ", depth, II);
			printf("Rule 2: --cnt to %d (%d)\n",
				now._cnt[now._a_t&1], now._a_t);
#endif
				trpt->o_pm |= (32|64);
			}
#endif

		};
		_m = 4; goto P999; /* 0 */
	case 13: /* STATE 2 - line 23 "task3.pml" - [channel!who,FROM_M,DONE] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][2] = 1;
		if (q_len(now.channel))
			continue;
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d!", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 6); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 4); strcat(simvals, simtmp);		}
#endif
		
		qsend(now.channel, 0, ((P0 *)this)->who, 6, 4, 3);
		{ boq = now.channel; };
		_m = 2; goto P999; /* 0 */
	case 14: /* STATE 3 - line 24 "task3.pml" - [channel?who,FROM_P,GIMME] (0:0:1 - 1) */
		reached[0][3] = 1;
		if (boq != now.channel) continue;
		if (q_len(now.channel) == 0) continue;

		XX=1;
		if (5 != qrecv(now.channel, 0, 1, 0)) continue;
		if (2 != qrecv(now.channel, 0, 2, 0)) continue;
		(trpt+1)->bup.oval = ((P0 *)this)->who;
		;
		((P0 *)this)->who = qrecv(now.channel, XX-1, 0, 0);
#ifdef VAR_RANGES
		logval("memory_manager:who", ((P0 *)this)->who);
#endif
		;
		qrecv(now.channel, XX-1, 2, 1);
		
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d?", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 5); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 2); strcat(simvals, simtmp);		}
#endif
		if (q_zero(now.channel))
		{	boq = -1;
#ifndef NOFAIR
			if (fairness
			&& !(trpt->o_pm&32)
			&& (now._a_t&2)
			&&  now._cnt[now._a_t&1] == II+2)
			{	now._cnt[now._a_t&1] -= 1;
#ifdef VERI
				if (II == 1)
					now._cnt[now._a_t&1] = 1;
#endif
#ifdef DEBUG
			printf("%3d: proc %d fairness ", depth, II);
			printf("Rule 2: --cnt to %d (%d)\n",
				now._cnt[now._a_t&1], now._a_t);
#endif
				trpt->o_pm |= (32|64);
			}
#endif

		};
		_m = 4; goto P999; /* 0 */
	case 15: /* STATE 4 - line 24 "task3.pml" - [channel!who,FROM_M,EPIC_FAIL] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][4] = 1;
		if (q_len(now.channel))
			continue;
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d!", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 6); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 3); strcat(simvals, simtmp);		}
#endif
		
		qsend(now.channel, 0, ((P0 *)this)->who, 6, 3, 3);
		{ boq = now.channel; };
		_m = 2; goto P999; /* 0 */
	case 16: /* STATE 5 - line 25 "task3.pml" - [channel?who,FROM_P,FREE] (0:0:1 - 1) */
		reached[0][5] = 1;
		if (boq != now.channel) continue;
		if (q_len(now.channel) == 0) continue;

		XX=1;
		if (5 != qrecv(now.channel, 0, 1, 0)) continue;
		if (1 != qrecv(now.channel, 0, 2, 0)) continue;
		(trpt+1)->bup.oval = ((P0 *)this)->who;
		;
		((P0 *)this)->who = qrecv(now.channel, XX-1, 0, 0);
#ifdef VAR_RANGES
		logval("memory_manager:who", ((P0 *)this)->who);
#endif
		;
		qrecv(now.channel, XX-1, 2, 1);
		
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d?", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 5); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 1); strcat(simvals, simtmp);		}
#endif
		if (q_zero(now.channel))
		{	boq = -1;
#ifndef NOFAIR
			if (fairness
			&& !(trpt->o_pm&32)
			&& (now._a_t&2)
			&&  now._cnt[now._a_t&1] == II+2)
			{	now._cnt[now._a_t&1] -= 1;
#ifdef VERI
				if (II == 1)
					now._cnt[now._a_t&1] = 1;
#endif
#ifdef DEBUG
			printf("%3d: proc %d fairness ", depth, II);
			printf("Rule 2: --cnt to %d (%d)\n",
				now._cnt[now._a_t&1], now._a_t);
#endif
				trpt->o_pm |= (32|64);
			}
#endif

		};
		_m = 4; goto P999; /* 0 */
	case 17: /* STATE 6 - line 25 "task3.pml" - [channel!who,FROM_M,DONE] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][6] = 1;
		if (q_len(now.channel))
			continue;
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d!", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 6); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 4); strcat(simvals, simtmp);		}
#endif
		
		qsend(now.channel, 0, ((P0 *)this)->who, 6, 4, 3);
		{ boq = now.channel; };
		_m = 2; goto P999; /* 0 */
	case 18: /* STATE 7 - line 26 "task3.pml" - [channel?who,FROM_P,FREE] (0:0:1 - 1) */
		reached[0][7] = 1;
		if (boq != now.channel) continue;
		if (q_len(now.channel) == 0) continue;

		XX=1;
		if (5 != qrecv(now.channel, 0, 1, 0)) continue;
		if (1 != qrecv(now.channel, 0, 2, 0)) continue;
		(trpt+1)->bup.oval = ((P0 *)this)->who;
		;
		((P0 *)this)->who = qrecv(now.channel, XX-1, 0, 0);
#ifdef VAR_RANGES
		logval("memory_manager:who", ((P0 *)this)->who);
#endif
		;
		qrecv(now.channel, XX-1, 2, 1);
		
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d?", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 5); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 1); strcat(simvals, simtmp);		}
#endif
		if (q_zero(now.channel))
		{	boq = -1;
#ifndef NOFAIR
			if (fairness
			&& !(trpt->o_pm&32)
			&& (now._a_t&2)
			&&  now._cnt[now._a_t&1] == II+2)
			{	now._cnt[now._a_t&1] -= 1;
#ifdef VERI
				if (II == 1)
					now._cnt[now._a_t&1] = 1;
#endif
#ifdef DEBUG
			printf("%3d: proc %d fairness ", depth, II);
			printf("Rule 2: --cnt to %d (%d)\n",
				now._cnt[now._a_t&1], now._a_t);
#endif
				trpt->o_pm |= (32|64);
			}
#endif

		};
		_m = 4; goto P999; /* 0 */
	case 19: /* STATE 8 - line 26 "task3.pml" - [channel!who,FROM_M,EPIC_FAIL] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][8] = 1;
		if (q_len(now.channel))
			continue;
#ifdef HAS_CODE
		if (readtrail && gui) {
			char simtmp[32];
			sprintf(simvals, "%d!", now.channel);
		sprintf(simtmp, "%d", ((P0 *)this)->who); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 6); strcat(simvals, simtmp);		strcat(simvals, ",");
		sprintf(simtmp, "%d", 3); strcat(simvals, simtmp);		}
#endif
		
		qsend(now.channel, 0, ((P0 *)this)->who, 6, 3, 3);
		{ boq = now.channel; };
		_m = 2; goto P999; /* 0 */
	case 20: /* STATE 12 - line 28 "task3.pml" - [-end-] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][12] = 1;
		if (!delproc(1, II)) continue;
		_m = 3; goto P999; /* 0 */
	case  _T5:	/* np_ */
		if (!((!(trpt->o_pm&4) && !(trpt->tau&128))))
			continue;
		/* else fall through */
	case  _T2:	/* true */
		_m = 3; goto P999;
#undef rand
	}