2 * PROMELA Validation Model
3 * FLOW CONTROL LAYER VALIDATION
6 #define LOSS 1 /* message loss */
7 #define DUPS 0 /* duplicate msgs */
8 #define QSZ 2 /* queue size */
12 abort, accept, ack, sync_ack, close, connect,
13 create, data, eof, open, reject, sync, transfer,
14 FATAL, NON_FATAL, COMPLETE
17 chan ses_to_flow[2] = [QSZ] of { byte, byte };
18 chan flow_to_ses[2] = [QSZ] of { byte, byte };
19 chan dll_to_flow[2] = [QSZ] of { byte, byte };
22 * Flow Control Layer Validation Model
28 #define M 4 /* range sequence numbers */
29 #define W 2 /* window size: M/2 */
31 proctype fc(chan s2f, f2d, f2s, d2f)
32 { bool busy[M]; /* outstanding messages */
33 byte q; /* seq# oldest unacked msg */
34 byte m; /* seq# last msg received */
35 byte s; /* seq# next msg to send */
36 byte window; /* nr of outstanding msgs */
37 byte type; /* msg type */
38 bit received[M]; /* receiver housekeeping */
39 bit x; /* scratch variable */
40 byte p; /* seq# of last msg acked */
41 byte I_buf[M], O_buf[M]; /* message buffers */
51 (window < W && nempty(s2f)
74 (window > 0 && busy[q] == false) ->
80 (nfull(f2d) && window > 0 && busy[q] == true) ->
85 (timeout && nfull(f2d) && window > 0 && busy[q] == true) ->
90 :: d2f?type,m /* lose any message */
109 :: (type == sync_ack) ->
111 :: (type != ack && type != sync && type != sync_ack)->
114 (received[m] == true) ->
115 x = ((0<p-m && p-m<=W)
116 || (0<p-m+M && p-m+M<=W)) };
119 :: (!x) /* else skip */
122 (received[m] == false) ->
125 received[(m-W+M)%M] = false
130 (received[p] == true && nfull(f2s) && nfull(f2d)) ->
138 proctype upper_s(chan s2f, f2s0)
147 :: f2s0?sync_ack,type ->
150 :: (type == toggle) -> break
160 (s_state == 0 && nfull(s2f)) ->
165 (s_state == 1 && nfull(s2f)) ->
172 proctype upper_r(chan f2s1)
179 :: f2s1?red,0 -> break
180 :: f2s1?blue,0 -> assert(0)
185 :: f2s1?red,0 -> assert(0)
186 :: f2s1?blue,0 -> goto end
191 :: f2s1?red,0 -> assert(0)
192 :: f2s1?blue,0 -> assert(0)
199 run fc(ses_to_flow[0], dll_to_flow[1], flow_to_ses[0], dll_to_flow[0]);
200 run fc(ses_to_flow[1], dll_to_flow[0], flow_to_ses[1], dll_to_flow[1]);
201 run upper_s(ses_to_flow[0], flow_to_ses[0]);
202 run upper_r(flow_to_ses[1])