// -------------------------------------------------------------------------------------------
// 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 safety property
  ltl □ 〚∀i1:Client,i2:Client with i1 ≠ N ∧ i2 ≠ N ∧ i1 < i2.
           ¬(pc[i1] = C ∧ pc[i2] = C)〛;

  // the liveness property
  ltl[fairness] ∀i:Client with i ≠ N. □ (〚pc[i] = S〛 ⇒ (◇〚pc[i] = C〛));

  // 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;
  fairness strong_all; // strongly fairly accept request from every client
  {
    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;
  fairness strong_all; // treat every waiting client strongly fairly
  {
    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;
  fairness strong_all; // strongly fairly forward request from every client
  {
    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;
  }
}


