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

//---------- VARIABLES DECLARATION ---------
int	track_0_Nurse,
	track_0_target,
	track_0_SUPER_ROLE,
	track_1_Nurse,
	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_Nurse = 0;
	track_0_target = 0;
	track_0_SUPER_ROLE = 0;
	track_1_Nurse = 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 user131
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_Nurse = 1;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_Nurse = 1;
		}
	}

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

	//---------- SIMULATION OF RULES ---------
	while(1){
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <SUPER_ROLE,Nurse,target>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_Nurse){
					track_0_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Nurse){
					track_1_target = 1;
				}
			}
		}
		//------------------- CAN_REVOKE RULE NUMBER 0 ---------------------
		// <SUPER_ROLE,Nurse>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_Nurse){
					track_0_Nurse = 0;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_Nurse){
					track_1_Nurse = 0;
				}
			}
		}
		//---------------Error------------
		if(track_0_target==1 || track_1_target==1){
			assert(0);
		}
	}

}