//-------- DECLARE VARIBLES ----------//
var	b_target : int ,
	b_anyfour1 : int ,
	b_anyfour2 : int ,
	b_anyfour3 : int ,
	b_anyfour4 : int ,
	b_SUPER_ROLE : int ,
	d_target : int ,
	d_anyfour1 : int ,
	d_anyfour2 : int ,
	d_anyfour3 : int ,
	d_anyfour4 : int ,
	d_SUPER_ROLE : int ,
	n_SUPER_ROLE : int ,
	n_anyfour1_anyfour2_anyfour3_anyfour4 : int ,
	n_target : int ;

//-------------- BEGIN Program --------------------//
begin
	//-------------- Init VARS ------------------------//
	b_target = 0;
	b_anyfour1 = 0;
	b_anyfour2 = 0;
	b_anyfour3 = 0;
	b_anyfour4 = 0;
	b_SUPER_ROLE = 0;
	d_target = 0;
	d_anyfour1 = 0;
	d_anyfour2 = 0;
	d_anyfour3 = 0;
	d_anyfour4 = 0;
	d_SUPER_ROLE = 0;
	n_SUPER_ROLE = 0;
	n_anyfour1_anyfour2_anyfour3_anyfour4 = 0;
	n_target = 0;
	// Initialize track variables in the system
	n_SUPER_ROLE = n_SUPER_ROLE + 1;

	while ( true )  do 

		//----- Non-deterministic assignment ------//
		b_target = random; assume b_target >= 0 and b_target <= 1;
		b_anyfour1 = random; assume b_anyfour1 >= 0 and b_anyfour1 <= 1;
		b_anyfour2 = random; assume b_anyfour2 >= 0 and b_anyfour2 <= 1;
		b_anyfour3 = random; assume b_anyfour3 >= 0 and b_anyfour3 <= 1;
		b_anyfour4 = random; assume b_anyfour4 >= 0 and b_anyfour4 <= 1;
		b_SUPER_ROLE = random; assume b_SUPER_ROLE >= 0 and b_SUPER_ROLE <= 1;

		d_target = random; assume d_target >= 0 and d_target <= 1;
		d_anyfour1 = random; assume d_anyfour1 >= 0 and d_anyfour1 <= 1;
		d_anyfour2 = random; assume d_anyfour2 >= 0 and d_anyfour2 <= 1;
		d_anyfour3 = random; assume d_anyfour3 >= 0 and d_anyfour3 <= 1;
		d_anyfour4 = random; assume d_anyfour4 >= 0 and d_anyfour4 <= 1;
		d_SUPER_ROLE = random; assume d_SUPER_ROLE >= 0 and d_SUPER_ROLE <= 1;

		//-------------- Simulation -------------------//
		//------------------ CAN_ASSIGN RULE NUMBER 0 -----------------
		// <SUPER_ROLE,TRUE,anyfour1>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0) then
			if(b_anyfour2==1 and b_anyfour3==1 and b_anyfour4==1) then
				n_anyfour1_anyfour2_anyfour3_anyfour4 = n_anyfour1_anyfour2_anyfour3_anyfour4+1;
			endif;
		endif;

		//------------------ CAN_ASSIGN RULE NUMBER 1 -----------------
		// <SUPER_ROLE,TRUE,anyfour2>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0) then
			if(b_anyfour1==1 and b_anyfour3==1 and b_anyfour4==1) then
				n_anyfour1_anyfour2_anyfour3_anyfour4 = n_anyfour1_anyfour2_anyfour3_anyfour4+1;
			endif;
		endif;

		//------------------ CAN_ASSIGN RULE NUMBER 2 -----------------
		// <SUPER_ROLE,TRUE,anyfour3>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0) then
			if(b_anyfour1==1 and b_anyfour2==1 and b_anyfour4==1) then
				n_anyfour1_anyfour2_anyfour3_anyfour4 = n_anyfour1_anyfour2_anyfour3_anyfour4+1;
			endif;
		endif;

		//------------------ CAN_ASSIGN RULE NUMBER 3 -----------------
		// <SUPER_ROLE,TRUE,anyfour4>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0) then
			if(b_anyfour1==1 and b_anyfour2==1 and b_anyfour3==1) then
				n_anyfour1_anyfour2_anyfour3_anyfour4 = n_anyfour1_anyfour2_anyfour3_anyfour4+1;
			endif;
		endif;

		//------------------ CAN_ASSIGN RULE NUMBER 4 -----------------
		// <SUPER_ROLE,anyfour1&anyfour2&anyfour3&anyfour4,target>
		//------------------------------------------------------------------
		if(brandom and d_SUPER_ROLE==1 and n_SUPER_ROLE>0 and b_anyfour1==1 and b_anyfour2==1 and b_anyfour3==1 and b_anyfour4==1 and n_anyfour1_anyfour2_anyfour3_anyfour4>0) then
			if(true) then
				n_target = n_target+1;
			endif;
		endif;

		//------------ ERROR Query ---------------//
		if (n_target>0) then
			skip;
		endif;
	done;  //End while loop
end  //End main