// -------------------------------------------------------------------------------------------
// a system with one server and N clients
// the server schedules a resource among the clients such that 
// at most one client holds the resource at a time
// -------------------------------------------------------------------------------------------

// the number of clients
val N:ℕ;

// the types
type Bit = ℕ[1];            // messages are just signals
type Client = ℕ[N];         // client ids 0..N-1, N: no client
type Buffer = Array[N,Bit]; // for each client a single message may be buffered

// the program counters of the clients
type PC = ℕ[2]; val R = 0; val S = 1; val C = 2;

// the system with one server and N clients
shared system clientServer
{
  // the state of the clients
  var pc: Array[N,PC] = Array[N,PC](R);
  var request: Buffer = Array[N,Bit](0);
  var answer: Buffer = Array[N,Bit](0);
  
  // the state of the server
  var given: Client = N;
  var waiting: Buffer = Array[N,Bit](0);
  var sender: Client = N;
  var rbuffer: Buffer = Array[N,Bit](0);
  var sbuffer: Buffer = Array[N,Bit](0);
  
  // the correctness property
  invariant ¬∃i1:Client,i2:Client with i1 ≠ N ∧ i2 ≠ N ∧ i1 < i2.
    pc[i1] = C ∧ pc[i2] = C;

  // the system invariants that imply the correctness property
  invariant ∀i:Client with i ≠ N ∧ pc[i] = R.
    sbuffer[i] = 0 ∧ answer[i] = 0 ∧ (request[i] = 0 ∨ rbuffer[i] = 0) ∧
    (i = given ⇔ request[i] = 1 ∨ rbuffer[i] = 1 ∨ sender = i);
  invariant ∀i:Client with i ≠ N ∧ pc[i] = S.
    (sbuffer[i] = 1 ∨ answer[i] = 1 ⇒ request[i] = 0 ∧ rbuffer[i] = 0 ∧ sender ≠ i) ∧
    (i ≠ given ⇒ request[i] = 0 ∨ rbuffer[i] = 0);
  invariant ∀i:Client with i ≠ N ∧ pc[i] = C.
    request[i] = 0 ∧ rbuffer[i] = 0 ∧ sender ≠ i ∧ sbuffer[i] = 0 ∧ answer[i] = 0;
  invariant ∀i:Client with i ≠ N ∧ (pc[i] = C ∨ sbuffer[i] = 1 ∨ answer[i] = 1).
    given = i ∧ ∀j:Client with j ≠ N ∧ j ≠ i. pc[j] ≠ C ∧ sbuffer[j] = 0 ∧ answer[j] = 0;
  invariant sender = N ⇒ ∀i:Client with i ≠ N ∧ (request[i] = 1 ∨ rbuffer[i] = 1). 
      sbuffer[i] = 0 ∧ answer[i] = 0;
  invariant ∀i:Client with i ≠ N ∧ sender = i.
    waiting[i] = 0;
  invariant ∀i:Client with i ≠ N ∧ sender = i ∧ pc[i] = R ∧ sender = given. 
    request[i] = 0 ∧ rbuffer[i] = 0;
  invariant ∀i:Client with i ≠ N ∧ sender = i ∧ pc[i] = S ∧ sender ≠ given. 
    request[i] = 0 ∧ rbuffer[i] = 0;
  invariant ∀i:Client with i ≠ N ∧ sender = i ∧ pc[i] = S ∧ sender = given. 
    request[i] = 0 ∨ rbuffer[i] = 0;
  invariant ∀i:Client with i ≠ N ∧ waiting[i] = 1.
    given ≠ i ∧ pc[i] = S ∧ 
    request[i] = 0 ∧ rbuffer[i] = 0 ∧ sbuffer[i] = 0 ∧ answer[i] = 0;
  invariant ∀i:Client with i ≠ N ∧ sbuffer[i] = 1.
    answer[i] = 0 ∧ request[i] = 0 ∧ rbuffer[i] = 0; 

  // the client transitions
  action R(i:Client) with i ≠ N ∧ pc[i] = R ∧ request[i] = 0;
  {
    pc[i] ≔ S; request[i] ≔ 1; 
  }
  action S(i:Client) with i ≠ N ∧ pc[i] = S ∧ answer[i] ≠ 0;
  {
    pc[i] ≔ C; answer[i] ≔ 0;
  }
  action C(i:Client) with i ≠ N ∧ pc[i] = C ∧ request[i] = 0;
  {
    pc[i] ≔ R; request[i] ≔ 1;
  }
  
  // the server transitions
  action D(i:Client) with i ≠ N ∧ sender = N ∧ rbuffer[i] ≠ 0;
  {
    sender ≔ i; rbuffer[i] ≔ 0;
  }
  action F() with sender ≠ N ∧ sender = given ∧ 
    ∀i:Client with i ≠ N. waiting[i] = 0;
  {
    given ≔ N; sender ≔ N;
  }
  action A1(i:Client) with i ≠ N ∧ 
    sender ≠ N ∧ sender = given ∧ waiting[i] ≠ 0 ∧ 
    sbuffer[i] = 0;
  {
    given ≔ i; waiting[i] = 0;
    sbuffer[given] ≔ 1; sender ≔ N;
  }
  action A2() with sender ≠ N ∧ sender ≠ given ∧ given = N ∧
    sbuffer[sender] = 0;
  {
    given ≔ sender; sbuffer[given] ≔ 1; sender ≔ N;
  }
  action W() with sender ≠ N ∧ sender ≠ given ∧ given ≠ N;
  {
    waiting[sender] ≔ 1 ; sender ≔ N;
  }
  
  // the transitions of the communication subsystem
  action REQ(i:Client) with i ≠ N ∧ request[i] ≠ 0 ∧ rbuffer[i] = 0;
  {
    request[i] ≔ 0; rbuffer[i] ≔ 1;
  }
  action ANS(i:Client) with i ≠ N ∧ sbuffer[i] ≠ 0 ∧ answer[i] = 0;
  {
    sbuffer[i] ≔ 0; answer[i] ≔ 1;
  }
}

