// Example inspired from hallway. Safe a panicking human with robot with faulty mnoves.

// model type is stochastic multiplayer game
smg 

// set up players
player p1
	agent
endplayer

player p2
	human
endplayer

// set up globals

global turn : [1..2] init 1; // whose player's turn?

// set up constants

// dimension of grid
const int X_MAX = 5;
const int Y_MAX = 5;

module agent

	// position on grid
	x : [0..X_MAX-1] init 0;
	y : [0..Y_MAX-1] init 0;
	look : [0..3] init 0; // 0: N, 1: E, 2: S, 3: W
	dmg : bool init false; // is agent damaged?

	// local state
	s1: [0..2] init 0; // 0: check dmg, 1: move

	// check dmg

	[] turn=1 & s1=0 & dmg -> 0.5 : (turn'=2) + 0.5 : (s1'=1); // loose turn if dmg
	[] turn=1 & s1=0 & !dmg -> (s1'=1); // nothing happens if not dmg

	// movements - up to four directions possible

	// move forward
	// orientation N 
	[] turn=1 & s1=1 & look=0 -> 
		0.8 : (y'=min(y+1, Y_MAX-1)) & (turn'=2) & (s1'=0) +
		0.05 : (turn'=2) & (s1'=0) + 
		0.05 : (x'=max(x-1,0)) & (look'=3) & (turn'=2) & (s1'=0) + 
		0.05 : (x'=min(x+1,X_MAX-1)) & (look'=1) & (turn'=2) & (s1'=0) + 
		0.025 : (y'=max(y-1,0)) & (turn'=2) & (s1'=0) + 
		0.025 : (y'=max(y-1,0)) & (look'=2) & (turn'=2) & (s1'=0);
	// orientation E
	[] turn=1 & s1=1 & look=1 -> 
		0.8 : (x'=min(x+1, X_MAX-1)) & (turn'=2) & (s1'=0) +
		0.05 : (turn'=2) & (s1'=0) + 
		0.05 : (y'=min(y+1,Y_MAX-1)) & (look'=0) & (turn'=2) & (s1'=0) + 
		0.05 : (y'=max(y-1,0)) & (look'=2) & (turn'=2) & (s1'=0) + 
		0.025 : (x'=max(x-1,0)) & (turn'=2) & (s1'=0) + 
		0.025 : (x'=max(x-1,0)) & (look'=3) & (turn'=2) & (s1'=0);
	// orientation S
	[] turn=1 & s1=1 & look=2 -> 
		0.8 : (y'=max(y-1, 0)) & (turn'=2) & (s1'=0) +
		0.05 : (turn'=2) & (s1'=0) + 
		0.05 : (x'=min(y+1,Y_MAX-1)) & (look'=1) & (turn'=2) & (s1'=0) + 
		0.05 : (x'=max(x-1,0)) & (look'=3) & (turn'=2) & (s1'=0) + 
		0.025 : (y'=min(y+1,Y_MAX-1)) & (turn'=2) & (s1'=0) + 
		0.025 : (y'=min(y+1,Y_MAX-1)) & (look'=0) & (turn'=2) & (s1'=0);
	// orientation W
	[] turn=1 & s1=1 & look=3 -> 
		0.8 : (x'=max(x-1, 0)) & (turn'=2) & (s1'=0) +
		0.05 : (turn'=2) & (s1'=0) + 
		0.05 : (y'=max(y-1,0)) & (look'=2) & (turn'=2) & (s1'=0) + 
		0.05 : (y'=min(y+1,Y_MAX-1)) & (look'=0) & (turn'=2) & (s1'=0) + 
		0.025 : (x'=min(x+1,X_MAX-1)) & (turn'=2) & (s1'=0) + 
		0.025 : (x'=min(x+1,X_MAX-1)) & (look'=1) & (turn'=2) & (s1'=0);

	// or change orientation freely
	[] turn=1 & s1=1 -> (look'=0) &  (s1'=2);
	[] turn=1 & s1=1 -> (look'=1) &  (s1'=2);
	[] turn=1 & s1=1 -> (look'=2) &  (s1'=2);
	[] turn=1 & s1=1 -> (look'=3) &  (s1'=2);

	[] turn=1 & s1=2 ->
		0.01 : (turn'=2) & (s1'=0) & (dmg'=true) +
		0.99 : (turn'=2) & (s1'=0);

endmodule

module human
	
	// position on grid
	a : [0..X_MAX-1] init X_MAX-1;
	b : [0..Y_MAX-1] init Y_MAX-1;

	// local state
        s2 : [0..1] init 0; // 0: move random?, 1: move panically

	// make a random move with probability 0.5
	[] turn=2 & s2=0 ->
		0.125: (a'=min(a+1,X_MAX-1)) & (turn'=1) & (s2'=0)// right
		+ 0.125: (a'=max(a-1,0)) & (turn'=1) & (s2'=0) // left
		+ 0.125: (b'=min(b+1,X_MAX-1)) & (turn'=1) & (s2'=0) // up
		+ 0.125: (b'=max(b-1,0)) & (turn'=1) & (s2'=0) // down
		+ 0.5: (s2'=1);

	// otherwise move non-deterministically (panic)

	// right
	[] turn=2 & s2=1 -> (a'=min(a+1,X_MAX-1)) & (turn'=1) & (s2'=0);
	// left
	[] turn=2 & s2=1 -> (a'=max(a-1,0)) & (turn'=1) & (s2'=0);
	//up
	[] turn=2 & s2=1 -> (b'=min(b+1,X_MAX-1)) & (turn'=1) & (s2'=0);
	// down
	[] turn=2 & s2=1 -> (b'=max(b-1,0)) & (turn'=1) & (s2'=0);
        // nothing
        [] turn=2 & s2=1 -> (turn'=1) & (s2'=0);

endmodule

label "saved" = x=a & y=b;
label "damaged" = dmg;