%%
%% N : the number of nodes
%% L : the capacity of the queue
%% M : the number of requests each node makes
%%
%% L should be greater than or equal to N.
%%

skdmxa{; N : nznat, L : nznat, M : nznat}: CONTEXT =
BEGIN
  %%
  %% Data types and their functions are defined.
  %%

  %%
  %% Node IDs are denoted by [1..N].
  %%
  Node_Id: TYPE = [1..N];

  %%
  %% Queue indexes are denoted by [0..(L+1)].
  %& Subtraction '-' cannot be done for those in [1..(L+1)].
  %% So, [0..(L+1)] is used instead.
  %%
  Queue_Idx: TYPE = [0..(L+1)];

  %%
  %% Each node makes requests M times to enter its critical section.
  %%
  Bnat: TYPE = [0..M];

  %%
  %% A queue is represented using an array data and a pointer tl.
  %% tl points an array element, in which an item is put next.
  %% If tl is 1, then the queue is empty.
  %% The first element of the array is the top of the queue if the
  %% queue is not empty.
  %%
  Queue: TYPE = [# data: ARRAY Queue_Idx OF Node_Id,
                   tl: Queue_Idx #];

  new_empty_queue: Queue = (# data := [[i : Queue_Idx] 1],
                              tl := 1 #);

  full?(queue : Queue): BOOLEAN = (queue.tl = L+1);

  empty?(queue : Queue): BOOLEAN = (queue.tl = 1);

  %% %% doesn't work because both i and queue.tl are vars
  %% in_aux?(queue : Queue, node : Node_Id, i : Queue_Idx): BOOLEAN =
  %%  IF i = queue.tl THEN false
  %%  ELSIF queue.data[i] = node THEN true
  %%  ELSE in_aux?(queue, node, i+1)
  %%  ENDIF;

  in_aux?(queue : Queue, node : Node_Id, i : Queue_Idx): BOOLEAN =
    IF i = L+1 THEN false
    ELSIF queue.data[i] = node THEN i < queue.tl
    ELSE in_aux?(queue, node, i+1)
    ENDIF;

  in?(queue : Queue, node : Node_Id): BOOLEAN = in_aux?(queue, node, 1);
    
  top(queue : Queue): Node_Id = queue.data[1];

  put(queue : Queue, i : Node_Id): Queue =
    IF full?(queue)
    THEN queue
    ELSE (queue WITH .data[queue.tl] := i) WITH .tl := queue.tl + 1
    ENDIF;

  get_aux(queue : Queue, i : Queue_Idx): Queue =
    IF i = L+1
    THEN queue WITH .tl := (queue.tl - 1)
    ELSE get_aux(queue WITH .data[i] := queue.data[i+1], i+1)
    ENDIF;

  get(queue : Queue): Queue = 
    IF empty?(queue)
    THEN queue
    ELSE get_aux(queue, 1)
    ENDIF;

  %%
  %% Request messages
  %%
  Request: TYPE = [# node: Node_Id, no: Bnat #]; 

  ReqMsg: TYPE = [# new: BOOLEAN, req: Request #];

  %%
  %% Privilege messages
  %%
  Privilege: TYPE = [# queue: Queue, done: ARRAY Node_Id OF Bnat #]; 

  PrivMsg: TYPE = [# new: BOOLEAN, priv: Privilege #];

  %%
  %% Labels
  %%
  Label: TYPE = {rem, l1, l2, l3, l4, l5, cs, l6, l7, l8, l9, l10};

  %%
  %% The behavior of each node is defined
  %%
  node [i : Node_Id]: MODULE =
  BEGIN
    %%
    %% reqmedium[i][j] denotes a channel with which node i sends a
    %% request to node j. 
    %% privmedium[i][j] denotes a channel with which node i sends a
    %% privilege to node j.
    %%
    GLOBAL reqmedium : ARRAY Node_Id OF ARRAY Node_Id OF ReqMsg
    GLOBAL privmedium : ARRAY Node_Id OF ARRAY Node_Id OF PrivMsg
    %%
    LOCAL requesting : BOOLEAN
    LOCAL have_privilege : BOOLEAN 
    LOCAL rn : ARRAY Node_Id OF Bnat
    LOCAL ln : ARRAY Node_Id OF Bnat
    LOCAL queue : Queue
    LOCAL idx : Node_Id
    LOCAL pc : Label
    LOCAL num_of_req : Bnat
    INITIALIZATION
      reqmedium = [[j : Node_Id] [[k : Node_Id] 
                    (# new := false, 
                       req := (# node := 1, 
                                 no := 0 #) #)]];
      privmedium = [[j : Node_Id] [[k : Node_Id] 
                    (# new := false, 
                       priv := (# queue := new_empty_queue,
                                  done := [[l : Node_Id] 1] #) #)]];
      requesting = false;
      have_privilege = IF i = 1 THEN true ELSE false ENDIF;
      rn = [[j : Node_Id] 0];
      ln = [[j : Node_Id] 0];
      queue = new_empty_queue;
      idx = 1;
      pc = rem;
      num_of_req = 0
    TRANSITION
    [
      try:
        pc = rem 
        --> pc' = IF num_of_req < M THEN l1 ELSE rem ENDIF;
            num_of_req' = IF num_of_req < M 
                          THEN num_of_req + 1
                          ELSE num_of_req 
                          ENDIF
      []
      set_req:
        pc = l1 --> pc' = l2;
                    requesting' = true
      []
      check_priv:
        pc = l2 --> pc' = IF have_privilege THEN cs ELSE l3 ENDIF
      []
      inc_req_no:
        pc = l3 --> pc' = l4;
                    rn'[i] = rn[i] + 1;
                    idx' = 1
      []
      send_req:
        pc = l4 --> pc' = IF idx = N THEN l5 ELSE l4 ENDIF;
                    reqmedium'[i][idx] 
                    = (# new := true,
                         req := (# node := i,
                                   no := rn[i] #) #);
                    idx' = IF idx = N THEN idx ELSE idx + 1 ENDIF
                    %%
                    %% The following is not appropriate because if idx
                    %%  = N, then idx + 1 is out of the range [1..N].
                    %% idx' = idx + 1
      []
      ([] (j : Node_Id):
      wait_priv:
        pc = l5 AND privmedium[j][i].new AND NOT(j = i)
        --> pc' = cs;
            have_privilege' = true;
            privmedium'[j][i] = (# new := false, 
                                  priv := (# queue := new_empty_queue,
                                             done := [[l : Node_Id] 1] #) #);
            queue' = privmedium[j][i].priv.queue;
            ln' = privmedium[j][i].priv.done)
      []
      exit:
        pc = cs --> pc' = l6
      []
      complete_req:
        pc = l6 --> pc' = l7;
                    ln'[i] = rn[i];
                    idx' = 1
      []
      update_queue:
        pc = l7 --> pc' = IF idx = N THEN l8 ELSE l7 ENDIF;
                    queue' = IF NOT(in?(queue, idx)) AND rn[idx] = ln[idx]+1
                             THEN put(queue, idx)
                             ELSE queue 
                             ENDIF;
                    idx' = IF idx = N THEN idx ELSE idx + 1 ENDIF
      []
      check_queue:
        pc = l8 --> pc' = IF empty?(queue) THEN l10 ELSE l9 ENDIF;
      []
      transfer_priv:
        pc = l9 --> pc' = l10;
                    have_privilege' = false;
                    privmedium'[i][top(queue)]
                    = (# new := true,
                         priv := (# queue := get(queue),
                                    done := ln #) #)
      []
      reset_req:
        pc = l10 --> pc' = rem;
                     requesting' = false
      []
      ([] (j : Node_Id):
      receive_req:
        reqmedium[j][i].new AND NOT(j = i)
        --> reqmedium'[j][i] = (# new := false,
                                  req := (# node := 1,
                                            no := 0 #) #);
            rn'[j] = IF rn[j] < reqmedium[j][i].req.no 
                     THEN reqmedium[j][i].req.no 
                     ELSE rn[j]
                     ENDIF;
            have_privilege' 
            = IF have_privilege AND NOT(requesting) AND rn'[j] = ln[j] + 1
              THEN false
              ELSE have_privilege
              ENDIF;
            privmedium'[i][j]
            = IF have_privilege AND NOT(requesting) AND rn'[j] = ln[j] + 1
              THEN (# new := true,
                      priv := (# queue := queue,
                                 done := ln #) #)
              ELSE privmedium[i][j]
              ENDIF)
    ]
  END;

  system: MODULE = ([] (i : Node_Id): node[i]);

%% mutual exclusion
%%
%% % sal-smc -v 3 --assertion='skdmxa{;2,2,2}!mutex'
%%
  mutex: THEOREM
    system |- G(FORALL (i : Node_Id, j : Node_Id):
                 (pc[i] = cs AND pc[j] = cs) => (i = j));

%% reachable to the critical section
%%
%% % sal-wmc -v 3 --assertion='skdmxa{;2,2,2}!reachable'
%% 
  reachable: THEOREM
    system |- (FORALL (i : Node_Id): EF(pc[i] = cs));

%% deadlock freedom
%%
%% % sal-deadlock-checker -v 3 --module='skdmxa{;2,2,2}!system'
%% 

%% lockout (starvation) freedom
%%
%% % sal-smc -v 3 --assertion='skdmxa{;2,2,2}!lofree'
%% 
  lofree: THEOREM
    system |- (FORALL (i : Node_Id, j : Node_Id): 
                G((G(pc[i] = l5 AND 
                     (EXISTS (k : Node_Id): privmedium[k][i].new AND NOT(k = i)))
                   => F(pc[i] = cs)) AND
                  (G(reqmedium[i][j].new) => F(NOT(reqmedium[i][j].new))) )
                  => G(pc[i] = l5 => F(pc[i] = cs)) );

END