%% N : the number of processes
%% L : the capacity of the queue

qlock2{; N : nznat, L : nznat}: CONTEXT =
BEGIN
  Process_Id: TYPE = [1..N];

  Queue_Idx: TYPE = [0..(L + 1)];

  Queue_Ops: TYPE = {put, top?, get, nop};

  queue: MODULE =
  BEGIN
    INPUT q_op : Queue_Ops
    INPUT pid : Process_Id
    OUTPUT top : Process_Id
    OUTPUT sat? : BOOLEAN
    LOCAL data : ARRAY Queue_Idx OF Process_Id
    LOCAL hd : Queue_Idx
    LOCAL tl : Queue_Idx
    INITIALIZATION
      hd = 1;
      tl = 0
    DEFINITION
      top = data[hd];
      sat? = (tl = L) 
    TRANSITION
    [
      put: 
        (q_op' = put) AND NOT(tl = L)
        --> data' = data WITH [tl + 1] := pid';
            tl' = tl + 1
      []
      top:
        (q_op' = top?)
        -->
      []
      get:
        (q_op' = get)
        --> hd' = hd + 1
      []
      reset:
        (hd = tl + 1) AND (tl = L)
        --> hd' = 1;
            tl' = 0;
    ]      
  END;

  Label: TYPE = {l1, l2, cs};

  process [i : Process_Id]: MODULE =
  BEGIN
    INPUT top : Process_Id
    INPUT sat? : BOOLEAN
    GLOBAL q_op : Queue_Ops
    GLOBAL pid : Process_Id
    LOCAL pc : Label
    INITIALIZATION
      pc = l1;
    TRANSITION
    [
      want:
        (pc = l1) AND NOT(sat?)
        --> pc' = l2;
            q_op' = put;
            pid' = i
      []
      try:
        (pc = l2) AND (top = i)
        --> pc' = cs;
            q_op' = top?;
      []
      exit:
        (pc = cs) 
        --> pc' = l1;
            q_op' = get
      []
      else:
        ELSE 
        --> q_op' = nop
    ]
  END;

  processes : MODULE = OUTPUT pid , q_op IN ([] (i : Process_Id): process[i]);

  system: MODULE = processes || queue;

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

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

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


%% lockout (starvation) freedom
%%
%% % sal-smc -v 3 --assertion='qlock2{;2,2}!lofree'
%%
  lofree: THEOREM
    system |- (FORALL (i : Process_Id):
                G(pc[i] = l2 => F(pc[i] = cs)));

END