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

//---------- VARIABLES DECLARATION ---------
int	track_0_Patient,
	track_0_PrimaryDoctor,
	track_0_target,
	track_0_SUPER_ROLE,
	track_1_Patient,
	track_1_PrimaryDoctor,
	track_1_target,
	track_1_SUPER_ROLE,
	b_0,
	b_1;

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

	//---------- INITIALIZE VARIABLES ---------
	b_0 = 0;
	b_1 = 0;

	track_0_Patient = 0;
	track_0_PrimaryDoctor = 0;
	track_0_target = 0;
	track_0_SUPER_ROLE = 0;
	track_1_Patient = 0;
	track_1_PrimaryDoctor = 0;
	track_1_target = 0;
	track_1_SUPER_ROLE = 0;

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

	//Configuration of user1
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
		}
		else if (!b_1) {
			b_1 = 1;
		}
	}

	//Configuration of SUPER_USER
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_SUPER_ROLE = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_SUPER_ROLE = 1;
		}
	}

	//Configuration of user101
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_PrimaryDoctor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_PrimaryDoctor = 1;
		}
	}

	//Configuration of user102
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_PrimaryDoctor = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_PrimaryDoctor = 1;
		}
	}

	//Configuration of user331
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Patient = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Patient = 1;
		}
	}

	//Configuration of user332
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Patient = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Patient = 1;
		}
	}

	//---------- SIMULATION OF RULES ---------
	while(1){
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <SUPER_ROLE,PrimaryDoctor&Patient,target>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_PrimaryDoctor && track_0_Patient){
					track_0_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_PrimaryDoctor && track_1_Patient){
					track_1_target = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 1 -----------------
		// <SUPER_ROLE,-Patient,PrimaryDoctor>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && !track_0_Patient){
					track_0_PrimaryDoctor = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && !track_1_Patient){
					track_1_PrimaryDoctor = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 2 -----------------
		// <SUPER_ROLE,-PrimaryDoctor,Patient>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && !track_0_PrimaryDoctor){
					track_0_Patient = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && !track_1_PrimaryDoctor){
					track_1_Patient = 1;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 0 ---------------------
		// <SUPER_ROLE,PrimaryDoctor>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_PrimaryDoctor){
					track_0_PrimaryDoctor = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_PrimaryDoctor){
					track_1_PrimaryDoctor = 0;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 1 ---------------------
		// <SUPER_ROLE,Patient>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_Patient){
					track_0_Patient = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Patient){
					track_1_Patient = 0;
				}
			}
		}
		//---------------Error------------
		if(track_0_target==1 || track_1_target==1){
			assert(0);
		}
	}

}