// non-repudiation protocol (with malicious recipient) 
// Markowitch & Roggeman [MR99]
// simple POMDP model (no timing)
// malicious recipient
// gxn 04/09/14

pomdp

// observable variables (N is hidden)
observables
        last, r, mess, ack, o
endobservables

// constants
const K; // range N is chosen over

module originator

	// location of originator
	o : [0..4];
	// 0 - init
	// 1 - send
	// 2 - waiting
	// 3 - finished
	// 4 - error

	N : [0..K]; // number of messages
	ack : [0..K]; // number of acks the originator has received

	// init
	//  get request (so set K)
	[req] o=0 & K=1 ->  1/K : (o'=1) & (N'=1);
	[req] o=0 & K=2 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2);
	[req] o=0 & K=3 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3);
	[req] o=0 & K=4 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4);
	[req] o=0 & K=5 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5);
	[req] o=0 & K=6 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6);
	[req] o=0 & K=7 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7);
	[req] o=0 & K=8 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8);
	[req] o=0 & K=9 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9);
	[req] o=0 & K=10 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10);
	[req] o=0  & K=11 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11);
	[req] o=0  & K=12 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12);
	[req] o=0  & K=13 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13);
	[req] o=0  & K=14 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13)
				+ 1/K : (o'=1) & (N'=14);
	[req] o=0  & K=15 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13)
				+ 1/K : (o'=1) & (N'=14)
				+ 1/K : (o'=1) & (N'=15);
	[req] o=0  & K=16 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13)
				+ 1/K : (o'=1) & (N'=14)
				+ 1/K : (o'=1) & (N'=15)
				+ 1/K : (o'=1) & (N'=16);
	[req] o=0  & K=17 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13)
				+ 1/K : (o'=1) & (N'=14)
				+ 1/K : (o'=1) & (N'=15)
				+ 1/K : (o'=1) & (N'=16)
				+ 1/K : (o'=1) & (N'=17);
	[req] o=0  & K=18 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13)
				+ 1/K : (o'=1) & (N'=14)
				+ 1/K : (o'=1) & (N'=15)
				+ 1/K : (o'=1) & (N'=16)
				+ 1/K : (o'=1) & (N'=17)
				+ 1/K : (o'=1) & (N'=18);
	[req] o=0  & K=19 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13)
				+ 1/K : (o'=1) & (N'=14)
				+ 1/K : (o'=1) & (N'=15)
				+ 1/K : (o'=1) & (N'=16)
				+ 1/K : (o'=1) & (N'=17)
				+ 1/K : (o'=1) & (N'=18)
				+ 1/K : (o'=1) & (N'=19);
	[req] o=0  & K=20 ->  1/K : (o'=1) & (N'=1)
				+ 1/K : (o'=1) & (N'=2)
				+ 1/K : (o'=1) & (N'=3)
				+ 1/K : (o'=1) & (N'=4)
				+ 1/K : (o'=1) & (N'=5)
				+ 1/K : (o'=1) & (N'=6)
				+ 1/K : (o'=1) & (N'=7)
				+ 1/K : (o'=1) & (N'=8)
				+ 1/K : (o'=1) & (N'=9)
				+ 1/K : (o'=1) & (N'=10)
				+ 1/K : (o'=1) & (N'=11)
				+ 1/K : (o'=1) & (N'=12)
				+ 1/K : (o'=1) & (N'=13)
				+ 1/K : (o'=1) & (N'=14)
				+ 1/K : (o'=1) & (N'=15)
				+ 1/K : (o'=1) & (N'=16)
				+ 1/K : (o'=1) & (N'=17)
				+ 1/K : (o'=1) & (N'=18)
				+ 1/K : (o'=1) & (N'=19)
				+ 1/K : (o'=1) & (N'=20);
	
	// send
	[message] o=1 -> (o'=2); // send a message
	// receive
	[ack] o=2 & ack<N-1 -> (o'=1) & (ack'=min(ack+1,K)); // not last ack
	[ack] o=2 & ack=N-1 -> (o'=3) & (ack'=min(ack+1,K)); // last ack

	[done] o=3 -> (o'=3); // protocol finished
		
endmodule


module malicious_recipient

	r : [0..3];
	// 0 initial state
	// 1 receives a message
	// 2 sends an ack
	// 3 recipient stops (either protocol finished or malicious behaviour)
		
	mess : [0..K]; // number of mess the originator has received
	last : [0..1]; // protocol is unfair

	[req] r=0 -> (r'=1); // initiate protocol
	[message] r=1 -> (r'=2) & (mess'=min(mess+1,K)); // receive message
	[ack] r=2 -> (r'=1); // send ack
	[done] true -> true; // originator lets recipient know the protocol is over (loop)
	[stop] r=2 -> (r'=3); // recipient stops early and tries to decode
	[] r=3 & mess=N & ack<N -> (r'=3) & (last'=1); // decodes and unfair
	[] r=3 & !(mess=N & ack<N) -> (r'=3); // cannot decode or not unfair

endmodule

// unfair state reached
label "unfair" = last=1;