Qs2_secret_sinPub_sinSub.spdl

usertype Message;  
usertype operations; 
usertype Acknowledgment; 

//https://www.hivemq.com/blog/mqtt-essentials-part-6-mqtt-quality-of-service-levels
protocol MQTT-Multi-Publishers(Pa, S, Sub) {      

	role Pa  {
			
			fresh PublishMessageA : Message;    //store message -> PublishMessageA , store message ID-> Pa
			fresh PUBREC  : operations;
			fresh PUBREL  : operations;
			var ack  : Acknowledgment;
			var PUBCOMP  : operations;

			send_1(Pa, S, {PublishMessageA,Pa}k(S) );
			
			recv_4(S, Pa, {PUBREC}k(Pa));    //?????When the sender receives the PUBREC it can safely discard the initial publish, because it knows that the counter part has successfully received the message
			
			send_5(Pa, S, {PUBREL}k(S));
			
			recv_8(S, Pa ,{PUBCOMP,ack}k(Pa));

			claim_a1(Pa, Secret,PublishMessageA);
			claim_a2(Pa,Weakagree);
		claim_r3(Pa,Niagree);
		claim_r4(Pa,Nisynch);

			}

//The server descripton includes the messages that has been sent and received

	role S  {

			var PublishMessageA: Message;
			var ack  : Acknowledgment;
			var PUBREC  : operations;
			var PUBREL  : operations;
			var PUBCOMP  : operations;
			var PUBCOMP  : operations;


			recv_1(Pa, S, {PublishMessageA,Pa}k(S));
			send_2(S, Sub, {Pa,S, PublishMessageA}k(Sub));
			
			recv_3 (Sub, S, {PUBREC, Sub}k(S));
			send_4 (S, Pa, {PUBREC}k(Pa));
			
			recv_5(Pa, S, {PUBREL}k(S));
			send_6(S, Sub, {PUBREL}k(Sub));

			recv_7(Sub,S, {PUBCOMP,ack}k(S));
			send_8(S, Pa ,{PUBCOMP,ack}k(Pa));



			}
//The subscriber description includes the messages that has been sent and received

	role Sub  {

			var PublishMessageA: Message;
			fresh ack  : Acknowledgment;
			fresh PUBREC  : operations;
			var PUBREL  : operations;
			fresh PUBCOMP  : operations;

			recv_2 (S, Sub, {Pa, S, PublishMessageA}k(Sub));
			send_3 (Sub, S, {PUBREC, Sub}k(S));

			recv_6(S, Sub, {PUBREL}k(Sub));
			send_7(Sub,S, {PUBCOMP,ack}k(S));


			}
}