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

//---------- VARIABLES DECLARATION ---------
int	track_0_PatientWithTPC,
	track_0_ThirdParty,
	track_0_target,
	track_0_SUPER_ROLE,
	track_1_PatientWithTPC,
	track_1_ThirdParty,
	track_1_target,
	track_1_SUPER_ROLE,
	track_2_PatientWithTPC,
	track_2_ThirdParty,
	track_2_target,
	track_2_SUPER_ROLE,
	b_0,
	b_1,
	b_2;

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

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

	track_0_PatientWithTPC = 0;
	track_0_ThirdParty = 0;
	track_0_target = 0;
	track_0_SUPER_ROLE = 0;
	track_1_PatientWithTPC = 0;
	track_1_ThirdParty = 0;
	track_1_target = 0;
	track_1_SUPER_ROLE = 0;
	track_2_PatientWithTPC = 0;
	track_2_ThirdParty = 0;
	track_2_target = 0;
	track_2_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;
		}
	}

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

	//Configuration of user2
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
		}
		else if (!b_1) {
			b_1 = 1;
		}
		else if (!b_2) {
			b_2 = 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;
		}
		else if (!b_2) {
			b_2 = 1;
			track_2_SUPER_ROLE = 1;
		}
	}

	//---------- SIMULATION OF RULES ---------
	while(1){
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <SUPER_ROLE,PatientWithTPC,target>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE || track_2_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_PatientWithTPC){
					track_0_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_PatientWithTPC){
					track_1_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_PatientWithTPC){
					track_2_target = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 1 -----------------
		// <SUPER_ROLE,TRUE,ThirdParty>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE || track_2_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0){
					track_0_ThirdParty = 1;
				}
			}
			if(nondet_bool()){
				if(b_1){
					track_1_ThirdParty = 1;
				}
			}
			if(nondet_bool()){
				if(b_2){
					track_2_ThirdParty = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 2 -----------------
		// <ThirdParty,TRUE,PatientWithTPC>
		//------------------------------------------------------------------
		if(track_0_ThirdParty || track_1_ThirdParty || track_2_ThirdParty){
			if(nondet_bool()){
				if(b_0){
					track_0_PatientWithTPC = 1;
				}
			}
			if(nondet_bool()){
				if(b_1){
					track_1_PatientWithTPC = 1;
				}
			}
			if(nondet_bool()){
				if(b_2){
					track_2_PatientWithTPC = 1;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 0 ---------------------
		// <ThirdParty,PatientWithTPC>
		//------------------------------------------------------------------
		if(track_0_ThirdParty || track_1_ThirdParty || track_2_ThirdParty){
			if(nondet_bool()){
				if(b_0 && track_0_PatientWithTPC){
					track_0_PatientWithTPC = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_PatientWithTPC){
					track_1_PatientWithTPC = 0;
				}
			}
			if(nondet_bool()){
				if(b_2 && track_2_PatientWithTPC){
					track_2_PatientWithTPC = 0;
				}
			}
		}
		//---------------Error------------
		if(track_0_target==1 || track_1_target==1 || track_2_target==1){
			assert(0);
		}
	}

}