% @specification(Subtype_agent_Unsafe)
% @channel_model(CCM)
% @connector(name=ASLan++ Connector, version=0.5.9)
% @connector_options(-gas, -opt=LUMP, -hc=ALL)
section signature:
	agent > agent0
	message > channel
	ak : agent -> public_key
	check_step_reached : nat * nat -> fact
	child : nat * nat -> fact
	ck : agent -> public_key
	defaultPseudonym : agent * nat -> agent
	descendant : nat * nat -> fact
	dishonest : agent -> fact
	pk : agent -> public_key
	state_Agent0 : agent0 * nat * nat * agent0 * message -> fact
	state_Environment : agent * nat * nat -> fact
section types:
	A0 : agent0
	Actor : agent
	Ak_arg_1 : agent
	Ck_arg_1 : agent
	Descendant_arg_1 : nat
	Descendant_arg_2 : nat
	Descendant_arg_3 : nat
	E_A0_Actor : agent0
	E_A0_IID : nat
	E_A0_SL : nat
	IID : nat
	IID_1 : nat
	Pk_arg_1 : agent
	Reached : message
	SL : nat
	a0 : agent0
	atag : text
	ctag : text
	dummy_agent : agent
	dummy_agent0 : agent0
	dummy_message : message
	dummy_nat : nat
	false : fact
	stag : text
	true : fact
section inits:
initial_state init :=
	dishonest(i).
	iknows(a0).
	iknows(atag).
	iknows(ctag).
	iknows(i).
	iknows(inv(ak(i))).
	iknows(inv(ck(i))).
	iknows(inv(pk(i))).
	iknows(stag).
	state_Environment(dummy_agent, dummy_nat, 1).
	true
section hornClauses:
hc public_ck(Ck_arg_1) :=
	iknows(ck(Ck_arg_1)) :-
		iknows(Ck_arg_1)
hc public_ak(Ak_arg_1) :=
	iknows(ak(Ak_arg_1)) :-
		iknows(Ak_arg_1)
hc public_pk(Pk_arg_1) :=
	iknows(pk(Pk_arg_1)) :-
		iknows(Pk_arg_1)
hc descendant_closure(Descendant_arg_1, Descendant_arg_2, Descendant_arg_3) :=
	descendant(Descendant_arg_1, Descendant_arg_3) :-
		descendant(Descendant_arg_1, Descendant_arg_2),
		descendant(Descendant_arg_2, Descendant_arg_3)
hc descendant_direct(Descendant_arg_1, Descendant_arg_2) :=
	descendant(Descendant_arg_1, Descendant_arg_2) :-
		child(Descendant_arg_1, Descendant_arg_2)
section rules:
% @new_instance(id=1, line=23, entity=Environment, child=Agent0, E_A0_Actor=a0)
step step_1_Environment__line_23(Actor, IID, IID_1) :=
	state_Environment(Actor, IID, 1)
	=[exists IID_1]=>
	child(IID, IID_1).
	state_Agent0(a0, IID_1, 1, dummy_agent0, dummy_message).
	state_Environment(Actor, IID, 2)
% @assignment(id=2, line=18, entity=Agent0, A0=E_A0_Actor)
%introduce facts due to lumping
%check_step_reached(E_A0_IID,)
step step_2_Agent0__line_18(A0, E_A0_Actor, E_A0_IID, Reached) :=
	not(dishonest(E_A0_Actor)).
	state_Agent0(E_A0_Actor, E_A0_IID, 1, A0, Reached)
	=>
	check_step_reached(E_A0_IID, 3).
	state_Agent0(E_A0_Actor, E_A0_IID, 3, E_A0_Actor, Reached)
%retract facts
%check_step_reached(E_A0_IID,)
step step_3_Agent0__line_19(A0, E_A0_Actor, E_A0_IID, Reached) :=
	check_step_reached(E_A0_IID, 3).
	state_Agent0(E_A0_Actor, E_A0_IID, 3, A0, Reached)
	=>
	state_Agent0(E_A0_Actor, E_A0_IID, 4, A0, Reached)
section goals:
attack_state step_reached(E_A0_IID, E_A0_SL) :=
	check_step_reached(E_A0_IID, E_A0_SL).
	not(false)