Как смоделировать логическое И-вычисление в Promela неатомарно?
Я хочу смоделировать оператор while (flag[j] == true && victim == i), где И-оценка должна выполняться неатомарно.
Как это возможно?
Как смоделировать логическое И-вычисление в Promela неатомарно?
comment
Мой ответ не достоин даже голосования?
- person GoZoner schedule 09.01.2016
Ответы (1)
loop:
if
:: flag[j] != true -> goto done
:: else
fi;
if
:: victim != i -> goto done
:: else
fi;
/* body of 'while' */
goto loop;
done:
/* after 'while' */
Обратите внимание: хотя передо мной нет среды Spin, что заставляет вас думать, что условное выражение вообще атомарно? Я бы проверил что-то вроде:
byte i = 0
i++ >= 0 && i-- >= 0
never { assert (1 == i) }
Но, в любом случае, первый код выше показывает, как сделать его неатомарным, если это необходимо.
person
GoZoner
schedule
16.12.2015
Извините, я был неактивен в последнее время. Большое спасибо за ваш ответ - я ценю это.
- person Shuzheng; 10.01.2016
