Untitled

/* 
   This is a more compact, parameterized version 
   of the previous model.

   It should not hit memory or maximum depth limit 
   since the maximum amount of data that can be sent
   during the execution is deliberately limited by
   the MAX_COUNT limit. 
*/

mtype = { ERR }
chan s2r = [2] of { bit }  
chan r2s = [2] of { mtype }
short count[2] = { 0, 0 }
short MAX_COUNT = 50; // limit on how many bits sent
bool done[2] = { false, false }

proctype Sender(bit b; short id) {
  do
  :: s2r!b -> b++; 
     if 
     :: r2s?ERR -> break;
     :: s2r!b -> b++; 
     fi;
  :: r2s?ERR -> break;
  od;
  done[id] = true;
}

proctype Receiver() {
  bit b = 0, old, any;
  s2r?b; count[b]++; old = b; b++; 
  do
  :: if
     :: (count[0]  + count[1] > MAX_COUNT) -> break;
     :: else -> skip;
     fi;
     if 
     :: s2r?b -> 
        if
        :: b == old -> break;
        :: b = 1 - old -> old = b; count[b]++;  
        fi;
     fi;
  od;
  r2s!ERR;
  r2s!ERR;
  timeout;
  do
  :: len(s2r) > 0 -> s2r?any;
  :: len(s2r) == 0 -> break;
  od
}

init {
	run Sender(0, 0);
	run Sender(1, 1);
	run Receiver();
	assert((count[0] - count[1] == 1) || (count[0] - count[1] == 0) || (count[0] - count[1] == -1));
	timeout;
	assert(done[0] && done[1]);
}


ltl s2rAlwaysEventuallyEmptyWheneverErr { []((len(r2s) > 0) -> <>(len(s2r) == 0)) }
ltl r2sAlwaysEventuallyEmpty { []<>(len(r2s) == 0) }
ltl s2rEventuallyUsed { <>(len(s2r) > 0) }
ltl zerosAndOnezWithin1CountOfEachOther { []((count[0] - count[1] == 1) || (count[0] - count[1] == 0) || (count[0] - count[1] == -1)) }
ltl bothSendersEventuallyTerminate { <>(done[0] && done[1]) }