пожалуйста, я большой специалист в области tihs, как я могу преобразовать классический пример FIFO, написанный в коде systemC, в язык PROMELA со свойствами в LTL, удовлетворяющими следующим трем свойствам:
Взаимное исключение: процессы производителя и потребителя никогда не обращаются к общему буферу одновременно.
Не голодание: потребитель обращается к буферу бесконечно часто. (Вы можете предположить, что у производителя никогда не заканчиваются данные для предоставления, а потребитель никогда не прекращает попытки прочитать новые данные.)
Производитель-потребитель: производитель никогда не перезаписывает буфер данных, если только потребитель уже не прочитал текущие данные. Потребитель никогда не читает буфер данных, если он не содержит новых данных. Обычный алгоритм для производителя-потребителя использует один флаговый бит. Бит флага устанавливается производителем, когда данные готовы к чтению, и сбрасывается потребителем после того, как он прочитал данные. Ради этого назначения нам нужно только моделировать, был ли прочитан буфер данных, а не моделировать содержимое данных. Для этого мы будем использовать один бит.
Ваша задача — смоделировать этот алгоритм в Promela, а затем проверить указанные выше свойства. Полезно помнить, что (1) и (3) — это свойства безопасности, а (2) — это свойство живучести. Вы можете использовать как LTL, так и встроенные утверждения, где это уместно.
Это моя первая попытка решить эту проблему:
#define NUMCHAN 4
chan channels[NUMCHAN];
chan full[0];
init
{
chan ch1 = [1] of { byte };
chan ch2 = [1] of { byte };
chan ch3 = [1] of { byte };
chan ch4 = [1] of { byte };
channels[0] = ch1;
channels[1] = ch2;
channels[2] = ch3;
channels[3] = ch4;
// Add further channels above, in accordance with NUMCHAN
// First let the producer write something, then start the consumer
run producer();
atomic {
_nr_pr == 1 -> run consumer();
}
}
proctype read()
{
byte var, i;
chan theChan;
do
:: fread?1 ->
if readptr == writeptr -> empty ! 1
fi
read ! 0
readptr = readptr+1 mod NUMCHAN
ack ?1
od
ack!1
i = 0;
do
:: i == NUMCHAN -> break
:: else -> theChan = channels[i];
if
:: skip // non-deterministic skip
:: nempty(theChan) ->
theChan ? var;
printf("Read value %d from channel %d\n", var, i+1)
fi;
i++
od
}
proctype consumer()
{
do // empty
if
empty ? 0 // read // data
theChan ? data
:: fread!1 -> ack ?1
od
}
Я создал два основных процесса: производитель и потребитель.
Производитель связан с другим процессом, называемым write, посредством канала fwrite, а потребитель связан с другим процессом, называемым прочитано по каналу fread. Здесь read и write содержат указатели read и write.
Потребитель неполный, я только набросал идею, которая у меня есть. Я хочу, чтобы чтение происходило после полной записи каналов или таблицы FIFO и что производитель может записать N количество информации, не довольствуясь размером FIFO.
