X-Git-Url: http://git.lttng.org/?a=blobdiff_plain;f=verif%2FSpin%2FTest%2Fpftp;fp=verif%2FSpin%2FTest%2Fpftp;h=0000000000000000000000000000000000000000;hb=a219d12930979a81f43a3a3f5499b2bd00141a84;hp=cd05dce78eddb5a03de0c1aee9207bdcdb91904f;hpb=31efe1f8304f09a4f4139c387a98d3215cd423c9;p=lttv.git

diff --git a/verif/Spin/Test/pftp b/verif/Spin/Test/pftp
deleted file mode 100755
index cd05dce7..00000000
--- a/verif/Spin/Test/pftp
+++ /dev/null
@@ -1,204 +0,0 @@
-/*
- * PROMELA Validation Model
- * FLOW CONTROL LAYER VALIDATION
- */
-
-#define LOSS		1	/* message loss   */
-#define DUPS		0	/* duplicate msgs */
-#define QSZ		2	/* queue size     */
-
-mtype = {
-	red, white, blue,
-	abort, accept, ack, sync_ack, close, connect,
-	create, data, eof, open, reject, sync, transfer,
-	FATAL, NON_FATAL, COMPLETE
-	}
-
-chan ses_to_flow[2] = [QSZ] of { byte, byte };
-chan flow_to_ses[2] = [QSZ] of { byte, byte };
-chan dll_to_flow[2] = [QSZ] of { byte, byte };
-
-/*
- * Flow Control Layer Validation Model
- */
-
-#define true	1
-#define false	0
-
-#define M	4	/* range sequence numbers   */
-#define W	2	/* window size: M/2         */
-
-proctype fc(chan s2f, f2d, f2s, d2f)
-{	bool	busy[M];	/* outstanding messages    */
-	byte	q;		/* seq# oldest unacked msg */
-	byte	m;		/* seq# last msg received  */
-	byte	s;		/* seq# next msg to send   */
-	byte	window;		/* nr of outstanding msgs  */
-	byte	type;		/* msg type                */
-	bit	received[M];	/* receiver housekeeping   */
-	bit	x;		/* scratch variable        */
-	byte	p;		/* seq# of last msg acked  */
-	byte	I_buf[M], O_buf[M];	/* message buffers */
-
-	xr s2f;
-	xs f2d;
-	xs f2s;
-	xr d2f;
-
-	/* sender part */
-end:	do
-	:: atomic {
-	   (window < W	&& nempty(s2f)
-			&& nfull(f2d)) ->
-			s2f?type,x;
-			window = window + 1;
-			busy[s] = true;
-			O_buf[s] = type;
-			f2d!type,s;
-			if
-			:: (type != sync) ->
-				s = (s+1)%M
-			:: (type == sync) ->
-				window = 0;
-				s = M;
-				do
-				:: (s > 0) ->
-					s = s-1;
-					busy[s] = false
-				:: (s == 0) ->
-					break
-				od
-			fi
-	   }
-	:: atomic {
-		(window > 0 && busy[q] == false) ->
-		window = window - 1;
-		q = (q+1)%M
-	   }
-#if DUPS
-	:: atomic {
-		(nfull(f2d) && window > 0 && busy[q] == true) ->
-		f2d!O_buf[q],q
-	   }
-#endif
-	:: atomic {
-		(timeout && nfull(f2d) && window > 0 && busy[q] == true) ->
-		f2d!O_buf[q],q
-	   }
-	/* receiver part */
-#if LOSS
-	:: d2f?type,m /* lose any message */
-#endif
-	:: d2f?type,m ->
-		if
-		:: atomic {
-			(type == ack) ->
-			busy[m] = false
-		   }
-		:: atomic {
-			(type == sync) ->
-			m = 0;
-			do
-			:: (m < M) ->
-				received[m] = 0;
-				m = m+1
-			:: (m == M) ->
-				break
-			od
-		   };	f2d!sync_ack,0
-		:: (type == sync_ack) ->
-			f2s!sync_ack,0
-		:: (type != ack && type != sync && type != sync_ack)->
-			if
-			:: atomic {
-				(received[m] == true) ->
-					x = ((0<p-m   && p-m<=W)
-					||   (0<p-m+M && p-m+M<=W)) };
-					if
-					:: (x) -> f2d!ack,m
-					:: (!x)	/* else skip */
-					fi
-			:: atomic {
-				(received[m] == false) ->
-					I_buf[m] = type;
-					received[m] = true;
-					received[(m-W+M)%M] = false
-			   }
-			fi
-		fi
-	:: /* atomic { */
-	   (received[p] == true && nfull(f2s) && nfull(f2d)) ->
-		f2s!I_buf[p],0;
-		f2d!ack,p;
-		p = (p+1)%M
-	   /* } */
-	od
-}
-
-proctype upper_s(chan s2f, f2s0)
-{	byte s_state;
-	byte type, toggle;
-
-	xs s2f;
-	xr f2s0;
-
-	s2f!sync,toggle;
-	do
-	:: f2s0?sync_ack,type ->
-		if
-		:: (type != toggle)
-		:: (type == toggle) -> break
-		fi
-	:: timeout ->
-		s2f!sync,toggle
-	od;
-	toggle = 1 - toggle;
-
-end:	do
-	:: s2f!white,0
-	:: atomic {
-		(s_state == 0 && nfull(s2f)) ->
-		s2f!red,0 ->
-		s_state = 1
-	   }
-	:: atomic {
-		(s_state == 1 && nfull(s2f)) ->
-		s2f!blue,0 ->
-		s_state = 2
-	   }
-	od
-}
-
-proctype upper_r(chan f2s1)
-{	byte r_state;
-
-	xr f2s1;
-
-	do
-	:: f2s1?white,0
-	:: f2s1?red,0 -> break
-	:: f2s1?blue,0 -> assert(0)
-	od;
-
-	do
-	:: f2s1?white,0
-	:: f2s1?red,0 -> assert(0)
-	:: f2s1?blue,0 -> goto end
-	od;
-end:
-	do
-	:: f2s1?white,0
-	:: f2s1?red,0 -> assert(0)
-	:: f2s1?blue,0 -> assert(0)
-	od
-}
-
-init
-{
-	atomic {
-	  run fc(ses_to_flow[0], dll_to_flow[1], flow_to_ses[0], dll_to_flow[0]);
-	  run fc(ses_to_flow[1], dll_to_flow[0], flow_to_ses[1], dll_to_flow[1]);
-	  run upper_s(ses_to_flow[0], flow_to_ses[0]);
-	  run upper_r(flow_to_ses[1])
-	}
-}