37 lines
398 B
Promela
37 lines
398 B
Promela
// intended behavior: no violation
|
|
// explanation: rearrange attacker does not have enough mem
|
|
chan c = [8] of { byte };
|
|
byte q=0;
|
|
|
|
init {
|
|
c!3;
|
|
c!5;
|
|
c!7;
|
|
}
|
|
|
|
active proctype consume() {
|
|
MAIN:
|
|
do
|
|
:: c ? 7 ->
|
|
q = q+1;
|
|
goto B1;
|
|
od
|
|
B1:
|
|
do
|
|
:: c ? 5 ->
|
|
q = q + 1;
|
|
goto B2;
|
|
od
|
|
B2:
|
|
do
|
|
:: c ? 3 ->
|
|
q = q + 1;
|
|
goto END;
|
|
od
|
|
END:
|
|
}
|
|
|
|
ltl proc {
|
|
always !(q==3);
|
|
}
|