13 lines
278 B
Promela
13 lines
278 B
Promela
chan msgs = [4] of { bit };
|
|
int count = 0;
|
|
|
|
active [1] proctype Producer() { // one producer
|
|
do :: atomic { count++; msgs ! 1; } od
|
|
}
|
|
|
|
active [4] proctype Consumer() { // four consumers
|
|
do :: atomic { msgs ? 1 -> count--; } od
|
|
}
|
|
|
|
ltl always_positive { always (count >= 0) }
|