// -----------------------------------------------------------------
//
// System.txt
// RISCAL specifiation of a client-server system
//
// (c) 2020, Wolfgang Schreiner: Thinking Programs
// 
// -----------------------------------------------------------------
 
val N = 4; axiom minN ⇔ N ≥ 1;
type Client  = ℕ[N-1];
type Client0 = ℕ[N];
type PC = ℕ[2];

// -----------------------------------------------------------------
// a shared variant of the system
// -----------------------------------------------------------------

shared system ClientServer1
{
  var given: Client0;       // the client allowed to enter (N, if none)
  var waiting: Set[Client]; // the set of clients waiting to enter
  var pc: Array[N,PC];      // the program counters of the clients
  var req: Set[Client];     // the set of pending client requests
  var ans: Set[Client];     // the set of pending server answers
  
  // the mutual exclusion property
  invariant ¬∃i1:Client,i2:Client with i1 < i2. pc[i1] = 2 ∧ pc[i2] = 2;
  
  // further invariants (inductive, imply mutual exclusion)
  invariant ∀i:Client with i = given.
    (pc[i] = 0 ∧ i ∈ req) ∨ (pc[i] = 1 ∧ i ∈ ans) ∨ 
    (pc[i] = 2 ∧ i ∉ req ∧ i ∉ ans);
  invariant ∀i:Client with i ∈ waiting.
    i ≠ given ∧ pc[i] = 1 ∧ i ∉ req ∧ i ∉ ans;
  invariant ∀i: Client with i ∈ req. i ∉ ans;
  invariant ∀i: Client with i ∈ ans. given = i;
  invariant ∀i: Client with pc[i] = 0. i ∉ ans ∧ (i ∈ req ⇒ i = given);
  invariant ∀i: Client with pc[i] = 1. i ∈ req ∨ i ∈ waiting ∨ i ∈ ans;
  invariant ∀i: Client with pc[i] = 2. i = given;
  
  init()
  {
    given ≔ N;
    waiting ≔ ∅[Client];
    pc ≔ Array[N,PC](0);
    req ≔ ∅[Client];
    ans ≔ ∅[Client];
  }
  
  // client i asks to enter the critical region
  action cask(i:Client) with pc[i] = 0 ∧ i ∉ req;
  {
    pc[i] ≔ 1; req ≔ req ∪ {i};
  }
  
  // client i gets permission to enter the critical region
  action cget(i:Client) with pc[i] = 1 ∧ i ∈ ans;
  {
    pc[i] ≔ 2; ans ≔ ans \ {i};
  }
  
  // client i leaves the critical region and returns the permission
  action cret(i:Client) with pc[i] = 2 ∧ i ∉ req;
  {
    pc[i] ≔ 0; req ≔ req ∪ {i};
  }
  
  // server receives request from client i and immediately answers it
  action sget(i:Client) with i ∈ req ∧ given = N ∧ i ∉ ans;
  {
    req ≔ req \ {i}; given ≔ i; ans ≔ ans ∪ {i};
  }
  
  // server receives request from client i and puts it on hold
  action swait(i:Client) with i ∈ req ∧ given ≠ N ∧ given ≠ i;
  {
    req ≔ req \ {i}; waiting ≔ waiting ∪ {i};
  }
  
  // server gets permission back from client i
  action sret1(i:Client) with i ∈ req ∧ given = i ∧ waiting = ∅[Client];
  {
    req := req \ {i}; given ≔ N; 
  }
  
  // server gets permission back from client i and forwards it to client j
  action sret2(i:Client,j:Client) with i ∈ req ∧ given = i ∧ j ∈ waiting ∧ j ∉ ans;
  {
    req := req \ {i}; given ≔ j;  waiting = waiting \ {j}; ans ≔ ans ∪ {j};  
  }  
}

// -----------------------------------------------------------------
// a distributed variant of the system
// -----------------------------------------------------------------

val B = N; axiom minB ⇔ B ≥ 1;

// the number of requests in buffer b of size bn from client i
fun number(b:Array[B,Record[i:Client]],bn:ℕ[B],i:Client):ℕ[B] =
  #k:ℕ[B] with k < bn ∧ b[k].i = i; 

distributed system ClientServer2
{
  // the mutual exclusion property
  invariant ∀i1:Client, i2:Client.
    (Client[i1].use = 1 ∧ Client[i2].use = 1 ⇒ i1 = i2);

  // an inductive invariant that implies mutual exclusion
  invariant ∀i:Client. 
    (Client[i].ask_number + Client[i].enter_number + Client[i].exit_number
     + number(Server.request, Server.request_number, i) = 1);
  invariant ∀i:Client. 
    number(Server.giveback, Server.giveback_number, i) ≤ 1;
  invariant ∀i:Client. 
    number(Server.giveback, Server.giveback_number, i) = 1 ⇒
    Client[i].enter_number = 0 ∧ Client[i].exit_number = 0;
  invariant ∀i:Client. 
    (Client[i].req = 1 ⇔
      number(Server.request, Server.request_number, i) = 1 ∨
      Client[i].enter_number = 1);
  invariant ∀i:Client. 
    (Client[i].use = 1 ⇔ Client[i].exit_number = 1);
  invariant ∀i:Client.
    (Server.client = i ⇔
      Client[i].enter_number = 1 ∨ Client[i].exit_number = 1 ∨
      number(Server.giveback, Server.giveback_number, i) = 1);

  // the server component with action buffers of size B
  component Server
  {
    var client:Client0;
    init() 
    { 
      client := N; 
    }
    action[B] request(i:Client) with client = N;
    {
      client := i; 
      send Client[i].enter();
    }
    action[B] giveback(i:Client)
    {
      client ≔ N;
    }
  }
  
  // the N client components (with action buffers of size 1)
  component Client[N]
  {
    var req: ℕ[1];
    var use: ℕ[1];
    init() 
    { 
      req ≔ 0;
      use ≔ 0;
      send Client[this].ask();
    }
    action ask()
    {
      req ≔ 1;
      send Server.request(this);
    }
    action enter()
    {
      req ≔ 0;
      use ≔ 1;
      send Client[this].exit();
    }
    action exit()
    {
      use ≔ 0;
      send Server.giveback(this);
      send Client[this].ask();
    }
  }
}

// -----------------------------------------------------------------
// invariant-based verification of mutual exclusion
// -----------------------------------------------------------------

type State = Record[
  given: Client0,
  waiting: Set[Client],
  pc: Map[Client,PC],
  req: Set[Client],
  ans: Set[Client]
];
 
pred I(s:State) ⇔
  s.given = N ∧
  s.waiting = ∅[Client] ∧
  s.pc = Map[Client,PC](0) ∧
  s.req = ∅[Client] ∧
  s.ans = ∅[Client]
;

rectype(0) Action =
  Request(Client) | Get(Client) | Return(Client) |
  Return1(Client) | Return2(Client,Client) | 
  Request1(Client) | Request2(Client);
  
pred enabled(a:Action,s:State) ⇔
  match a with
  {
    Request(i:Client) -> 
      s.pc[i] = 0 ∧ ¬(i ∈ s.req);
    Get(i:Client) -> 
      s.pc[i] = 1 ∧ i ∈ s.ans;
    Return(i:Client) -> 
      s.pc[i] = 2 ∧ ¬(i ∈ s.req);
    Return1(i:Client) -> 
      i ∈ s.req ∧ i = s.given ∧ s.waiting = ∅[Client];
    Return2(i:Client,g:Client) -> 
      i ∈ s.req ∧ i = s.given ∧ g ∈ s.waiting ∧ ¬(g ∈ s.ans);
    Request1(i:Client) -> 
      i ∈ s.req ∧ i ≠ s.given ∧ s.given = N ∧ ~(i ∈ s.ans);
    Request2(i:Client) -> 
      i ∈ s.req ∧ i ≠ s.given ∧ s.given ≠ N;
  }
;

fun execute(a:Action,s:State):State =
  match a with
  {
    Request(i:Client) -> 
      s with .pc = (s.pc with [i] = 1) with .req = s.req∪{i};
    Get(i:Client) -> 
      s with .pc = (s.pc with [i] = 2) with .ans = s.ans\{i};
    Return(i:Client) -> 
      s with .pc = (s.pc with [i] = 0) with .req = s.req∪{i};
    Return1(i:Client) -> 
      s with .req = s.req\{i} with .given = N;
    Return2(i:Client,g:Client) -> 
      s with .req = s.req\{i} with .given = g 
        with .waiting = s.waiting\{g} with .ans = s.ans∪{g};
    Request1(i:Client) -> 
      s with .req = s.req\{i} with .given = i with .ans = s.ans∪{i};
    Request2(i:Client) -> 
      s with .req = s.req\{i} with .waiting = s.waiting∪{i};
  }
;

pred MutEx(s:State) ⇔ 
  ∀i:Client,j:Client with i≠j. ¬(s.pc[i] = 2 ∧ s.pc[j] = 2);

pred Invariant(s:State) ⇔ 
  ∀i:Client.
    (i = s.given ⇒
      (s.pc[i] = 0 ∧ i ∈ s.req) ∨
      (s.pc[i] = 1 ∧ i ∈ s.ans) ∨ 
      (s.pc[i] = 2 ∧ ¬(i ∈ s.req) ∧ ¬(i ∈ s.ans))) ∧ 
    (i ∈ s.waiting ⇒
      i ≠ s.given ∧ s.pc[i] = 1 ∧ ¬(i ∈ s.req) ∧ ¬(i ∈ s.ans)) ∧
    (i ∈ s.req ⇒ ¬(i ∈ s.ans)) ∧
    (i ∈ s.ans ⇒ s.given = i) ∧
    (s.pc[i] = 0 ⇒ ¬(i ∈ s.ans) ∧
      (i ∈ s.req ⇒ i = s.given)) ∧
    (s.pc[i] = 1 ⇒ 
      i ∈ s.req ∨ i ∈ s.waiting ∨ i ∈ s.ans) ∧
    (s.pc[i] = 2 ⇒ i = s.given)
;

theorem MutEx0(s:State) ⇔ 
  Invariant(s) ⇒ MutEx(s);
theorem MutEx1(s:State) ⇔ 
  I(s) ⇒ Invariant(s);
theorem MutEx2(s:State) ⇔ 
  Invariant(s) ⇒
    ∀a:Action with enabled(a,s). 
      let s0 = execute(a,s) in Invariant(s0);

// -----------------------------------------------------------------
// end of file
// -----------------------------------------------------------------