ltl p1 { [](sender:x==0 -> <>(receiver:r==0||receiver:corrupt==true))&& [](sender:x==1 -> <>(receiver:r==1||receiver:corrupt==true))&&[](sender:x==2 -> <>(receiver:r==2||receiver:corrupt==true))&&[](sender:x==3 -> <>(receiver:r==3||receiver:corrupt==true))}
chan link = [2] of {byte} ;

proctype sender(chan c) {
  byte x = 0 ;
  do /* repeat forever */
  :: printf("Sending %u\n", x) ; c!x ; x = (x+1)%4 ;
  od ;
}

proctype receiver(chan c) {
  byte r ;
  byte trash ;
  bool corrupt = false ;
  do /* repeat forever */
  :: c?r     -> corrupt = false ; printf("Receiving %u\n", r) ;
  :: c?trash -> corrupt = true  ; printf("CORRUPTED\n") ; (false) ;
  od ;
}

init {
  run sender(link) ;
  run receiver(link) ;
}