/*
 *  Àëãîðèòì Ôîðäà - Ôàëêåðñîíà äëÿ ïîèñêà ìàêñèìàëüíîãî ïîòîêà â òðàíñïîðòíîé ñåòè.
 *
 *  Òðàíñïîðòíàÿ ñåòü çàäàåòñÿ ÷èñëîì óçëîâ N (2 <= N <= MAX_N) è íàáîðîì ðåáåð
 *  ñ óêàçàíèåì ïðîïóñêíîé ñïîñîáíîñòè êàæäîãî ñóùåñòâóþùåãî ðåáðà C (0 <= C <= MAXC).
 *  Åñëè ïðîïóñêíàÿ ñïîñîáíîñòü ðåáðà ðàâíà 0, òî ðåáðà íåò.
 *
 *  Ïîòîê èùåòñÿ ìåæäó èñòî÷íèêîì S (âåðøèíà ñ íîìåðîì 0), è ñòîêîì T (âåðøèíà ñ íîìåðîì N-1).
 *
 *  Èäåÿ àëãîðèòìà çàêëþ÷àåòñÿ â èòåðàòèâíîì óâåëè÷åíèè ïîòîêà ñ 0 äî ìàêñèìàëüíî âîçìîæíîãî. Íà êàæäîé èòåðàöèè èùåòñÿ ïóòü,
 *  ïî êîòîðîìó ìîæíî ïóñòèòü äîïîëíèòåëüíûé ïîòîê èç èñòî÷íèêà â ñòîê.
 *  Àëãîðèòì ðàáîòàåò çà âðåìÿ O(E * f), ãäå E - ÷èñëî ðåáåð, f - ìàêñèìàëüíûé ïîòîê â ñåòè.
 */

#define MAX_N 3		// maximum vertex count
#define MAX_M 3		// maximum number of edges
#define MAXC 3		// maximum edge constraint

// algorithm states:
#define UNKNOWN					0
#define SEARCHING_PATH			1
#define SEARCHING_FINISHED		2
#define CALCULATING_INC_VALUE	3
#define CALCULATING_FINISHED	4
#define INCREASING_FLOW			5
#define INCREASING_FINISHED		6
#define ALGORITHM_FINISHED		7


typedef array {
	int a[MAX_N];
}


byte state;		// current state

int n;			// states' count

array c[MAX_N];	// edge constrains
array f[MAX_N];	// edge flow

bool foundPath;
int incFlowValue;
int maxFlow;

int pi;					// path index
int path[MAX_N];		// for path saving
bool visited[MAX_N];	// is vertex x visited?


/* ------------------------------- auxiliary "functions" -------------------------------- */

int minValue;

inline min(a, b) {
    printf("Comparing %d and %d\n",a,b);
	if
	:: (a < b)	->
		minValue = a;
	:: else		->
		minValue = b;
	fi;
}

int randomValue;

// generate random in range [minV, maxV]
inline genRandom(minV, maxV) {
	randomValue = minV;
	do
	:: (randomValue == maxV)		->
		break;	// increased up to max value -> stop
	:: else						->
		if
		:: randomValue++;	// randomly increment
		:: break;			// or stop
		fi;
	od;
}


/* ------------------------------- algorithm "functions" -------------------------------- */

int i, j;	// temp variables


inline findPathImpl() {
	// clearing
	for (i : 0..(n-1)) {
		visited[i] = false;
	}

	foundPath = false;
	pi = 0;
	path[pi] = 0;	// starting from source
	bool findNext;

	// searching...
	do
	:: ((!foundPath) && (pi >= 0))	->
		if
		:: (!visited[path[pi]])		->	// going forward
			visited[path[pi]] = true;
			if
			:: (path[pi] == n - 1)	->	foundPath = true;
			:: else					->	path[pi+1] = 0;	// new search
			fi;
		:: else						->	// continuing search
			path[pi+1]++;
		fi;

		if
		:: (!foundPath)		->
			pi++;
			findNext = false;
			do
			:: ((path[pi] < n) && (!findNext))	->
				i = path[pi - 1];
				j = path[pi];
				if
				:: ((c[i].a[j] - f[i].a[i] > 0) && (!visited[j]))	->
					findNext = true;
				:: else 	->
					path[pi]++;
				fi;
			:: else 			->	break;
			od;
			if
			:: (!findNext)	->	pi = pi - 2;
			:: else			->	skip;
			fi;
		:: else		->	skip;
		fi;
	:: else		-> break;
	od;
}


inline findPath() {
	state = SEARCHING_PATH;
	findPathImpl();
	state = SEARCHING_FINISHED;
}


int pi2;

inline calculateIncreaseValue() {
	state = CALCULATING_INC_VALUE;

	incFlowValue = 2 * MAXC;
	pi2 = 0;
	do
	:: (pi2 < pi) 	->
		i = path[pi2];
		j = path[pi2 + 1];

		min(incFlowValue, c[i].a[j] - f[i].a[j]);
		incFlowValue = minValue;

		pi2++;
	:: else 		->	break;
	od;

	state = CALCULATING_FINISHED;
}

inline increaseFlow() {
	state = INCREASING_FLOW;

	pi2 = 0;
	do
	:: (pi2 < pi) 	->
		i = path[pi2];
		j = path[pi2 + 1];

        printf("From %d to %d reduce %d\n", i, j, incFlowValue);

		f[i].a[j] = f[i].a[j] + incFlowValue;
		f[j].a[i] = f[j].a[i] - incFlowValue;

		pi2++;
	:: else 		->	break;
	od;
	maxFlow = maxFlow + incFlowValue;

	state = INCREASING_FINISHED;
}


inline findMaxFlow() {
	maxFlow = 0;

	findPath();
	do
	:: (foundPath)	->
		calculateIncreaseValue();
		increaseFlow();

        if
        :: (incFlowValue > 0) -> findPath();
        :: else -> foundPath = false;
        fi;
	:: else 		->	break;
	od;

	state = ALGORITHM_FINISHED;
}


init {
	printf("INIT: Starting\n\n");

	printf("Generating input:\n");

	genRandom(2, MAX_N);
	n = randomValue;
	genRandom(0, MAX_M);
	int m = randomValue;
	printf("Vertex count = %d\n", n);
	printf("Edges (count = %d):\n", m);
	int en, cc;
	for (en : 0..(m-1)) {
		genRandom(0, n - 1);
		i = randomValue;
		genRandom(0, n - 1);
		j = randomValue;
		genRandom(1, MAXC);
		cc = randomValue;
		printf("%d -> %d, c = %d\n", i, j, cc);
		c[i].a[j] = cc;
	}
	printf("\n");

	printf("Starting algorithm...\n");
	findMaxFlow();
	printf("Finished. Max flow = %d\n\n", maxFlow);

	findPathImpl();

	printf("INIT: Finished\n");
}