+++ /dev/null
-/*
- * 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])
- }
-}
projects / lttv.git / blobdiff