свойство LTL и программа Promela

Question

У меня есть следующая программа, которая моделирует 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 и использовать его для проверки?

---

от комментариев: и я хочу, чтобы проверить это свойство, например, если ФИФО заполнен, один не должен иметь запрос на запись, что это правильный синтаксис полный означает, что ФИФО полно и wr_idx? является указателем записи, я не знаю, как получить доступ к полной, пустой, wr_idx, rd_idx, глубине процесса fifo в свойствах ltl fifo_no_write_when_full {[] (full ->! wr_idx)}

Answer 1

Вот пример от на основе процесса FIFO с размером 1, который я дал вам here, приспособленный для произвольного размер, который можно настроить с помощью 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, глубина на процессе ФИФО в свойства Ltl fifo_no_write_when_full {[] (полный ->! wr_idx)}

Первый всего, обратите внимание, что в моем коде rd_idx соответствует head, depth(должны) соответствуют count и что я не использовал явный wr_idx, поскольку последний может быть получен от первых двух: он задается (head + count) % FIFO_SIZE.Это не просто выбор чистоты кода, потому что с меньшим количеством переменных в модели Promela на самом деле помогает с память потребление и время работы процесса проверки.

Конечно, если вы действительно хотите иметь wr_idx в своей модели, вы можете добавить его самостоятельно. (:

Второй, если вы посмотрите на Promelamanual для 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

В примере я предоставил я выбрал принять первую интерпретацию собственности.