**************
* initialize *
**************
clear;


*******************************
* Channel assuming no errors  *
*******************************
agent Chancs =
		'sendsyncs.'recvsyncs.Chancs
	+ 	'sendacksyncs.'recvacksyncs.Chancs
	+	'sendfincs.'recvfincs.Chancs
	+ 	'sendackfincs.'recvackfincs.Chancs
	+ 	'sendfinackcs.'recvfinackcs.Chancs
	+ 	'senddatacs.'recvdatacs.Chancs;


agent Chansc = 
		'sendsynacksc.'recvsynacksc.Chansc 
	+ 	'sendfinsc.'recvfinsc.Chansc
	+ 	'sendfinacksc.'recvfinacksc.Chansc
	+ 	'sendackfinsc.'recvackfinsc.Chansc
	+ 	'sendacksc.'recvacksc.Chansc;

agent Chan = (Chancs | Chansc);


**********
* Client *
**********

agent Closedc = open.sendsyncs.Synsentc;
agent Synsentc = recvsynacksc.sendacksyncs.Estbc;
agent Estbc = 
	senddatacs.(recvacksc.Estbc + recvfinsc.sendackfincs.recvacksc.Closewaitc)
	+ closec.sendfincs.Finwait1c
	+ recvfinsc.sendackfincs.Closewaitc;
agent Closewaitc = 
	closec.sendfincs.Lastackc
	+ senddatacs.recvacksc.Closewaitc;
agent Lastackc = recvackfinsc.Closedc;
agent Finwait1c = recvackfinsc.Finwait2c
	+ recvfinsc.sendackfincs.Closingc; 
agent Closingc = recvackfinsc.Timewaitc;
agent Finwait2c = recvfinsc.sendackfincs.Timewaitc;
agent Timewaitc = tau.Closedc;

**********
* Server *
**********

agent Closeds = tau.Listens;
agent Listens = recvsyncs.sendsynacksc.Synrcvds; 
agent Synrcvds = 
	recvacksyncs.Estbs
	+ recvdatacs.sendacksc.Estbs;
agent Estbs = 
	closes.sendfinsc.Finwait1s
	+ recvdatacs.sendacksc.Estbs
	+ recvfincs.sendackfinsc.Closewaits;
	
agent Closewaits = 
	closes.sendfinsc.Lastacks
	+ recvdatacs.sendacksc.Closewaits;
agent Lastacks = recvackfincs.Closeds;
agent Finwait1s = 
	recvdatacs.sendacksc.Finwait1s
	+ recvfincs.sendackfinsc.Closings 
	+ recvackfincs.Finwait2s;
agent Closings = recvackfincs.Timewaits;
agent Finwait2s = 
	recvfincs.sendackfinsc.Timewaits
	+ recvdatacs.sendacksc.Finwait2s;
agent Timewaits = $tau.Closeds;

*****************
* Protocol Unit *
*****************

agent AgentSet = (Closedc | Chan | Listens);

set ActionSet = {
sendsyncs, recvsyncs, sendacksyncs, recvacksyncs,
sendfincs, recvfincs, sendackfincs, recvackfincs,
sendfinackcs, recvfinackcs,
sendsynacksc, recvsynacksc,
sendfinsc, recvfinsc, sendfinacksc, recvfinacksc,
sendackfinsc, recvackfinsc,
senddatacs,  recvdatacs,  sendacksc, recvacksc};


set ConnectActionSet = {
sendsyncs, recvsyncs, sendacksyncs, recvacksyncs,
sendsynacksc, recvsynacksc,
senddatacs,  recvdatacs,  sendacksc, recvacksc,
sendfincs, recvfincs, sendackfincs, recvackfincs,
sendfinackcs, recvfinackcs,
sendfinsc, recvfinsc, sendfinacksc, recvfinacksc,
sendackfinsc, recvackfinsc,
open};

set CloseActionSet = {
sendfincs, recvfincs, sendackfincs, recvackfincs,
sendfinackcs, recvfinackcs,
sendfinsc, recvfinsc, sendfinacksc, recvfinacksc,
sendackfinsc, recvackfinsc,
senddatacs,  recvdatacs,  sendacksc, recvacksc,
sendsyncs, recvsyncs, sendacksyncs, recvacksyncs,
sendsynacksc, recvsynacksc};



**************************************
* Open - Close Implementation & Spec *
**************************************
agent TCP = AgentSet\ActionSet;
agent Spec =  open.(closes.closec.Spec + closec.closes.Spec); 




****************************************************************
* Connection setup (three-way handshake) Implementation & Spec *
* (Close -> Estb)				               *
****************************************************************

agent TCP_con_set = AgentSet\ActionSet;
agent Server_con = recvsyncs.sendsynacksc.recvacksyncs.Estbs;
agent Client_con =  open.sendsyncs.recvsynacksc.sendacksyncs.Estbc;

agent Spec_con_set = (Server_con | Chan | Client_con)\CloseActionSet;


*********************************
* Channel Implementation & Spec *
* (Reliable Message Delivery)   *
*********************************
set UnnecessaryForMsgAction = {
sendfincs, recvfincs, sendackfincs, recvackfincs,
sendfinackcs, recvfinackcs,
sendfinsc, recvfinsc, sendfinacksc, recvfinacksc,
sendackfinsc, recvackfinsc,
sendsyncs, recvsyncs, sendacksyncs, recvacksyncs,
sendsynacksc, recvsynacksc,
closec, closes, open};

agent Established = (Estbc | Chan | Estbs)\UnnecessaryForMsgAction;
agent Spec_Estb = (senddatacs.recvacksc.Estbc | 
		   recvdatacs.sendacksc.Estbs |
		   'senddatacs.'recvdatacs.Chancs |
		   'sendacksc.'recvacksc.Chansc)\UnnecessaryForMsgAction;


***************************************
* Disconnection Implementation & Spec *
* (Estb -> Close)                     *
***************************************

agent AgentSetFromEstb = (Estbc | Chan | Estbs);
agent TCP_discon = AgentSetFromEstb\ConnectActionSet;	


agent Server_discon1 = closes.sendfinsc.recvackfincs.recvfincs.sendackfinsc.(Timewaits+Closeds+Listens);
agent Client_discon1 =  recvfinsc.sendackfincs.closec.sendfincs.recvackfinsc.(Timewaitc+Closedc);
agent Discon1 = (Server_discon1 | Chan | Client_discon1);

agent Server_discon2 = recvfincs.sendackfinsc.closes.sendfinsc.recvackfincs.Closeds;
agent Client_discon2 = closec.sendfincs.recvackfinsc.recvfinsc.sendackfincs.(Timewaitc+Closedc);
agent Discon2 = (Server_discon2 | Chan | Client_discon2);

agent Server_discon3 = closes.sendfinsc.recvackfincs.recvfincs.sendackfinsc.(Timewaits+Closeds+Listens);
agent Client_discon3 = closec.sendfincs.recvfinsc.sendackfincs.recvackfinsc.(Timewaitc+Closedc);
agent Discon3 = (Server_discon3 | Chan | Client_discon3);

agent Server_discon4 = closes.sendfinsc.recvfincs.sendackfinsc.recvackfincs.(Timewaits+Closeds+Listens);
agent Client_discon4 = closec.sendfincs.recvackfinsc.recvfinsc.sendackfincs.(Timewaitc+Closedc);
agent Discon4 = (Server_discon4 | Chan | Client_discon4);

agent Spec_discon = (Discon1+Discon2+Discon3+Discon4)\ConnectActionSet;


***************
* Proposition *
***************

prop Always(A) = max(X.A & [-]X);
prop Poss(A) = min(X.A | <->X);
prop Even(A) = min(X.A | (<->T & [-]X));
prop Evenaction(a) = min(X.<->T & [-a]X);

prop DeadlockFree = Always(<->T);

prop Can(a) = min(X.<a>T | <t>X); 
prop Can't(a) = ~(Can(a));

prop Livedata= Always([senddatacs] Evenaction(recvacksc));
prop Lives = Always([recvsyncs] Evenaction(recvacksyncs));
prop Livec = Always([sendsyncs] Evenaction(sendacksyncs));

prop StrongUntil(P, Q) = min(Z.Q | (P & [-]Z & <->T));
prop WeakUntil(P, Q) = max(Z.Q | (P & [-]Z));

prop Safety1 = Always(WeakUntil(Can't(senddatacs), Evenaction(recvsynacksc)));
prop Safety2 = Always(WeakUntil(Evenaction(sendfincs), Can't(senddatacs)));

* Liveness
*1. if a client goes to Estbc, a server must go to Estbs
*2. if data sent, ack received   
*3. if a client goes to Closed from Estb, a server must go to Closeds
*4. or No Deadlock

* Safety

* Fairness
*prop Live_con = Always([recvacksyncs] Even()); 

*
* Model Checking 0
*

cp (TCP, Livedata);
cp (TCP, Lives);
cp (TCP, Livec);

*cp (TCP,Live_con);



*
*   TEST 1
*

deadlocksobs (TCP);
deadlocksobs (Spec);


eq (TCP, Spec);		* weakly bisimilar
dfweak (TCP, Spec);	*find a weak HML formula distinguishing two agents



*
*  TEST 2 
*

* THERE MUST BE DEADLOCKS SINCE THE STATES ARE FINITE.
* SO, WE DON'T NEED DEADLOCK TESTS

**deadlocksobs (TCP_con_set);
**deadlocksobs (Spec_con_set);

eq (TCP_con_set, Spec_con_set);		* weakly bisimilar
dfweak (TCP_con_set, Spec_con_set);	*find a weak HML formula distinguishing two agents


*
*   TEST 3
*

deadlocksobs (Established);
deadlocksobs (Spec_Estb);

eq (Established, Spec_Estb);		* weakly bisimilar
dfweak (Established, Spec_Estb);	*find a weak HML formula distinguishing two agents

*cong (Established, Spec_Estb);	* observationally congruent (equal)


*
*   TEST 4
*

*deadlocksobs (TCP_discon);
*deadlocksobs (Spec_discon);

eq (TCP_discon, Spec_discon);		* weakly bisimilar
dfweak (TCP_discon, Spec_discon);  *find a weak HML formula distinguishing two agents