LTL свойства и программа Promela
У меня есть следующая программа, которая моделирует FIFO с процессом в PROMELA:
mtype = { PUSH, POP, IS_EMPTY, IS_FULL };
#define PRODUCER_UID 0
#define CONSUMER_UID 1
proctype fifo(chan inputs, outputs)
{
mtype command;
int data, tmp, src_uid;
bool data_valid = false;
do
:: true ->
inputs?command(tmp, src_uid);
if
:: command == PUSH ->
if
:: data_valid ->
outputs!IS_FULL(true, src_uid);
:: else ->
data = tmp
data_valid = true;
outputs!PUSH(data, src_uid);
fi
:: command == POP ->
if
:: !data_valid ->
outputs!IS_EMPTY(true, src_uid);
:: else ->
outputs!POP(data, src_uid);
data = -1;
data_valid = false;
fi
:: command == IS_EMPTY ->
outputs!IS_EMPTY(!data_valid, src_uid);
:: command == IS_FULL ->
outputs!IS_FULL(data_valid, src_uid);
fi;
od;
}
proctype producer(chan inputs, outputs)
{
mtype command;
int v;
do
:: true ->
atomic {
inputs!IS_FULL(false, PRODUCER_UID) ->
outputs?IS_FULL(v, PRODUCER_UID);
}
if
:: v == 1 ->
skip
:: else ->
select(v: 0..16);
printf("P[%d] - produced: %d\n", _pid, v);
access_fifo:
atomic {
inputs!PUSH(v, PRODUCER_UID);
outputs?command(v, PRODUCER_UID);
}
assert(command == PUSH);
fi;
od;
}
proctype consumer(chan inputs, outputs)
{
mtype command;
int v;
do
:: true ->
atomic {
inputs!IS_EMPTY(false, CONSUMER_UID) ->
outputs?IS_EMPTY(v, CONSUMER_UID);
}
if
:: v == 1 ->
skip
:: else ->
access_fifo:
atomic {
inputs!POP(v, CONSUMER_UID);
outputs?command(v, CONSUMER_UID);
}
assert(command == POP);
printf("P[%d] - consumed: %d\n", _pid, v);
fi;
od;
}
init {
chan inputs = [0] of { mtype, int, int };
chan outputs = [0] of { mtype, int, int };
run fifo(inputs, outputs); // pid: 1
run producer(inputs, outputs); // pid: 2
run consumer(inputs, outputs); // pid: 3
}
я хочу добавить wr_ptr а также rd_ptr в программе для указания записи и чтения указателей относительно глубины FIFO, когда PUSH Обновление выполняется:
wr_ptr = wr_ptr % depth;
empty=0;
if
:: (rd_ptr == wr_ptr) -> full=true;
fi
и аналогичные шансы на POP обновления
Не могли бы вы помочь мне добавить это в эту программу?
или я должен сделать это свойство ltl и использовать это, чтобы проверить это?
из комментариев: и я хочу проверить это свойство, например, если fifo заполнен, у него не должно быть запроса на запись, то есть правильный синтаксис?full означает, что fifo заполнен, а wr_idx - указатель записи, я не знаю как получить доступ к полной, пустой, wr_idx, rd_idx, глубине процесса fifo в свойствах ltl fifo_no_write_when_full {[] (full ->! wr_idx)}
1 ответ
Вот пример процесса FIFO с размером 1 что я дал вам здесь адаптированный для произвольного размера, который может быть настроен с FIFO_SIZE, В целях проверки я хотел бы сохранить это значение как можно меньше (например, 3), потому что в противном случае вы просто расширяете пространство состояний, не добавляя более существенного поведения.
mtype = { PUSH, POP, IS_EMPTY, IS_FULL };
#define PRODUCER_UID 0
#define CONSUMER_UID 1
#define FIFO_SIZE 10
proctype fifo(chan inputs, outputs)
{
mtype command;
int tmp, src_uid;
int data[FIFO_SIZE];
byte head = 0;
byte count = 0;
bool res;
do
:: true ->
inputs?command(tmp, src_uid);
if
:: command == PUSH ->
if
:: count >= FIFO_SIZE ->
outputs!IS_FULL(true, src_uid);
:: else ->
data[(head + count) % FIFO_SIZE] = tmp;
count = count + 1;
outputs!PUSH(data[(head + count - 1) % FIFO_SIZE], src_uid);
fi
:: command == POP ->
if
:: count <= 0 ->
outputs!IS_EMPTY(true, src_uid);
:: else ->
outputs!POP(data[head], src_uid);
atomic {
head = (head + 1) % FIFO_SIZE;
count = count - 1;
}
fi
:: command == IS_EMPTY ->
res = count <= 0;
outputs!IS_EMPTY(res, src_uid);
:: command == IS_FULL ->
res = count >= FIFO_SIZE;
outputs!IS_FULL(res, src_uid);
fi;
od;
}
Без изменений producer, consumer или же init было необходимо:
proctype producer(chan inputs, outputs)
{
mtype command;
int v;
do
:: true ->
atomic {
inputs!IS_FULL(false, PRODUCER_UID) ->
outputs?IS_FULL(v, PRODUCER_UID);
}
if
:: v == 1 ->
skip
:: else ->
select(v: 0..16);
printf("P[%d] - produced: %d\n", _pid, v);
access_fifo:
atomic {
inputs!PUSH(v, PRODUCER_UID);
outputs?command(v, PRODUCER_UID);
}
assert(command == PUSH);
fi;
od;
}
proctype consumer(chan inputs, outputs)
{
mtype command;
int v;
do
:: true ->
atomic {
inputs!IS_EMPTY(false, CONSUMER_UID) ->
outputs?IS_EMPTY(v, CONSUMER_UID);
}
if
:: v == 1 ->
skip
:: else ->
access_fifo:
atomic {
inputs!POP(v, CONSUMER_UID);
outputs?command(v, CONSUMER_UID);
}
assert(command == POP);
printf("P[%d] - consumed: %d\n", _pid, v);
fi;
od;
}
init {
chan inputs = [0] of { mtype, int, int };
chan outputs = [0] of { mtype, int, int };
run fifo(inputs, outputs); // pid: 1
run producer(inputs, outputs); // pid: 2
run consumer(inputs, outputs); // pid: 3
}
Теперь у вас должно быть достаточно материала для работы и вы готовы написать свои собственные свойства. По этому поводу в своем вопросе вы пишете:
Я не знаю, как получить доступ к полному, пустому, wr_idx, rd_idx, глубине процесса fifo в свойствах ltl fifo_no_write_when_full {[] (full ->! Wr_idx)}
Прежде всего, обратите внимание, что в моем коде rd_idx соответствует head, depth (должен) соответствовать count и что я не использовал явный wr_idx потому что последний может быть получен из первых двух: он дается (head + count) % FIFO_SIZE, Это не просто выбор чистоты кода, потому что меньшее количество переменных в модели Promela фактически помогает с потреблением памяти и временем выполнения процесса проверки.
Конечно, если вы действительно хотите иметь wr_idx в вашей модели вы можете добавить его самостоятельно. (:
Во-вторых, если вы посмотрите руководство Promela для свойств ltl, вы обнаружите, что:
Имена или символы должны быть определены для представления логических выражений для глобальных переменных из модели.
Другими словами, невозможно поместить локальные переменные в выражение ltl. Если вы хотите использовать их, вы должны вынуть их из локального пространства процесса и поместить в глобальное пространство.
Итак, чтобы проверить fifo_no_write_when_full * вы могли бы:
- перенести декларацию
countв глобальном пространстве - добавить ярлык
fifo_write:Вот:
:: command == PUSH ->
if
:: count >= FIFO_SIZE ->
outputs!IS_FULL(true, src_uid);
:: else ->
fifo_write:
data[(head + count) % FIFO_SIZE] = tmp;
count = count + 1;
outputs!PUSH(data[(head + count - 1) % FIFO_SIZE], src_uid);
fi
- проверить свойство:
ltl fifo_no_write_when_full { [] ( (count >= FIFO_SIZE) -> ! fifo@fifo_write) }
В-третьих, перед любой попыткой проверить любое из ваших свойств с помощью обычных команд, например
~$ spin -a fifo.pml
~$ gcc -o fifo pan.c
~$ ./fifo -a -N fifo_no_write_when_full
вы должны изменить producer а также consumer так что ни один из них не выполняется в течение неопределенного периода времени и, следовательно, удерживает пространство поиска на небольшой глубине. В противном случае вы можете получить ошибку такого рода
error: max search depth too small
и убедитесь, что проверка исчерпала все ваши аппаратные ресурсы, не придя к разумному выводу.
*: собственно имя fifo_no_write_when_full является достаточно общим и может иметь несколько интерпретаций, например
-
fifoне выполняетpushкогда он полон -
producerне можетpushеслиfifoявляетсяfull
В приведенном мною примере я выбрал первую интерпретацию свойства.