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

//---------- VARIABLES DECLARATION ---------
int	track_0_target,
	track_0_anyfour1,
	track_0_SUPER_ROLE,
	track_0_ToCheckRole,
	track_0_TargetPrime,
	track_1_target,
	track_1_anyfour1,
	track_1_SUPER_ROLE,
	track_1_ToCheckRole,
	track_1_TargetPrime,
	b_0,
	b_1;

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

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

	track_0_target = 0;
	track_0_anyfour1 = 0;
	track_0_SUPER_ROLE = 0;
	track_0_ToCheckRole = 0;
	track_0_TargetPrime = 0;
	track_1_target = 0;
	track_1_anyfour1 = 0;
	track_1_SUPER_ROLE = 0;
	track_1_ToCheckRole = 0;
	track_1_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;
		}
		else if (!b_1) {
			b_1 = 1;
			track_1_SUPER_ROLE = 1;
			track_1_ToCheckRole = 1;
		}
	}

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

	//---------- SIMULATION OF RULES ---------
	while(1){
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <SUPER_ROLE,TRUE,anyfour1>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0){
					track_0_anyfour1 = 1;
				}
			}
			if(nondet_bool()){
				if(b_1){
					track_1_anyfour1 = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 1 -----------------
		// <SUPER_ROLE,anyfour1,target>
		//------------------------------------------------------------------
		if(track_0_SUPER_ROLE || track_1_SUPER_ROLE){
			if(nondet_bool()){
				if(b_0 && track_0_anyfour1){
					track_0_target = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_anyfour1){
					track_1_target = 1;
				}
			}
		}
		//------------------ CAN_ASSIGN RULE NUMBER 2 -----------------
		// <ToCheckRole,ToCheckRole&target,TargetPrime>
		//------------------------------------------------------------------
		if(track_0_ToCheckRole || track_1_ToCheckRole){
			if(nondet_bool()){
				if(b_0 && track_0_ToCheckRole && track_0_target){
					track_0_TargetPrime = 1;
				}
			}
			if(nondet_bool()){
				if(b_1 && track_1_ToCheckRole && track_1_target){
					track_1_TargetPrime = 1;
				}
			}
		}
		//---------------Error------------
		if(track_0_TargetPrime==1 || track_1_TargetPrime==1){
			assert(0);
		}
	}

}