forked from kmsalem/Carousel-TLA
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathchan.pml
82 lines (68 loc) · 1.23 KB
/
chan.pml
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
mtype{MSG}
chan toClient = [10] of {chan}
chan getRN = [20] of {int}
/*random number generator*/
proctype Random_num (int upperbound; chan RN)
{
int nr;
do
:: nr >= upperbound -> nr = 0
:: nr < 0 -> nr=upperbound -1
:: nr++ /* randomly increment */
:: nr-- /* or decrement */
:: nr >= 0 && nr < upperbound -> RN ! nr /* or output */
od;
}
/*participants*/
proctype P1(chan out)
{
chan in = [10] of {mtype, bit};
do
::bit recebit;
out ! in;
in ? MSG(recebit);
od
}
proctype P2(chan out)
{
chan in = [10] of {mtype, bit};
do
::bit recebit;
out ! in;
in ? MSG(recebit);
od
}
proctype P3(chan out)
{
chan in = [10] of {mtype, bit};
do
::bit recebit;
out ! in;
in ? MSG(recebit);
od
}
/*Client*/
proctype Client(chan RN, in)
{
int sSet;
bit sendbit;
RN ? sSet;
chan toSend;
do
::if
::sSet >= 0 ->
in? toSend;
toSend ! MSG(sendbit);
sSet--;
::else -> break;
fi
od
}
/*main function*/
init{
run Random_num (2, getRN);
run P1(toClient);
run P2(toClient);
run P3(toClient);
run Client(getRN, toClient);
}