mtype = {request, success, maybefailure, failure, notyet};

byte logc = notyet;
byte logs = notyet;

chan c2s = [0] of {byte};
chan s2c = [0] of {byte};


ltl p0a { (<>[](logc == success)) || (<>[](logc == maybefailure)) || (<>[](logc == failure))}
ltl p0b { (<>[](logs == success)) || (<>[](logs == failure)) || (<>[](logs == notyet))}

ltl p1 { (<>[](logc == success)) -> (<>[](logs == success)) }
ltl p2 { (<>[](logs == success)) -> (<>[](logc == success)) }
ltl p3 { (<>[](logc == failure)) -> (<>[](logs == failure)) }
ltl p4 { (<>[](logs == failure)) -> (<>[](logc == failure)) }
ltl p5 { (<>[](logs == failure)) -> ((<>[](logc == failure)) || (<>[](logc == maybefailure)))}


active proctype client(){
  byte rmsg;
  bool retried = false;

  start:
  c2s ! request;
  if
    :: s2c ? rmsg -> 
       if
         :: rmsg == success ->
            logc = success
         :: rmsg == failure ->
            logc = failure
       fi
    :: timeout ->
       if
         :: !retried ->
            retried = true;
            goto start
         :: else -> logc = maybefailure
       fi
  fi
}

active proctype server(){
  byte rmsg;

  reset:
  do
    :: c2s ? rmsg ->
       if
         :: logs != notyet ->
            s2c ! logs
         :: else ->
            if
              :: logs = success;
                 s2c ! success
              :: logs = failure;
                 s2c ! failure
            fi
       fi
  od
}

active proctype network_loss(){
  byte rmsg;
  do
    :: s2c ? rmsg
    :: c2s ? rmsg
  od
}