// intrusion detection CSG model taken from
// Dynamic Policy-Based IDS Configuration 
// Quanyan Zhu and Tamer Basar
// gxn 20/03/18

const int scenario; // 1 or 2

// scenario 1:
// - small chance an attack is successful
// - high chance of recovering to healthy if attack is prevented
// - small chance of failure from compromised state (if attack continues)
// - high change that we repair from failure to compromised when attack stops

// scenario 2:
// - high chance an attack is successful
// - small chance of recovering to healthy if attack is prevented
// - high chance of failure from compromised state (if attack continues)
// - small change that we repair from failure to compromised when attack stops

const double attack = scenario=1 ? 0.2 : 0.8;
const double recover = scenario=1 ? 0.8 : 0.2;
const double fail = scenario=1 ? 0.2 : 0.8;
const double repair = scenario=1 ? 0.8 : 0.2;

csg

player policy policy endplayer
player attacker attacker endplayer

const int rounds; // number of rounds

module rounds

	r : [0..rounds]; // current time-step
	
	[] r<rounds -> (r'=r+1);
	[] r=rounds -> true;
	
endmodule

module csystem

	s : [1..3]; // system state
	// 1 - healthy
	// 2 - compromised
	// 3 - failure
	
	[defend1,attack1] s=1 -> (s'=1);
	[defend1,attack2] s=1 -> 1-attack : (s'=1) + attack : (s'=2);
	[defend2,attack1] s=1 -> 1-attack : (s'=1) + attack : (s'=2);
	[defend2,attack2] s=1 -> (s'=1);

	[defend1,attack1] s=2 -> recover : (s'=1) + 1-recover : (s'=2);
	[defend1,attack2] s=2 -> 1-fail : (s'=2) + fail : (s'=3);
	[defend2,attack1] s=2 -> 1-fail : (s'=2) + fail : (s'=3);
	[defend2,attack2] s=2 -> recover : (s'=1) + 1-recover : (s'=2);

	[defend1,attack1] s=3 -> repair : (s'=2) + 1-repair : (s'=3);
	[defend1,attack2] s=3 -> (s'=3);
	[defend2,attack1] s=3 -> (s'=3);
	[defend2,attack2] s=3 -> repair : (s'=2) + 1-repair : (s'=3);

endmodule

module policy
	
	[defend1] r<rounds -> true;
	[defend2] r<rounds -> true;

endmodule

module attacker
	
	[attack1] r<rounds -> true;
	[attack2] r<rounds -> true;
	
endmodule

rewards "damage"
	[defend1,attack1] s=1 : 0;
	[defend1,attack2] s=1 : 1;
	[defend2,attack1] s=1 : 0.5;
	[defend2,attack2] s=1 : 0;
	[defend1,attack1] s=2 : 1;
	[defend1,attack2] s=2 : 2;
	[defend2,attack1] s=2 : 1.5;
	[defend2,attack2] s=2 : 1;
	[defend1,attack1] s=3 : 1;
	[defend1,attack2] s=3 : 3;
	[defend2,attack1] s=3 : 2.5;
	[defend2,attack2] s=3 : 1;
endrewards	

const K;

rewards "i_damage"
	[defend1,attack1] r=K-1 & s=1 : 0;
	[defend1,attack2] r=K-1 & s=1 : 1;
	[defend2,attack1] r=K-1 & s=1 : 0.5;
	[defend2,attack2] r=K-1 & s=1 : 0;
	[defend1,attack1] r=K-1 & s=2 : 1;
	[defend1,attack2] r=K-1 & s=2 : 2;
	[defend2,attack1] r=K-1 & s=2 : 1.5;
	[defend2,attack2] r=K-1 & s=2 : 1;
	[defend1,attack1] r=K-1 & s=3 : 1;
	[defend1,attack2] r=K-1 & s=3 : 3;
	[defend2,attack1] r=K-1 & s=3 : 2.5;
	[defend2,attack2] r=K-1 & s=3 : 1;
endrewards