byte a= 0;

active [5] proctype P() {  
  byte tmp, i;
  i=0;
  do
  :: i>=3 -> 
    break;
  :: else ->
    tmp=a; tmp++; a=tmp; 
      /* symulacja incr przy pomocy akumulatora
      */
    i++;
  od
}

ltl L1 {<>[] (a==15)}
ltl L2 {! <>[] (a==7)}
ltl L3 {! <>[] (a==2)} 
  /* L3 - nie dziala, wlacza sie OOM killer !
      po wl. swapa dziala ale wolno, nie udalo mi sie zakonczyc...
  */