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

//---------- VARIABLES DECLARATION ---------
int	track_0_target,
	track_0_SUPER_ROLE,
	track_0_ToCheckRole,
	track_0_TargetPrime,
	b_0;

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

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

	track_0_target = 0;
	track_0_SUPER_ROLE = 0;
	track_0_ToCheckRole = 0;
	track_0_TargetPrime = 0;

	//---------- CONFIGURATION_USERS ---------
	//Configuration of SUPER_USER
	if (nondet_bool()){
		if (!b_0) {
			b_0 = 1;
			track_0_SUPER_ROLE = 1;
			track_0_ToCheckRole = 1;
		}
	}

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

	//---------- SIMULATION OF RULES ---------
	while(1){
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <ToCheckRole,ToCheckRole&target,TargetPrime>
		//------------------------------------------------------------------
		if(track_0_ToCheckRole){
			if(nondet_bool()){
				if(b_0 && track_0_ToCheckRole && track_0_target){
					track_0_TargetPrime = 1;
				}
			}
		}
		//---------------Error------------
		if(track_0_TargetPrime==1){
			assert(0);
		}
	}

}