clientServer: THEORY
BEGIN

  % client indices and program counter constants
  Index : TYPE+ = { x: nat | x = 1 OR x = 2 } CONTAINING 1
  Index0: TYPE+ = { x: nat | x < 3 } CONTAINING 0
  PC: TYPE+ = { R, S, C }

  % client states
  pc, pc0: [ Index -> PC ]
  request, request0: [ Index -> bool ]
  answer, answer0: [ Index -> bool ]

  % server states
  given, given0: Index0
  waiting, waiting0: Index0
  sender, sender0: Index0
  rbuffer, rbuffer0: [ Index -> bool ]
  sbuffer, sbuffer0: [ Index -> bool ]

  i, j: VAR Index

  % ---------------------------------------------------------------------------
  % initial state condition
  % ---------------------------------------------------------------------------

  IC(pc: PC, request: bool, answer: bool): bool =
    pc = R AND request = FALSE AND answer = FALSE

  IS(given: Index0, waiting: Index0, sender: Index0, 
     rbuffer: [ Index -> bool ], sbuffer: [ Index -> bool ]): bool =
    given = 0 AND waiting = 0 AND sender = 0 AND
    (FORALL i: rbuffer(i) = FALSE AND sbuffer(i) = FALSE)

  Initial: bool =
    (FORALL i: IC(pc(i), request(i), answer(i))) AND 
    IS(given, waiting, sender, rbuffer, sbuffer)

  % ---------------------------------------------------------------------------
  % transition relation
  % ---------------------------------------------------------------------------

  RC(pc:  PC, request:  bool, answer:  bool,
     pc0: PC, request0: bool, answer0: bool): bool =
    (pc = R AND request = FALSE AND
      pc0 = S AND request0 = TRUE AND answer0 = answer) OR
    (pc = S AND answer = TRUE AND
      pc0 = C AND request0 = request AND answer0 = FALSE) OR
    (pc = C AND request = FALSE AND
      pc0 = R and request0 = TRUE AND answer0 = answer)

  RS(given: Index0, waiting: Index0, sender: Index0, 
       rbuffer: [ Index -> bool ], sbuffer: [ Index -> bool ],
     given0: Index0, waiting0: Index0, sender0: Index0, 
       rbuffer0: [ Index -> bool ], sbuffer0: [ Index -> bool ]): bool =

    (EXISTS i: 
      sender = 0 AND rbuffer(i) = TRUE AND
      sender0 = i AND rbuffer0(i) = FALSE AND
      given = given0 AND waiting = waiting0 AND sbuffer = sbuffer0 AND
      FORALL j: j /= i => rbuffer(j) = rbuffer0(j)) OR

    (sender /= 0 AND sender = given AND waiting = 0 AND
      given0 = 0 AND sender0 = 0 AND
      waiting = waiting0 AND rbuffer = rbuffer0 AND sbuffer = sbuffer0) OR

    (sender /= 0 AND
      sender = given AND waiting /= 0 AND
      sbuffer(waiting) = FALSE AND % change order for type-checking
      given0 = waiting AND waiting0 = 0 AND
      sbuffer0(waiting) = TRUE AND sender0 = 0 AND
      rbuffer = rbuffer0 AND
      (FORALL j: j /= waiting => sbuffer(j) = sbuffer0(j))) OR

    (sender /= 0 AND sbuffer(sender) = FALSE AND
      sender /= given AND given = 0 AND
      given0 = sender AND
      sbuffer0(sender) = TRUE AND sender0 = 0 AND
      waiting = waiting0 AND rbuffer = rbuffer0 AND
      (FORALL j: j /= sender => sbuffer(j) = sbuffer0(j))) OR

    (sender /= 0 AND sender /= given AND given /= 0 AND
      waiting0 = sender AND sender0 = 0 AND
      given = given0 AND rbuffer = rbuffer0 AND sbuffer = sbuffer0)

  External(i: Index, 
           pc:  PC, request:  bool, answer:  bool,
           pc0: PC, request0: bool, answer0: bool,
           given:  Index0,  waiting: Index0,  sender: Index0, 
             rbuffer: [ Index -> bool ],  sbuffer: [ Index -> bool ],
           given0: Index0, waiting0: Index0, sender0: Index0, 
             rbuffer0: [ Index -> bool ], sbuffer0: [ Index -> bool ]): bool =
    (request = TRUE AND 
      pc0 = pc AND request0 = FALSE AND answer0 = answer AND
      rbuffer0(i) = TRUE AND 
      given = given0 AND waiting = waiting0 AND sender = sender0 AND
      sbuffer = sbuffer0 AND
      (FORALL j: j /= i => rbuffer(j) = rbuffer0(j))) OR

    (pc0 = pc AND request0 = request AND answer0 = TRUE AND
      sbuffer(i) = TRUE AND sbuffer0(i) = FALSE AND
      given = given0 AND waiting = waiting0 AND sender = sender0 AND
      rbuffer = rbuffer0 AND
      (FORALL j: j /= i => sbuffer(j) = sbuffer0(j)))

  Next: bool =

    ((EXISTS i: RC(pc (i), request (i), answer (i),
                   pc0(i), request0(i), answer0(i)) AND
       (FORALL j: j /= i =>
         pc(j) = pc0(j) AND request(j) = request0(j) AND
         answer(j) = answer0(j))) AND
      given = given0 AND waiting = waiting0 AND sender = sender0 AND
      rbuffer = rbuffer0 AND sbuffer = sbuffer0) OR

    (RS(given,  waiting,  sender,  rbuffer,  sbuffer,
        given0, waiting0, sender0, rbuffer0, sbuffer0) AND
     (FORALL j: pc(j) = pc0(j) AND request(j) = request0(j) AND
                 answer(j) = answer0(j))) OR

    (EXISTS i: 
       External(i, pc (i), request (i), answer (i),
                   pc0(i), request0(i), answer0(i),
                given,  waiting,  sender,  rbuffer,  sbuffer,
                given0, waiting0, sender0, rbuffer0, sbuffer0) AND
       (FORALL j: j /= i =>
         pc(j) = pc0(j) AND request(j) = request0(j) AND
         answer(j) = answer0(j)))

  % ---------------------------------------------------------------------------
  % invariant
  % ---------------------------------------------------------------------------
  Invariant0(pc: [Index->PC], request: [Index -> bool], 
              answer: [Index -> bool], 
            given: Index0, waiting: Index0, sender: Index0, 
              rbuffer: [Index -> bool], sbuffer: [Index->bool]): bool = 
    FORALL i: 
      (pc(i) = C OR sbuffer(i) = TRUE OR answer(i) = TRUE => 
        given = i AND
        FORALL j: j /= i => 
           pc(j) /= C AND
           sbuffer(j) = FALSE AND answer(j) = FALSE) AND
      (pc(i) = R => 
        sbuffer(i) = FALSE AND answer(i) = FALSE AND
        (i /= given => 
          request(i) = FALSE AND rbuffer(i) = FALSE AND sender /= i) 
        (i = given =>
          request(i) = TRUE OR rbuffer(i) = TRUE OR sender = i) AND
        (request(i) = FALSE OR rbuffer(i) = FALSE)) AND
      (pc(i) = S =>
        (sbuffer(i) = TRUE OR answer(i) = TRUE =>
           request(i) = FALSE AND rbuffer(i) = FALSE AND sender /= i) AND
        (i /= given =>
           request(i) = FALSE OR rbuffer(i) = FALSE)) AND
      (pc(i) = C =>
        request(i) = FALSE AND rbuffer(i) = FALSE AND sender /= i AND
        sbuffer(i) = FALSE AND answer(i) = FALSE) AND
      (sender = 0 AND (request(i) = TRUE OR rbuffer(i) = TRUE) =>
         sbuffer(i) = FALSE AND answer(i) = FALSE) AND
      (sender = i =>
        (sender = given AND pc(i) = R => 
          request(i) = FALSE and rbuffer(i) = FALSE) AND
        (waiting /= i) AND
        (pc(i) = S AND i /= given =>
          request(i) = FALSE AND rbuffer(i) = FALSE) AND
        (pc(i) = S AND i = given =>
          request(i) = FALSE OR rbuffer(i) = FALSE)) AND
      (waiting = i =>
        given /= i AND
        pc(waiting) = S AND 
        request(waiting) = FALSE AND rbuffer(waiting) = FALSE AND
        sbuffer(waiting) = FALSE AND answer(waiting) = FALSE) AND
      (sbuffer(i) = TRUE => 
        answer(i) = FALSE AND request(i) = FALSE AND rbuffer(i) = FALSE)

  % ---------------------------------------------------------------------------
  % invariant proof
  % ---------------------------------------------------------------------------
  Inv1a: THEOREM
    Initial => 
    Invariant0(pc, request, answer, 
      given, waiting, sender, rbuffer, sbuffer)

  Inv2a: THEOREM
    Invariant0(pc, request, answer, 
       given, waiting, sender, rbuffer, sbuffer) AND Next =>
    Invariant0(pc0, request0, answer0, 
      given0, waiting0, sender0, rbuffer0, sbuffer0)

  % ---------------------------------------------------------------------------
  % mutual exclusion proof
  % ---------------------------------------------------------------------------
  MutExa: THEOREM
    Invariant0(pc, request, answer, 
      given, waiting, sender, rbuffer, sbuffer) =>
    NOT (pc(1) = C AND pc(2) = C)

END clientServer