1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
/*
* File Server Validation Model
*/
proctype fserver(bit n)
{
end: do
:: ses_to_fsrv[n]?create -> /* incoming */
if
:: fsrv_to_ses[n]!reject
:: fsrv_to_ses[n]!accept ->
do
:: ses_to_fsrv[n]?data
:: ses_to_fsrv[n]?eof -> break
:: ses_to_fsrv[n]?close -> break
od
fi
:: ses_to_fsrv[n]?open -> /* outgoing */
if
:: fsrv_to_ses[n]!reject
:: fsrv_to_ses[n]!accept ->
do
:: fsrv_to_ses[n]!data -> progress: skip
:: ses_to_fsrv[n]?close -> break
:: fsrv_to_ses[n]!eof -> break
od
fi
od
}
|
