36 lines
391 B
Promela
36 lines
391 B
Promela
// INTENDED BEHAVIOR: no violation
|
|
// explanation: can only replay once
|
|
chan c = [8] of { byte };
|
|
byte q=1;
|
|
|
|
init {
|
|
c!5;
|
|
}
|
|
|
|
active proctype consume() {
|
|
MAIN:
|
|
do
|
|
:: c ? 5 -> goto PROC1;
|
|
od
|
|
PROC1:
|
|
do
|
|
:: c ? 5 ->
|
|
c!3;
|
|
goto PROC2;
|
|
od
|
|
PROC2:
|
|
do
|
|
:: c ? 3 -> goto PROC3;
|
|
od
|
|
PROC3:
|
|
do
|
|
:: c ? 3 -> goto PROC4;
|
|
od
|
|
PROC4:
|
|
q=0;
|
|
}
|
|
|
|
ltl proc {
|
|
always !(q == 0);
|
|
}
|