% This file contains a variant of the mCRL2 version of the sliding window protocol
% as it occurs in the book "Modelling Reactive Systems" by Fokkink, Groote
% and Reniers. The buffers are modelled using lists instead of functions as is
% done in swp_func.mcrl2.
%
% The `constant' n is the size of the buffers in the protocol, set to 2.
% There is a domain D of data elements. In this specification it is made
% finite. It has an infinite number of data elements, modelled by the natural
% numbers. It also contains two unspecified lists q1 and q2, which represent
% initial buffers with garbage content.
%
% State space generation is impossible, but is feasible if the domain D is
% a finite set, e.g. by setting D = struct d1|d2;
% Absence of deadlock can be checked via translation to pbes and removing the
% data domain D using pbesparelm.

map  n: Pos;
eqn  n=2;

sort %D = Nat;
     D = struct d1 | d2;
     DBuf = List(D);
     BBuf = List(Bool);
map  empty: BBuf;
     insert: D#Nat#DBuf -> DBuf;
     insert: Bool#Nat#BBuf -> BBuf;
     nextempty_mod: Nat#BBuf#Nat#Pos -> Nat;
     q1,q2:DBuf;
var  d,d':D; i,j,m: Nat; q: DBuf; c,c':Bool; n':Pos; b:BBuf;
eqn  q1 = [d1, d1];
     q2 = q1;
     empty = [false,false];
     i == 0 -> insert(d,i,q) = d |> tail(q);
     i > 0 -> insert(d,i, d'|>q) = d' |> insert(d,Int2Nat(i-1),q);
     i == 0 -> insert(c,i,b) = c |> tail(b);
     i > 0 -> insert(c,i,c'|>b) = c' |> insert(c,Int2Nat(i-1),b);
     b.(i mod n') && m>0 ->
         nextempty_mod(i,b,m,n') = nextempty_mod((i+1) mod 2*n', b,Int2Nat(m-1),n');
     !(b.(i mod n') && m>0) ->
         nextempty_mod(i,b,m,n') =i mod 2*n';

act  r1,s4: D;
     s2,r2,c2,s3,r3,c3: D#Nat;
     s5,r5,c5,s6,r6,c6: Nat;
     i;

proc S(l,m:Nat,q:DBuf) =
        sum d:D. (m<n) ->
                r1(d).S(l,m+1,insert(d,(l+m) mod n,q))<>delta+
        sum k:Nat. (k<m) -> s2(q.((l+k) mod n),(l+k) mod 2*n).S(l,m,q)<>delta+
        sum k:Nat. r6(k).S(k,(m-k+l) mod 2*n,q);

     R(l':Nat,q':DBuf,b:BBuf) =
        sum d:D,k:Nat. r3(d,k).(((k-l') mod (2*n) < n)
                  -> R(l',insert(d,k mod n,q'),insert(true,k mod n,b))
                  <> R(l',q',b))+
        (b.(l' mod n)) -> s4(q'.(l' mod n)).
                          R((l'+1) mod 2*n,q',insert(false,l' mod n,b))<>delta+
        s5(nextempty_mod(l',b,n,n)).R(l',q',b);

     K = sum d:D,k:Nat. r2(d,k).(i.s3(d,k)+i).K;
     L = sum k:Nat. r5(k).(i.s6(k)+i).L;

     SWP(q,q':DBuf)=
        allow({c2,c3,c5,c6,i,r1,s4},
           comm({r2|s2->c2, r3|s3->c3, r5|s5->c5, r6|s6->c6},
              S(0,0,q) ||
              K ||
              L ||
              R(0,q',empty)));

init SWP(q1,q1);
