Prog3

gistfile1.txt

// tjadam, jawaterm
// 2014.3.26
// Group Assignment 3 - Play By Your Own Rules

int topcard[5];  // 0 through 3 for each player


proctype player(int i) {
	do
		:: atomic{
			if
				:: topcard[(i+4)%5] > topcard[i] -> topcard[i] = topcard[(i+4)%5]
				:: topcard[(i+1)%5] > topcard[i] -> topcard[i] = topcard[(i+1)%5]
			fi;
		}
	od;

}

proctype owner() {
	atomic{
		//shuffle n number of times
		int j;
		int v;
		for( j : 0..4 ){
			select (v : 0..3);
			topcard[j] = v;
		}
	}
}

init{
	//shuffle once
	int j;
	int v;
	for( j : 0..4 ){
		select (v : 0..3);
		topcard[j] = v;
	}


	int x;
	for(x : 0..4){
		run player(x);
	}

	run owner();
}

#define winning (topcard[0] == topcard[1] && topcard[1] == topcard[2] && \
				 topcard[2] == topcard[3] && topcard[3] == topcard[4])

ltl victory { <> [] winning };