*** We define a "sliding window" data type to store the elements and
*** by the RC protocol to store the packet numbers it has received.

*** Note that we attempt to use the rationals!!

(fmod WINDOW is 
  protecting ORDERED-NAT-TIME-LIST .
  protecting RAT .

  *** Rationals with a default element (for division by 0):
  sort DefRat .
  subsort Rat < DefRat .
  op noRat : -> DefRat [ctor] .

  sort Window .

  op window : OrderedNzNatList NzNat Nat -> Window [ctor] .
  *** window(listOfElements, bound, noOfElsRecvdWithinInterval)

  *** Initialize window with bound:
  op initWindow : NzNat -> Window .
  op noOfTrues : Window -> Nat .
  op lowestMsgNo : Window -> Nat .    *** Default 0. OK???
  op size : Window -> Nat .
  op add : NzNat Window -> Window .   *** "user-constructor"
  op windowLPE : Window -> DefRat . 

  var W : Window .
  vars NZNL NZNL' : OrderedNzNatList .
  vars NZN NZN' NZN'' NZN''' NZN'''' : NzNat .
  var N : Nat .

  eq initWindow(NZN) = window(nil, NZN, 0) .
  eq noOfTrues(window(NZNL, NZN, N)) = N .
  eq lowestMsgNo(window(NZN ++ NZNL, NZN', N)) = NZN .
  eq lowestMsgNo(window(nil, NZN, 0)) = 0 .   *** ??????
  eq size(window(NZNL, NZN, N)) = 
        if last(NZNL) < NZN then last(NZNL) else NZN fi .
  *** When adding an element, the window may have to slide a little:
  eq add(NZN, window(nil, NZN', 0)) = window(NZN, NZN', 1) .

  eq add(NZN, window(NZN' ++ NZNL, NZN'', s N)) = 
        (if ((NZN' + NZN'') <= NZN) then *** remove elements in the beginning
            add(NZN, window(NZNL, NZN'', N))
         else    
           (if (NZN < NZN') then             *** add first:
               (if (last(NZN' ++ NZNL) < (NZN + NZN'')) then
                   *** but is there room for it?
                   window(NZN ++ (NZN' ++ NZNL), NZN'', s s N)
                else *** no room in front:
                   window(NZN' ++ NZNL, NZN'', s N) 
                fi)
            else (if NZN inList (NZN' ++ NZNL)
                  then window(NZN' ++ NZNL, NZN'', s N)
                  else window(add(NZN, NZN' ++ NZNL), NZN'', s s N)
                  fi)
            fi)
         fi) .

  eq add(NZN, window(NZN', NZN'', NZN''')) = 
        if NZN == NZN' then  window(NZN', NZN'', NZN''')
        else (if NZN < NZN' then
                 (if NZN' < NZN + NZN'' 
                  then window(NZN ++ NZN', NZN'', NZN''' + 1)
                  else window(NZN', NZN'', NZN''')
                  fi)
              else (if NZN < NZN' + NZN'' 
                    then window(NZN' ++ NZN, NZN'', NZN''' + 1)
                    else window(NZN, NZN'', 1) 
                    fi)
              fi)
        fi .

*** Is the following function correct?
  eq windowLPE(W) =  if size(W) == 0 then noRat 
                     else sd(size(W), noOfTrues(W)) / size(W) fi .
endfm)