section signature:

	user_to_role : user * role -> fact
	poto : userORrole * taskName -> fact
	task_to_data : taskName * set * set -> fact
	aknows : entity * data -> fact
	mc_pair : data * data -> data
	contains : set * data -> fact
	task : taskName * nat -> taskInstance
	canExecute : user * role * humanTaskName -> fact
	granted : user * role * taskInstance -> fact
	executed : user * taskInstance -> fact
	ready : taskInstance -> fact
	done : taskInstance -> fact
	entity > organization
	entity > user
	data > object
	data > set
	userORrole > user
	userORrole > role
	taskName > automatedTaskName
	taskName > humanTaskName

section types:

	start_event_startevent1,parallelgateway1_to_usertask3,parallelgateway1_to_servicetask2,parallelgateway4_to_usertask5,exclusivegateway1_to_usertask8,exclusivegateway1_to_exclusivegateway2,exclusivegateway2_to_usertask9,exclusivegateway3_to_parallelgateway1,exclusivegateway4_to_usertask7,exclusivegateway4_to_exclusivegateway3: fact
	HT,usertask1,usertask2,usertask3,usertask4,usertask5,usertask6,usertask7,usertask8,usertask9: humanTaskName
	IN,OUT,in_usertask1,out_usertask1,in_usertask2,out_usertask2,in_usertask3,out_usertask3,in_servicetask2,out_servicetask2,in_usertask4,out_usertask4,in_usertask5,out_usertask5,in_usertask6,out_usertask6,in_usertask7,out_usertask7,in_usertask8,out_usertask8,in_usertask9,out_usertask9: set
	manager,supervisor,clerk,R: role
	N,N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16,N17,N18,N19,N20,N21,N22,N23,N24,N25,N26,N27,N28,N29,N30,N31,N32,N33,N34,N35,N36,N37,N38,N39,N40,N41,N42: nat
	AT,servicetask2: automatedTaskName
	user1_manager,user2_manager,user1_supervisor,user2_supervisor,user1_clerk,user2_clerk,A,U0,U1: user

section inits:

	initial_state init_1 :=

		user_to_role(user1_manager,manager).
		user_to_role(user2_manager,manager).
		user_to_role(user1_supervisor,supervisor).
		user_to_role(user2_supervisor,supervisor).
		user_to_role(user1_clerk,clerk).
		user_to_role(user2_clerk,clerk).
		start_event_startevent1.
		task_to_data(usertask1,in_usertask1,out_usertask1).
		task_to_data(usertask2,in_usertask2,out_usertask2).
		task_to_data(usertask3,in_usertask3,out_usertask3).
		task_to_data(servicetask2,in_servicetask2,out_servicetask2).
		task_to_data(usertask4,in_usertask4,out_usertask4).
		task_to_data(usertask5,in_usertask5,out_usertask5).
		task_to_data(usertask6,in_usertask6,out_usertask6).
		task_to_data(usertask7,in_usertask7,out_usertask7).
		task_to_data(usertask8,in_usertask8,out_usertask8).
		task_to_data(usertask9,in_usertask9,out_usertask9)

section hornClauses:

	hc rbac_ac (A,R,HT) := canExecute(A,R,HT) :- user_to_role(A,R), poto(R,HT)
	hc direct_ac (A,R,HT) := canExecute(A,R,HT) :- user_to_role(A,R), poto(A,HT)
	hc poto_usertask1:= poto(clerk,usertask1)
	hc poto_usertask2:= poto(supervisor,usertask2)
	hc poto_usertask3:= poto(supervisor,usertask3)
	hc poto_usertask4:= poto(supervisor,usertask4)
	hc poto_usertask5:= poto(supervisor,usertask5)
	hc poto_usertask6:= poto(manager,usertask6)
	hc poto_usertask7:= poto(manager,usertask7)
	hc poto_usertask8:= poto(clerk,usertask8)
	hc poto_usertask9:= poto(clerk,usertask9)

section rules:

	step authorizeTaskExecution(A,R,HT,N) := canExecute(A,R,HT). ready(task(HT,N)) => granted(A,R,task(HT,N))
	step h_taskExecution(A,R,HT,N,IN,OUT) := granted(A,R,task(HT,N)). task_to_data(HT,IN,OUT) => executed(A,task(HT,N)). done(task(HT,N)). task_to_data(HT,IN,OUT). aknows(A,IN). aknows(A,OUT)
	step atask_execution(AT,N,IN,OUT) := ready(task(AT,N)). task_to_data(AT,IN,OUT) => done(task(AT,N)). task_to_data(AT,IN,OUT)
	step w_usertask1(N0) := start_event_startevent1=[exists N0] => ready(task(usertask1,N0))
	step w_usertask2(N2,N1) := done(task(usertask1,N2))=[exists N1] => ready(task(usertask2,N1))
	step w_parallelgateway1 := exclusivegateway3_to_parallelgateway1 => parallelgateway1_to_usertask3. parallelgateway1_to_servicetask2
	step w_usertask3(N3) := parallelgateway1_to_usertask3=[exists N3] => ready(task(usertask3,N3))
	step w_servicetask2(N4) := parallelgateway1_to_servicetask2=[exists N4] => ready(task(servicetask2,N4))
	step w_usertask4(N6,N5) := done(task(servicetask2,N6))=[exists N5] => ready(task(usertask4,N5))
	step w_parallelgateway4(N7,N8) := done(task(usertask3,N7)). done(task(usertask4,N8)) => parallelgateway4_to_usertask5
	step w_usertask5(N9) := parallelgateway4_to_usertask5=[exists N9] => ready(task(usertask5,N9))
	step w_usertask6(N11,N10) := done(task(usertask5,N11))=[exists N10] => ready(task(usertask6,N10))
	step w_usertask7(N12) := exclusivegateway4_to_usertask7=[exists N12] => ready(task(usertask7,N12))
	step exclusivegateway1_branch1(N13) := done(task(usertask7,N13)) => exclusivegateway1_to_usertask8
	step exclusivegateway1_branch2(N13) := done(task(usertask7,N13)) => exclusivegateway1_to_exclusivegateway2
	step w_usertask8(N14) := exclusivegateway1_to_usertask8=[exists N14] => ready(task(usertask8,N14))
	step exclusivegateway2_branch1(N15) := done(task(usertask8,N15)) => exclusivegateway2_to_usertask9
	step exclusivegateway2_branch2 := exclusivegateway1_to_exclusivegateway2 => exclusivegateway2_to_usertask9
	step w_usertask9(N16) := exclusivegateway2_to_usertask9=[exists N16] => ready(task(usertask9,N16))
	step exclusivegateway3_branch1(N41) := done(task(usertask2,N41)) => exclusivegateway3_to_parallelgateway1
	step exclusivegateway3_branch2 := exclusivegateway4_to_exclusivegateway3 => exclusivegateway3_to_parallelgateway1
	step exclusivegateway4_branch1(N42) := done(task(usertask6,N42)) => exclusivegateway4_to_usertask7
	step exclusivegateway4_branch2(N42) := done(task(usertask6,N42)) => exclusivegateway4_to_exclusivegateway3

section goals:

	attack_state sod_securitySod1_1(U0,N17,N18,N19):=  executed(U0,task(usertask5,N17)).  executed(U0,task(usertask6,N18)).  executed(U0,task(usertask7,N19))
	attack_state sod_securitySod1_2(U0,U1,N20,N21,N22):=  executed(U0,task(usertask6,N20)).  executed(U0,task(usertask7,N21)).  executed(U1,task(usertask5,N22))
	attack_state sod_securitySod1_3(U0,U1,N23,N24,N25):=  executed(U0,task(usertask5,N23)).  executed(U0,task(usertask6,N24)).  executed(U1,task(usertask7,N25))
	attack_state sod_securitySod1_4(U0,U1,N26,N27,N28):=  executed(U0,task(usertask5,N26)).  executed(U0,task(usertask7,N27)).  executed(U1,task(usertask6,N28))
	attack_state sod_securitySod2_1(U0,N29,N30,N31):=  executed(U0,task(usertask4,N29)).  executed(U0,task(usertask5,N30)).  executed(U0,task(usertask3,N31))
	attack_state sod_securitySod2_2(U0,U1,N32,N33,N34):=  executed(U0,task(usertask4,N32)).  executed(U0,task(usertask3,N33)).  executed(U1,task(usertask5,N34))
	attack_state sod_securitySod2_3(U0,U1,N35,N36,N37):=  executed(U0,task(usertask4,N35)).  executed(U0,task(usertask5,N36)).  executed(U1,task(usertask3,N37))
	attack_state sod_securitySod2_4(U0,U1,N38,N39,N40):=  executed(U0,task(usertask5,N38)).  executed(U0,task(usertask3,N39)).  executed(U1,task(usertask4,N40))