Mercurial > hg > Members > nobuyasu > Spin

annotate Samples/App.F.flow_cl.h @ 0:86e67be8bc5f draft

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some files
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Fri, 29 Jun 2012 01:14:43 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 /*
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 * Flow Control Layer Validation Model
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 #define true 1
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 #define false 0
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 #define M 4 /* range sequence numbers */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 #define W 2 /* window size: M/2 */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 proctype fc(bit n)
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 { bool busy[M]; /* outstanding messages */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 byte q; /* seq# oldest unacked msg */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 byte m; /* seq# last msg received */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 byte s; /* seq# next msg to send */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 byte window; /* nr of outstanding msgs */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 byte type; /* msg type */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 bit received[M]; /* receiver housekeeping */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 bit x; /* scratch variable */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 byte p; /* seq# of last msg acked */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 byte I_buf[M], O_buf[M]; /* message buffers */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 /* sender part */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 end: do
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 (window < W && len(ses_to_flow[n]) > 0
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 && len(flow_to_dll[n]) < QSZ) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 ses_to_flow[n]?type,x;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 window = window + 1;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 busy[s] = true;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 O_buf[s] = type;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 flow_to_dll[n]!type,s;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 if
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 :: (type != sync) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 s = (s+1)%M
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 :: (type == sync) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 window = 0;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 s = M;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 do
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 :: (s > 0) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 s = s-1;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 busy[s] = false
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 :: (s == 0) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 break
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 od
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 fi
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 (window > 0 && busy[q] == false) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 window = window - 1;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 q = (q+1)%M
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 #if DUPS
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 (len(flow_to_dll[n]) < QSZ
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 && window > 0 && busy[q] == true) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 flow_to_dll[n]! O_buf[q],q
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 #endif
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 (timeout && len(flow_to_dll[n]) < QSZ
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 && window > 0 && busy[q] == true) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 flow_to_dll[n]! O_buf[q],q
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 /* receiver part */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 #if LOSS
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 :: dll_to_flow[n]?type,m /* lose any message */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 #endif
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 :: dll_to_flow[n]?type,m ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 if
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 (type == ack) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 busy[m] = false
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 (type == sync) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 flow_to_dll[n]!sync_ack,m;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 m = 0;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 do
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 :: (m < M) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 received[m] = 0;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 m = m+1
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 :: (m == M) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 break
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 od
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 :: (type == sync_ack) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 flow_to_ses[n]!sync_ack,m
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 :: (type != ack && type != sync && type != sync_ack)->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 if
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 (received[m] == true) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 x = ((0<p-m && p-m<=W)
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 || (0<p-m+M && p-m+M<=W)) };
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 if
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 :: (x) -> flow_to_dll[n]!ack,m
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 :: (!x) /* else skip */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 fi
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 :: atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 (received[m] == false) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 I_buf[m] = type;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 received[m] = true;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 received[(m-W+M)%M] = false
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 fi
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 fi
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 :: (received[p] == true && len(flow_to_ses[n])<QSZ
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 && len(flow_to_dll[n])<QSZ) ->
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 flow_to_ses[n]!I_buf[p],0;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 flow_to_dll[n]!ack,p;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 p = (p+1)%M
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 od
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 }