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
80
81
82
83
84
85
86
87
88
89
90
91
|
/* This promela model was used to verify a past design of the bus object. */
bool lock = false;
inline enterMon() {
atomic {
!lock;
lock = true;
}
}
inline leaveMon() {
lock = false;
}
typedef Condition {
bool gate;
byte waiting;
}
#define emptyC(C) (C.waiting == 0)
inline waitC(C) {
atomic {
C.waiting++;
lock = false;
C.gate;
C.gate = false;
C.waiting--;
}
}
inline signalC(C) {
atomic {
if
:: (C.waiting > 0) ->
C.gate = true;
!lock;
lock = true;
:: else
fi;
}
}
mtype = { clear, set };
mtype writing_event = clear;
byte critical = 0;
Condition done_writing;
bool live = false;
active proctype RX()
{
end:
do
:: enterMon();
if
:: (writing_event == set) ->
waitC(done_writing);
:: else
fi;
critical++;
assert(critical == 1);
live = true;
live = false;
critical--;
leaveMon();
od
}
active proctype TX()
{
end:
do
:: atomic {
writing_event == clear ->
writing_event = set;
}
enterMon();
critical++;
assert(critical == 1);
live = true;
live = false;
critical--;
writing_event = clear;
signalC(done_writing);
leaveMon();
od
}
ltl {[]<> live}
|
