mtype = { MESSAGE };

chan request[2] = [1] of { mtype };
chan answer [2] = [1] of { mtype };

proctype client(byte id)
{
  do :: true ->
    request[id-1] ! MESSAGE;
    A: answer[id-1]  ? MESSAGE;
    C: skip;
    request[id-1] ! MESSAGE
  od;
}

proctype server()
{
  unsigned given   : 2 = 0;
  unsigned waiting : 2 = 0;
  unsigned sender  : 2;
  do :: true ->
    R: if
    :: request[0] ? MESSAGE ->
      S1: sender = 1
    :: request[1] ? MESSAGE ->
      S2: sender = 2
    fi;

    if
    :: sender == given ->
      if
      :: waiting == 0 -> 
        given = 0
      :: else ->
        given = waiting;
        waiting = 0;
        answer[given-1] ! MESSAGE;
      fi;
    :: given == 0 ->
      given = sender;
      answer[given-1] ! MESSAGE
    :: else
      waiting = sender
    fi;
  od;  
}

init
{
  run client(1);
  run client(2);
  run server();
}

ltl mutex { []!(client[1]@C && client[2]@C) }
ltl progress1 { [](client[2]@ A -> <>client[2]@C) }
ltl progress2 {  
(([]<>(server@R && len(request[1])>0)) -> ([]<>server@S2)) -> 
    [](client[2]@A -> <>client[2]@C) }
ltl progress3 { 
(([]<>(server@R && len(request[1])>0)) -> ([]<>server@S2)) ->
  ([]<>client[2]@C) }