smg

// parameters
const int n_resources = 3;
const int n_tasks = 2;
const int n_sensors = 4;


// sensor resources
const int resource1=1;
const int resource2=2;
const int resource3=3;
const int resource4=1;

// network configuration
const int e12=1;
const int e13=1;
const int e14=1;

const int e21=e12;
const int e23=1;
const int e24=1;

const int e31=e13;
const int e32=e23;
const int e34=1;

const int e41=e14;
const int e42=e24;
const int e43=e34;

player p0 controller, [str1], [str2], [str3], [str4] endplayer
module controller // schedules the algorithm

	// algorithm status
	status : [-1..7];

	// task resource indicator variables
	t1_r1 : [0..1];
	t1_r2 : [0..1];
	t1_r3 : [0..1];
	
	t2_r1 : [0..1];
	t2_r2 : [0..1];
	t2_r3 : [0..1];

	// schedule placeholders
	turn1 : [0..n_sensors];
	turn2 : [0..n_sensors];
	turn3 : [0..n_sensors];
	turn4 : [0..n_sensors];
	turn5 : [0..n_sensors];
	
	[to_remove] status=-1 -> (status'=0);

	// selecting schedule uniformly at random
	[] status=0 ->  1/24 : (turn1'=1) & (turn2'=2) & (turn3'=3) & (turn4'=4) & (status'=1)
		 + 1/24 : (turn1'=1) & (turn2'=2) & (turn3'=4) & (turn4'=3) & (status'=1)
		 + 1/24 : (turn1'=1) & (turn2'=3) & (turn3'=2) & (turn4'=4) & (status'=1)
		 + 1/24 : (turn1'=1) & (turn2'=3) & (turn3'=4) & (turn4'=2) & (status'=1)
		 + 1/24 : (turn1'=1) & (turn2'=4) & (turn3'=2) & (turn4'=3) & (status'=1)
		 + 1/24 : (turn1'=1) & (turn2'=4) & (turn3'=3) & (turn4'=2) & (status'=1)
		 + 1/24 : (turn1'=2) & (turn2'=1) & (turn3'=3) & (turn4'=4) & (status'=1)
		 + 1/24 : (turn1'=2) & (turn2'=1) & (turn3'=4) & (turn4'=3) & (status'=1)
		 + 1/24 : (turn1'=2) & (turn2'=3) & (turn3'=1) & (turn4'=4) & (status'=1)
		 + 1/24 : (turn1'=2) & (turn2'=3) & (turn3'=4) & (turn4'=1) & (status'=1)
		 + 1/24 : (turn1'=2) & (turn2'=4) & (turn3'=1) & (turn4'=3) & (status'=1)
		 + 1/24 : (turn1'=2) & (turn2'=4) & (turn3'=3) & (turn4'=1) & (status'=1)
		 + 1/24 : (turn1'=3) & (turn2'=1) & (turn3'=2) & (turn4'=4) & (status'=1)
		 + 1/24 : (turn1'=3) & (turn2'=1) & (turn3'=4) & (turn4'=2) & (status'=1)
		 + 1/24 : (turn1'=3) & (turn2'=2) & (turn3'=1) & (turn4'=4) & (status'=1)
		 + 1/24 : (turn1'=3) & (turn2'=2) & (turn3'=4) & (turn4'=1) & (status'=1)
		 + 1/24 : (turn1'=3) & (turn2'=4) & (turn3'=1) & (turn4'=2) & (status'=1)
		 + 1/24 : (turn1'=3) & (turn2'=4) & (turn3'=2) & (turn4'=1) & (status'=1)
		 + 1/24 : (turn1'=4) & (turn2'=1) & (turn3'=2) & (turn4'=3) & (status'=1)
		 + 1/24 : (turn1'=4) & (turn2'=1) & (turn3'=3) & (turn4'=2) & (status'=1)
		 + 1/24 : (turn1'=4) & (turn2'=2) & (turn3'=1) & (turn4'=3) & (status'=1)
		 + 1/24 : (turn1'=4) & (turn2'=2) & (turn3'=3) & (turn4'=1) & (status'=1)
		 + 1/24 : (turn1'=4) & (turn2'=3) & (turn3'=1) & (turn4'=2) & (status'=1)
		 + 1/24 : (turn1'=4) & (turn2'=3) & (turn3'=2) & (turn4'=1) & (status'=1);


	// initialising non-empty tasks uniformly at random
	[] status=1 -> 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2);

	// executing the schedule

	// 1st round
	[str1] status=2 & turn1=1 -> (status'=2);
	[fin1] status=2 & turn1=1 -> (status'=3);
	[str2] status=2 & turn1=2 -> (status'=2);
	[fin2] status=2 & turn1=2 -> (status'=3);
	[str3] status=2 & turn1=3 -> (status'=2);
	[fin3] status=2 & turn1=3 -> (status'=3);
	[str4] status=2 & turn1=4 -> (status'=2);
	[fin4] status=2 & turn1=4 -> (status'=3);

	// 2nd round
	[str1] status=3 & turn2=1 -> (status'=3);
	[fin1] status=3 & turn2=1 -> (status'=4);
	[str2] status=3 & turn2=2 -> (status'=3);
	[fin2] status=3 & turn2=2 -> (status'=4);
	[str3] status=3 & turn2=3 -> (status'=3);
	[fin3] status=3 & turn2=3 -> (status'=4);
	[str4] status=3 & turn2=4 -> (status'=3);
	[fin4] status=3 & turn2=4 -> (status'=4);

	// 3rd round
	[str1] status=4 & turn3=1 -> (status'=4);
	[fin1] status=4 & turn3=1 -> (status'=5);
	[str2] status=4 & turn3=2 -> (status'=4);
	[fin2] status=4 & turn3=2 -> (status'=5);
	[str3] status=4 & turn3=3 -> (status'=4);
	[fin3] status=4 & turn3=3 -> (status'=5);
	[str4] status=4 & turn3=4 -> (status'=4);
	[fin4] status=4 & turn3=4 -> (status'=5);

	// 4th round
	[str1] status=5 & turn4=1 -> (status'=5);
	[fin1] status=5 & turn4=1 -> (status'=6);
	[str2] status=5 & turn4=2 -> (status'=5);
	[fin2] status=5 & turn4=2 -> (status'=6);
	[str3] status=5 & turn4=3 -> (status'=5);
	[fin3] status=5 & turn4=3 -> (status'=6);
	[str4] status=5 & turn4=4 -> (status'=5);
	[fin4] status=5 & turn4=4 -> (status'=6);

	[] status=6 -> (status'=7);
	[] status=7 -> true;


endmodule

player p1 sensor1, [fin1],[init1_1] ,[init1_2], [join1_1], [join1_2], [to_remove] endplayer
module sensor1

	state1 : [0..3];

	// team membership indicators
	m1_t1 : [0..1];
	m1_t2 : [0..1];

	// task scheduling
	turn1_1 : [0..n_tasks];
	turn2_1 : [0..n_tasks];

	[to_remove] status=-1 -> true;

	// starting turn, selecting order of tasks
	[str1] state1=0 -> (state1'=1);

	// if there is no team and has required skill - initiating the team
	[init1_1] state1=1 & !committed & team_size_t1=0 & has_resource_t1 -> (m1_t1'=1);
	[init1_2] state1=1 & !committed & team_size_t2=0 & has_resource_t2 -> (m1_t2'=1);

	// if team already exists and one of the neighbours is in it - joining the team 
	[join1_1] state1=1 & !committed & team_size_t1>0 & can_join_t1 & has_resource_t1 & !resource_filled_t1 -> (m1_t1'=1);
	[join1_2] state1=1 & !committed & team_size_t2>0 & can_join_t2 & has_resource_t2 & !resource_filled_t2 -> (m1_t2'=1);
	
	[fin1] state1>0 -> (state1'=0); 

endmodule

player p2 sensor2, [fin2],[init2_1] ,[init2_2], [join2_1], [join2_2] endplayer
module sensor2 = sensor1 
[ 
	state1=state2, 

	str1=str2,
	fin1=fin2,

	m1_t1=m2_t1,
	m1_t2=m2_t2,

	m2_t1=m1_t1,
	m2_t2=m1_t2,

	turn1_1=turn1_2,
	turn2_1=turn2_2,

	resource1=resource2,	
	resource2=resource1,

	e12=e21,
	e13=e23,
	e14=e24,
	e15=e25,

	e21=e12,
	e23=e13,
	e24=e14,
	e25=e15,
	init1_1=init2_1,
	init1_2=init2_2,
	join1_1=join2_1,
	join1_2=join2_2
] 
endmodule

player p3 sensor3, [fin3], [init3_1] ,[init3_2], [join3_1], [join3_2] endplayer
module sensor3 = sensor1 
[ 
	state1=state3, 

	str1=str3,
	fin1=fin3,

	m1_t1=m3_t1,
	m1_t2=m3_t2,
	m3_t1=m1_t1,
	m3_t2=m1_t2,
	turn1_1=turn1_3,
	turn2_1=turn2_3,

	resource1=resource3,	
	resource3=resource1,

	e12=e32,
	e13=e31,
	e14=e34,
	e15=e35,

	e31=e13,
	e32=e12,
	e34=e14,
	e35=e15,
	
	init1_1=init3_1,
	init1_2=init3_2,
	join1_1=join3_1,
	join1_2=join3_2
] 
endmodule

player p4 sensor4, [fin4], [init4_1] ,[init4_2], [join4_1], [join4_2] endplayer
module sensor4 = sensor1 
[ 
	state1=state4, 

	str1=str4,
	fin1=fin4,

	m1_t1=m4_t1,
	m1_t2=m4_t2,

	m4_t1=m1_t1,
	m4_t2=m1_t2,

	turn1_1=turn1_4,
	turn2_1=turn2_4,

	resource1=resource4,	
	resource4=resource1,

	e12=e42,
	e13=e43,
	e14=e41,
	e15=e45,

	e41=e14,
	e42=e12,
	e43=e13,
	e45=e15,
	
	init1_1=init4_1,
	init1_2=init4_2,
	join1_1=join4_1,
	join1_2=join4_2
] 
endmodule



// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;

// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2;

// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 > 0;

// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );

// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4);

// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))) / (e12+e13+e14);




// labels and formulae for property specification 
formula finished = (status=6);


formula task1_completed = finished 
		 	 & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1)))
			 & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2)))
			 & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3)));

formula task2_completed = finished
			 & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1)))
			 & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2)))
			 & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3)));


formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1);

formula agent2_joins_successful_team = (task1_completed & m2_t1=1) | (task2_completed & m2_t2=1);

formula agent3_joins_successful_team = (task1_completed & m3_t1=1) | (task2_completed & m3_t2=1);

formula agent4_joins_successful_team = (task1_completed & m4_t1=1) | (task2_completed & m4_t2=1);


// rewards
rewards "w_1_total"
    agent1_joins_successful_team : 1;
    agent2_joins_successful_team : 1;
    agent3_joins_successful_team : 1;
    agent4_joins_successful_team : 1;
endrewards

rewards "w_2_total"
    task1_completed : 1;
    task2_completed : 1;
endrewards

rewards "penalties"

[str1] true: 1;
[init1_1] true: 1;
[init1_2] true: 1;
[join1_1] true: 1;
[join1_2] true: 1;
[fin1] true: 1;

endrewards