1/*
2 * PROMELA Validation Model
3 * FLOW CONTROL LAYER VALIDATION
4 */
5
6/* see end of file for LTL properties */
7
8#define LOSS		1	/* message loss   */
9#define DUPS		0	/* duplicate msgs */
10#define QSZ		2	/* queue size     */
11
12mtype = {
13	red, white, blue,
14	abort, accept, ack, sync_ack, close, connect,
15	create, data, eof, open, reject, sync, transfer,
16	FATAL, NON_FATAL, COMPLETE
17	}
18
19chan ses_to_flow[2] = [QSZ] of { byte, byte };
20chan flow_to_ses[2] = [QSZ] of { byte, byte };
21chan dll_to_flow[2] = [QSZ] of { byte, byte };
22
23/*
24 * Flow Control Layer Validation Model
25 */
26
27#define true	1
28#define false	0
29
30#define M	4	/* range sequence numbers   */
31#define W	2	/* window size: M/2         */
32
33proctype fc(chan s2f, f2d, f2s, d2f)
34{	bool	busy[M];	/* outstanding messages    */
35	byte	q;		/* seq# oldest unacked msg */
36	byte	m;		/* seq# last msg received  */
37	byte	s;		/* seq# next msg to send   */
38	byte	window;		/* nr of outstanding msgs  */
39	byte	type;		/* msg type                */
40	bit	received[M];	/* receiver housekeeping   */
41	bit	x;		/* scratch variable        */
42	byte	p;		/* seq# of last msg acked  */
43	byte	I_buf[M], O_buf[M];	/* message buffers */
44
45	xr s2f;
46	xs f2d;
47	xs f2s;
48	xr d2f;
49
50	/* sender part */
51end:	do
52	:: atomic {
53	   (window < W	&& nempty(s2f)
54			&& nfull(f2d)) ->
55			s2f?type,x;
56			window = window + 1;
57			busy[s] = true;
58			O_buf[s] = type;
59			f2d!type,s;
60			if
61			:: (type != sync) ->
62				s = (s+1)%M
63			:: (type == sync) ->
64				window = 0;
65				s = M;
66				do
67				:: (s > 0) ->
68					s = s-1;
69					busy[s] = false
70				:: (s == 0) ->
71					break
72				od
73			fi
74	   }
75	:: atomic {
76		(window > 0 && busy[q] == false) ->
77		window = window - 1;
78		q = (q+1)%M
79	   }
80#if DUPS
81	:: atomic {
82		(nfull(f2d) && window > 0 && busy[q] == true) ->
83		f2d!O_buf[q],q
84	   }
85#endif
86	:: atomic {
87		(timeout && nfull(f2d) && window > 0 && busy[q] == true) ->
88		f2d!O_buf[q],q
89	   }
90	/* receiver part */
91#if LOSS
92	:: d2f?type,m /* lose any message */
93#endif
94	:: d2f?type,m ->
95		if
96		:: atomic {
97			(type == ack) ->
98			busy[m] = false
99		   }
100		:: atomic {
101			(type == sync) ->
102			m = 0;
103			do
104			:: (m < M) ->
105				received[m] = 0;
106				m = m+1
107			:: (m == M) ->
108				break
109			od
110		   };	f2d!sync_ack,0
111		:: (type == sync_ack) ->
112			f2s!sync_ack,0
113		:: (type != ack && type != sync && type != sync_ack)->
114			if
115			:: atomic {
116				(received[m] == true) ->
117					x = ((0<p-m   && p-m<=W)
118					||   (0<p-m+M && p-m+M<=W)) };
119					if
120					:: (x) -> f2d!ack,m
121					:: (!x)	/* else skip */
122					fi
123			:: atomic {
124				(received[m] == false) ->
125					I_buf[m] = type;
126					received[m] = true;
127					received[(m-W+M)%M] = false
128			   }
129			fi
130		fi
131	:: /* atomic { */
132	   (received[p] == true && nfull(f2s) && nfull(f2d)) ->
133		f2s!I_buf[p],0;
134		f2d!ack,p;
135		p = (p+1)%M
136	   /* } */
137	od
138}
139
140proctype upper_s(chan s2f, f2s0)
141{	byte s_state;
142	byte type, toggle;
143
144	xs s2f;
145	xr f2s0;
146
147	s2f!sync,toggle;
148	do
149	:: f2s0?sync_ack,type ->
150		if
151		:: (type != toggle)
152		:: (type == toggle) -> break
153		fi
154	:: timeout ->
155		s2f!sync,toggle
156	od;
157	toggle = 1 - toggle;
158
159end:	do
160	:: s2f!white,0
161	:: atomic {
162		(s_state == 0 && nfull(s2f)) ->
163		s2f!red,0 ->
164		s_state = 1
165	   }
166	:: atomic {
167		(s_state == 1 && nfull(s2f)) ->
168		s2f!blue,0 ->
169		s_state = 2
170	   }
171	od
172}
173
174proctype upper_r(chan f2s1)
175{	byte r_state;
176
177	xr f2s1;
178
179	do
180	:: f2s1?white,0
181	:: f2s1?red,0 -> break
182	:: f2s1?blue,0 -> assert(0)
183	od;
184
185	do
186	:: f2s1?white,0
187	:: f2s1?red,0 -> assert(0)
188	:: f2s1?blue,0 -> goto end
189	od;
190end:
191	do
192	:: f2s1?white,0
193	:: f2s1?red,0 -> assert(0)
194	:: f2s1?blue,0 -> assert(0)
195	od
196}
197
198init
199{
200	atomic {
201	  run fc(ses_to_flow[0], dll_to_flow[1], flow_to_ses[0], dll_to_flow[0]);
202	  run fc(ses_to_flow[1], dll_to_flow[0], flow_to_ses[1], dll_to_flow[1]);
203	  run upper_s(ses_to_flow[0], flow_to_ses[0]);
204	  run upper_r(flow_to_ses[1])
205	}
206}
207
208ltl p1 { ( len(flow_to_ses[1]) > 0 -> flow_to_ses[1]?[white]) U ( flow_to_ses[1]?[red] ) }
209ltl p2 { (!(flow_to_ses[1]?[blue])) U (flow_to_ses[1]?[red]) }
210ltl p3 { <> (flow_to_ses[1]?[blue]) }
211