title: LTL properties and promela program
body: <p>I have the following program that models a <em>FIFO</em> with a <em>process</em> in <em>PROMELA</em>:</p>
  
  <pre><code>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 -&gt;
              inputs?command(tmp, src_uid);
              if
                  :: command == PUSH -&gt;
                      if
                          :: data_valid -&gt;
                              outputs!IS_FULL(true, src_uid);
                          :: else -&gt;
                              data = tmp
                              data_valid = true;
                              outputs!PUSH(data, src_uid);
                      fi
                  :: command == POP -&gt;
                      if
                          :: !data_valid -&gt;
                              outputs!IS_EMPTY(true, src_uid);
                          :: else -&gt;
                              outputs!POP(data, src_uid);
                              data = -1;
                              data_valid = false;
                      fi
                  :: command == IS_EMPTY -&gt;
                      outputs!IS_EMPTY(!data_valid, src_uid);
                  :: command == IS_FULL -&gt;
                      outputs!IS_FULL(data_valid, src_uid);
              fi;
      od;
  }
  
  proctype producer(chan inputs, outputs)
  {
      mtype command;
      int v;
  
      do
          :: true -&gt;
              atomic {
                  inputs!IS_FULL(false, PRODUCER_UID) -&gt;
                  outputs?IS_FULL(v, PRODUCER_UID);
              }
              if
                  :: v == 1 -&gt;
                      skip
                  :: else -&gt;
                      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 -&gt;
              atomic {
                  inputs!IS_EMPTY(false, CONSUMER_UID) -&gt;
                  outputs?IS_EMPTY(v, CONSUMER_UID);
              }
              if
                  :: v == 1 -&gt;
                      skip
                  :: else -&gt;
  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
  }
  </code></pre>
  
  <p>I want to add <code>wr_ptr</code> and <code>rd_ptr</code> in the program to indicate write and read pointers relative to the depth of FIFO when a <code>PUSH</code> update is performed:</p>
  
  <pre><code>wr_ptr = wr_ptr % depth;
  empty=0;
  if
      :: (rd_ptr == wr_ptr) -&gt; full=true; 
  fi
  </code></pre>
  
  <p>and similar chances on <code>POP</code> updates</p>
  
  <p>Could you please help me to add this to this program?</p>
  
  <p>or should i make it an ltl property and use that to check it?</p>
  
  <hr>
  
  <p><em>from comments:</em> and i want to verify this property, for example If the fifo is full, one should not have a write request, that is the right syntax?full means that fifo is full and wr_idx is the write pointer, I do not know how to access the full, empty, wr_idx, rd_idx, depth on the fifo process in the properties ltl fifo_no_write_when_full {[] (full -> ! wr_idx)} </p>