% -------------------------------------------------------------------
%
% Verification of a small client/server system.
%
% -------------------------------------------------------------------

newcontext "clientServer";

% -------------------------------------------------------------------
% types and program variables
% -------------------------------------------------------------------

Index: TYPE = SUBTYPE(LAMBDA(x:INT): x=1 OR x=2);
Index0: TYPE = SUBTYPE(LAMBDA(x:INT): x=0 OR x=1 OR x=2);

PCBASE: TYPE;
R: PCBASE;
S: PCBASE;
C: PCBASE;
PC: TYPE = SUBTYPE(LAMBDA(x:PCBASE): x=R OR x=S OR x=C);
PCs: AXIOM R /= S AND R /= C AND S /= C;

pc: Index->PC; 
pc0: Index->PC;
request: Index->BOOLEAN; 
request0: Index->BOOLEAN;
answer: Index->BOOLEAN; 
answer0: Index->BOOLEAN;

given: Index0;
given0: Index0;
waiting: Index0;
waiting0: Index0;
sender: Index0;
sender0: Index0;
rbuffer: Index -> BOOLEAN;
rbuffer0: Index -> BOOLEAN;
sbuffer: Index -> BOOLEAN;
sbuffer0: Index -> BOOLEAN;

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

IC: (PC, BOOLEAN, BOOLEAN) -> BOOLEAN =
  LAMBDA(pc: PC, request: BOOLEAN, answer: BOOLEAN):
    pc = R AND (request <=> FALSE) AND (answer <=> FALSE);

IS: (Index0, Index0, Index0, Index->BOOLEAN, Index->BOOLEAN) -> BOOLEAN =
  LAMBDA(given: Index0, waiting: Index0, sender: Index0,
         rbuffer: Index->BOOLEAN, sbuffer: Index->BOOLEAN):
    given = 0 AND waiting = 0 AND sender = 0 AND
    (FORALL(i:Index): (rbuffer(i)<=>FALSE) AND (sbuffer(i)<=>FALSE));

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

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

RC: (PC, BOOLEAN, BOOLEAN, PC, BOOLEAN, BOOLEAN)->BOOLEAN =
  LAMBDA(pc: PC, request: BOOLEAN, answer: BOOLEAN,
         pc0: PC, request0: BOOLEAN, answer0: BOOLEAN): 
    (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: (Index0, Index0, Index0, Index->BOOLEAN, Index->BOOLEAN,
     Index0, Index0, Index0, Index->BOOLEAN, Index->BOOLEAN)->BOOLEAN =
  LAMBDA(given: Index0, waiting: Index0, sender: Index0,
         rbuffer: Index->BOOLEAN, sbuffer: Index->BOOLEAN, 
         given0: Index0, waiting0: Index0, sender0: Index0,
         rbuffer0: Index->BOOLEAN, sbuffer0: Index->BOOLEAN):

    (EXISTS(i:Index):
       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:Index): 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
       given0 = waiting AND waiting0 = 0 AND
       (sbuffer0(waiting)<=>TRUE) AND (sender0 = 0) AND
       (rbuffer = rbuffer0) AND
       (FORALL(j:Index): 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:Index): 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: (Index, PC, BOOLEAN, BOOLEAN, PC, BOOLEAN, BOOLEAN,
           Index0, Index0, Index0, Index->BOOLEAN, Index->BOOLEAN,
           Index0, Index0, Index0, Index->BOOLEAN, Index->BOOLEAN)->BOOLEAN =
  LAMBDA(i:Index, 
         pc: PC, request: BOOLEAN, answer: BOOLEAN,
         pc0: PC, request0: BOOLEAN, answer0: BOOLEAN,
         given: Index0, waiting: Index0, sender: Index0,
           rbuffer: Index->BOOLEAN, sbuffer: Index->BOOLEAN,
         given0: Index0, waiting0: Index0, sender0: Index0,
           rbuffer0: Index->BOOLEAN, sbuffer0: Index->BOOLEAN): 
    ((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: Index): 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: Index): j /= i => (sbuffer(j) <=> sbuffer0(j))));

Next: BOOLEAN =
  ((EXISTS (i: Index): 
      RC(pc(i), request(i), answer(i),
         pc0(i), request0(i), answer0(i)) AND
     (FORALL (j: Index): 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:Index): pc(j) = pc0(j) AND (request(j) <=> request0(j)) AND
      (answer(j) <=> answer0(j)))) OR

  (EXISTS (i: Index):
    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: Index): j /= i =>
      pc(j) = pc0(j) AND (request(j) <=> request0(j)) AND
      (answer(j) <=> answer0(j))));

% -------------------------------------------------------------------------------
% invariant
% -------------------------------------------------------------------------------

Invariant: (Index->PC, Index->BOOLEAN, Index->BOOLEAN,
            Index0, Index0, Index0, Index->BOOLEAN, Index->BOOLEAN) -> BOOLEAN =
  LAMBDA(pc: Index->PC, request: Index->BOOLEAN, answer: Index->BOOLEAN,
         given: Index0, waiting: Index0, sender: Index0,
         rbuffer: Index->BOOLEAN, sbuffer: Index->BOOLEAN):
    FORALL (i: Index):
      (pc(i) = C OR (sbuffer(i) <=> TRUE) OR (answer(i) <=> TRUE) =>
         given = i AND
         (FORALL (j: Index): 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) 
           AND
         (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));

% -------------------------------------------------------------------------------
% invariance proof
% -------------------------------------------------------------------------------

Inv1: FORMULA 
  Initial => 
    Invariant(pc, request, answer, given, waiting, sender, rbuffer, sbuffer);

Inv2: FORMULA 
  Invariant(pc, request, answer, given, waiting, sender, 
    rbuffer, sbuffer) AND Next =>
  Invariant(pc0, request0, answer0, given0, waiting0, sender0, 
    rbuffer0, sbuffer0);

% -------------------------------------------------------------------------------
% mutual exclusion proof
% -------------------------------------------------------------------------------

MutEx: FORMULA
  Invariant(pc, request, answer, given, waiting, sender, rbuffer, sbuffer) =>
  NOT(pc(1) = C AND pc(2) = C);