#include <stdio.h>
_Bool nondet_bool();

//---------- VARIABLES DECLARATION ---------
int	track_0_Dean,
	track_0_DeptChair,
	track_0_President,
	track_0_Professor,
	track_0_Provost,
	track_0_target,
	track_0_SUPER_ROLE,
	track_1_Dean,
	track_1_DeptChair,
	track_1_President,
	track_1_Professor,
	track_1_Provost,
	track_1_target,
	track_1_SUPER_ROLE,
	track_2_Dean,
	track_2_DeptChair,
	track_2_President,
	track_2_Professor,
	track_2_Provost,
	track_2_target,
	track_2_SUPER_ROLE,
	track_3_Dean,
	track_3_DeptChair,
	track_3_President,
	track_3_Professor,
	track_3_Provost,
	track_3_target,
	track_3_SUPER_ROLE,
	track_4_Dean,
	track_4_DeptChair,
	track_4_President,
	track_4_Professor,
	track_4_Provost,
	track_4_target,
	track_4_SUPER_ROLE,
	b_0,
	b_1,
	b_2,
	b_3,
	b_4;

//---------- BEGIN MAIN PROGRAM ---------
int main()
{

	//---------- INITIALIZE VARIABLES ---------
	b_0 = 0;
	b_1 = 0;
	b_2 = 0;
	b_3 = 0;
	b_4 = 0;

	track_0_Dean = 0;
	track_0_DeptChair = 0;
	track_0_President = 0;
	track_0_Professor = 0;
	track_0_Provost = 0;
	track_0_target = 0;
	track_0_SUPER_ROLE = 0;
	track_1_Dean = 0;
	track_1_DeptChair = 0;
	track_1_President = 0;
	track_1_Professor = 0;
	track_1_Provost = 0;
	track_1_target = 0;
	track_1_SUPER_ROLE = 0;
	track_2_Dean = 0;
	track_2_DeptChair = 0;
	track_2_President = 0;
	track_2_Professor = 0;
	track_2_Provost = 0;
	track_2_target = 0;
	track_2_SUPER_ROLE = 0;
	track_3_Dean = 0;
	track_3_DeptChair = 0;
	track_3_President = 0;
	track_3_Professor = 0;
	track_3_Provost = 0;
	track_3_target = 0;
	track_3_SUPER_ROLE = 0;
	track_4_Dean = 0;
	track_4_DeptChair = 0;
	track_4_President = 0;
	track_4_Professor = 0;
	track_4_Provost = 0;
	track_4_target = 0;
	track_4_SUPER_ROLE = 0;

	//---------- CONFIGURATION_USERS ---------
	//Configuration of user0
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
		}
		else if (!b_1) {
			b_1 = 1;
		}
		else if (!b_2) {
			b_2 = 1;
		}
		else if (!b_3) {
			b_3 = 1;
		}
		else if (!b_4) {
			b_4 = 1;
		}
	}

	//Configuration of user1
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Dean = 1;
			track_0_Professor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Dean = 1;
			track_1_Professor = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_Dean = 1;
			track_2_Professor = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_Dean = 1;
			track_3_Professor = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_Dean = 1;
			track_4_Professor = 1;
		}
	}

	//Configuration of SUPER_USER
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_DeptChair = 1;
			track_0_Professor = 1;
			track_0_SUPER_ROLE = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_DeptChair = 1;
			track_1_Professor = 1;
			track_1_SUPER_ROLE = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_DeptChair = 1;
			track_2_Professor = 1;
			track_2_SUPER_ROLE = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_DeptChair = 1;
			track_3_Professor = 1;
			track_3_SUPER_ROLE = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_DeptChair = 1;
			track_4_Professor = 1;
			track_4_SUPER_ROLE = 1;
		}
	}

	//Configuration of user3
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
		}
		else if (!b_1) {
			b_1 = 1;
		}
		else if (!b_2) {
			b_2 = 1;
		}
		else if (!b_3) {
			b_3 = 1;
		}
		else if (!b_4) {
			b_4 = 1;
		}
	}

	//Configuration of user4
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
		}
		else if (!b_1) {
			b_1 = 1;
		}
		else if (!b_2) {
			b_2 = 1;
		}
		else if (!b_3) {
			b_3 = 1;
		}
		else if (!b_4) {
			b_4 = 1;
		}
	}

	//Configuration of user5
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
		}
		else if (!b_1) {
			b_1 = 1;
		}
		else if (!b_2) {
			b_2 = 1;
		}
		else if (!b_3) {
			b_3 = 1;
		}
		else if (!b_4) {
			b_4 = 1;
		}
	}

	//Configuration of user6
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Provost = 1;
			track_0_Professor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Provost = 1;
			track_1_Professor = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_Provost = 1;
			track_2_Professor = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_Provost = 1;
			track_3_Professor = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_Provost = 1;
			track_4_Professor = 1;
		}
	}

	//Configuration of user7
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
		}
		else if (!b_1) {
			b_1 = 1;
		}
		else if (!b_2) {
			b_2 = 1;
		}
		else if (!b_3) {
			b_3 = 1;
		}
		else if (!b_4) {
			b_4 = 1;
		}
	}

	//Configuration of user108
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Professor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Professor = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_Professor = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_Professor = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_Professor = 1;
		}
	}

	//Configuration of user109
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Professor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Professor = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_Professor = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_Professor = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_Professor = 1;
		}
	}

	//Configuration of user110
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Professor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Professor = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_Professor = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_Professor = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_Professor = 1;
		}
	}

	//Configuration of user111
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Professor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Professor = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_Professor = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_Professor = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_Professor = 1;
		}
	}

	//Configuration of user112
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Professor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Professor = 1;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_Professor = 1;
		}
		else if (!b_3) {
			b_3 = 1;
			track_3_Professor = 1;
		}
		else if (!b_4) {
			b_4 = 1;
			track_4_Professor = 1;
		}
	}

	//---------- SIMULATION OF RULES ---------
	while(1){
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <SUPER_ROLE,Dean&DeptChair,target>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE || track_2_SUPER_ROLE || track_3_SUPER_ROLE || track_4_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_Dean && track_0_DeptChair){
					track_0_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Dean && track_1_DeptChair){
					track_1_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Dean && track_2_DeptChair){
					track_2_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Dean && track_3_DeptChair){
					track_3_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Dean && track_4_DeptChair){
					track_4_target = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 1 -----------------
		// <President,TRUE,Professor>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0){
					track_0_Professor = 1;
				}
			}
			if(nondet_bool()){
				if(b_1){
					track_1_Professor = 1;
				}
			}
			if(nondet_bool()){
				if(b_2){
					track_2_Professor = 1;
				}
			}
			if(nondet_bool()){
				if(b_3){
					track_3_Professor = 1;
				}
			}
			if(nondet_bool()){
				if(b_4){
					track_4_Professor = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 2 -----------------
		// <Dean,Professor&-Dean&-President&-Provost,DeptChair>
		//------------------------------------------------------------------
		if(track_0_Dean || track_1_Dean || track_2_Dean || track_3_Dean || track_4_Dean){
			if(nondet_bool()){
				if(b_0 && track_0_Professor && !track_0_Dean && !track_0_President && !track_0_Provost){
					track_0_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Professor && !track_1_Dean && !track_1_President && !track_1_Provost){
					track_1_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Professor && !track_2_Dean && !track_2_President && !track_2_Provost){
					track_2_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Professor && !track_3_Dean && !track_3_President && !track_3_Provost){
					track_3_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Professor && !track_4_Dean && !track_4_President && !track_4_Provost){
					track_4_DeptChair = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 3 -----------------
		// <President,Professor&-Dean&-DeptChair&-President,Provost>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0 && track_0_Professor && !track_0_Dean && !track_0_DeptChair && !track_0_President){
					track_0_Provost = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Professor && !track_1_Dean && !track_1_DeptChair && !track_1_President){
					track_1_Provost = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Professor && !track_2_Dean && !track_2_DeptChair && !track_2_President){
					track_2_Provost = 1;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Professor && !track_3_Dean && !track_3_DeptChair && !track_3_President){
					track_3_Provost = 1;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Professor && !track_4_Dean && !track_4_DeptChair && !track_4_President){
					track_4_Provost = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 4 -----------------
		// <Provost,Professor&-DeptChair&-President&-Provost,Dean>
		//------------------------------------------------------------------
		if(track_0_Provost || track_1_Provost || track_2_Provost || track_3_Provost || track_4_Provost){
			if(nondet_bool()){
				if(b_0 && track_0_Professor && !track_0_DeptChair && !track_0_President && !track_0_Provost){
					track_0_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Professor && !track_1_DeptChair && !track_1_President && !track_1_Provost){
					track_1_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Professor && !track_2_DeptChair && !track_2_President && !track_2_Provost){
					track_2_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Professor && !track_3_DeptChair && !track_3_President && !track_3_Provost){
					track_3_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Professor && !track_4_DeptChair && !track_4_President && !track_4_Provost){
					track_4_Dean = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 5 -----------------
		// <Provost,Professor&-Dean&-President&-Provost,DeptChair>
		//------------------------------------------------------------------
		if(track_0_Provost || track_1_Provost || track_2_Provost || track_3_Provost || track_4_Provost){
			if(nondet_bool()){
				if(b_0 && track_0_Professor && !track_0_Dean && !track_0_President && !track_0_Provost){
					track_0_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Professor && !track_1_Dean && !track_1_President && !track_1_Provost){
					track_1_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Professor && !track_2_Dean && !track_2_President && !track_2_Provost){
					track_2_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Professor && !track_3_Dean && !track_3_President && !track_3_Provost){
					track_3_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Professor && !track_4_Dean && !track_4_President && !track_4_Provost){
					track_4_DeptChair = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 6 -----------------
		// <President,Professor&-Dean&-President&-Provost,DeptChair>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0 && track_0_Professor && !track_0_Dean && !track_0_President && !track_0_Provost){
					track_0_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Professor && !track_1_Dean && !track_1_President && !track_1_Provost){
					track_1_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Professor && !track_2_Dean && !track_2_President && !track_2_Provost){
					track_2_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Professor && !track_3_Dean && !track_3_President && !track_3_Provost){
					track_3_DeptChair = 1;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Professor && !track_4_Dean && !track_4_President && !track_4_Provost){
					track_4_DeptChair = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 7 -----------------
		// <President,Professor&-DeptChair&-President&-Provost,Dean>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0 && track_0_Professor && !track_0_DeptChair && !track_0_President && !track_0_Provost){
					track_0_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Professor && !track_1_DeptChair && !track_1_President && !track_1_Provost){
					track_1_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Professor && !track_2_DeptChair && !track_2_President && !track_2_Provost){
					track_2_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Professor && !track_3_DeptChair && !track_3_President && !track_3_Provost){
					track_3_Dean = 1;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Professor && !track_4_DeptChair && !track_4_President && !track_4_Provost){
					track_4_Dean = 1;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 0 ---------------------
		// <President,Professor>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0 && track_0_Professor){
					track_0_Professor = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Professor){
					track_1_Professor = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Professor){
					track_2_Professor = 0;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Professor){
					track_3_Professor = 0;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Professor){
					track_4_Professor = 0;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 1 ---------------------
		// <President,Provost>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0 && track_0_Provost){
					track_0_Provost = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Provost){
					track_1_Provost = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Provost){
					track_2_Provost = 0;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Provost){
					track_3_Provost = 0;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Provost){
					track_4_Provost = 0;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 2 ---------------------
		// <Provost,Dean>
		//------------------------------------------------------------------
		if(track_0_Provost || track_1_Provost || track_2_Provost || track_3_Provost || track_4_Provost){
			if(nondet_bool()){
				if(b_0 && track_0_Dean){
					track_0_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Dean){
					track_1_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Dean){
					track_2_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Dean){
					track_3_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Dean){
					track_4_Dean = 0;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 3 ---------------------
		// <Dean,DeptChair>
		//------------------------------------------------------------------
		if(track_0_Dean || track_1_Dean || track_2_Dean || track_3_Dean || track_4_Dean){
			if(nondet_bool()){
				if(b_0 && track_0_DeptChair){
					track_0_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_DeptChair){
					track_1_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_DeptChair){
					track_2_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_DeptChair){
					track_3_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_DeptChair){
					track_4_DeptChair = 0;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 4 ---------------------
		// <President,Dean>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0 && track_0_Dean){
					track_0_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Dean){
					track_1_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_Dean){
					track_2_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_Dean){
					track_3_Dean = 0;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_Dean){
					track_4_Dean = 0;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 5 ---------------------
		// <Provost,DeptChair>
		//------------------------------------------------------------------
		if(track_0_Provost || track_1_Provost || track_2_Provost || track_3_Provost || track_4_Provost){
			if(nondet_bool()){
				if(b_0 && track_0_DeptChair){
					track_0_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_DeptChair){
					track_1_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_DeptChair){
					track_2_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_DeptChair){
					track_3_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_DeptChair){
					track_4_DeptChair = 0;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 6 ---------------------
		// <President,DeptChair>
		//------------------------------------------------------------------
		if(track_0_President || track_1_President || track_2_President || track_3_President || track_4_President){
			if(nondet_bool()){
				if(b_0 && track_0_DeptChair){
					track_0_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_DeptChair){
					track_1_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_DeptChair){
					track_2_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_3 && track_3_DeptChair){
					track_3_DeptChair = 0;
				}
			}
			if(nondet_bool()){
				if(b_4 && track_4_DeptChair){
					track_4_DeptChair = 0;
				}
			}
		}
		//---------------Error------------
		if(track_0_target==1 || track_1_target==1 || track_2_target==1 || track_3_target==1 || track_4_target==1){
			assert(0);
		}
	}

}