--
-- Asynchronous data sending problem: A sender repeatedly sends natural
-- numbers one by one from zero to a receiver via a cell. 
--
-- Sender::
--   loop send x [d1,oo]
--
-- Cell::
--   initially empty = true
--   loop send x --> empty := false
--                   content := x
--     || rec x  --> empty := true
--
-- Receiver::
--   loop rec x if cell is non-empty [0,d2]
--

mod! TIMEVAL {
  [Zero NzReal+ < Real+]
  [NzReal+ Inf < Timeval+]
  [Real+ Timeval+ < Timeval]
  op 0 : -> Zero
  op oo : -> Inf
  op _<_ : Timeval Timeval -> Bool
  op _<=_ : Timeval Timeval -> Bool
--  op _+_ : Real+ Real+ -> Real+
  op _+_ : Timeval Timeval -> Timeval
  vars X Y Z : Real+
  eq X < 0 = false .
  eq X < oo = true .
  eq oo < X = false .
  eq X < X = false .
  eq 0 <= X = true .
  eq oo <= X = false .
  eq X <= oo = true .
  eq X <= X = true .
--
  -- used in proof2.mod
  ceq X + Y <= X = false if 0 < Y .
  ceq X <= Y = true if Y < X .
}

mod! PEANONAT {
  [ Nat ]
  op 0 : -> Nat
  op s : Nat -> Nat
  op inc : Nat -> Nat
  op dec : Nat -> Nat
  op _<_ : Nat Nat -> Bool  
  op _<=_ : Nat Nat -> Bool  
  op _=_ : Nat Nat -> Bool {comm}
  vars X Y : Nat
  eq inc(X) = s(X) .
  eq dec(s(X)) = X .
  eq s(dec(X)) = X .
  eq dec(X) < Y = X < s(Y) .
  eq X < dec(Y) = s(X) < Y .
  eq 0 < s(X) = true .
  eq s(X) < 0 = false .
  eq X < X = false .
  eq s(X) < s(Y) = X < Y .
  eq dec(X) <= Y = X <= s(Y) .
  eq X <= dec(Y) = s(X) <= Y .
  eq 0 <= s(X) = true .
  eq s(X) <= 0 = false .
  eq X <= X = true .
  eq s(X) <= s(Y) = X <= Y .
  eq (X = X) = true .
}

mod! LIST {
  pr( PEANONAT )
  [ List ]
  op nil : -> List
  op __ : Nat List -> List
  op put : List Nat -> List
  op _.._ : Nat Nat -> List
  op _=_ : List List -> Bool {comm}
  vars X Y Z : Nat
  vars L L1 : List
  eq put(nil,Y) = Y nil .
  eq put(X L,Y) = X put(L,Y) .
  eq put(X .. X,s(X)) = X .. s(X) .
  ceq put(X .. Y,s(Y)) = X .. s(Y) if X < Y .
  ceq put(X .. Y,Z) = Z .. Z if Y < X .
  eq X .. X = X nil .
  ceq X .. Y = nil if Y < X .
  ceq X .. Y = X (inc(X) .. Y) if X < Y .
  eq (L = L) = true .
  eq (X L = nil) = false .
}

mod* ASEND {
  pr(PEANONAT + LIST + TIMEVAL)
  *[Sys]*
-- initial state
  op  init    :           -> Sys
-- observation operators
  bop empty   : Sys       -> Bool
  bop content : Sys       -> Nat
  bop data    : Sys       -> Nat
  bop list    : Sys       -> List
  bop now     : Sys       -> Real+
  bop l       : Sys       -> Real+
  bop u       : Sys       -> Timeval+
-- action operators
  bop send    : Sys       -> Sys
  bop rec     : Sys       -> Sys  
  bop tick    : Sys Real+ -> Sys
-- delays
  op d1 : -> Real+
  op d2 : -> Timeval+
  eq d2 < d1 = true .
  eq 0 < d1 = true .
-- CafeOBJ variables
  var S : Sys
  var D : Real+
-- in any initial state
  eq empty(init) = true .
  eq data(init)  = 0 .
  eq list(init)  = nil .
  eq now(init)   = 0 .
  eq l(init)     = d1 .
  eq u(init)     = oo .
-- send(S)
  ceq empty(send(S))   = false        if l(S) <= now(S) .
  ceq content(send(S)) = data(S)      if l(S) <= now(S) .
  ceq data(send(S))    = inc(data(S)) if l(S) <= now(S) .
  eq  list(send(S))    = list(S) .
  eq  now(send(S))     = now(S) .
  ceq l(send(S))       = now(S) + d1  if l(S) <= now(S) .
  ceq u(send(S))       = now(S) + d2  if l(S) <= now(S) .
  ceq send(S)          = S            if not(l(S) <= now(S)) .
-- rec(S)
  ceq empty(rec(S))   = true                    if not empty(S) .
  eq  content(rec(S)) = content(S) .
  eq  data(rec(S))    = data(S) .
  ceq list(rec(S))    = put(list(S),content(S)) if not empty(S) .
  eq  now(rec(S))     = now(S) .
  eq  l(rec(S))       = l(S) .
  ceq u(rec(S))       = oo                      if not empty(S) .
  ceq rec(S)          = S                       if empty(S) .
-- tick(S,D)
  eq  empty(tick(S,D))   = empty(S) .
  eq  content(tick(S,D)) = content(S) .
  eq  data(tick(S,D))    = data(S) .
  eq  list(tick(S,D))    = list(S) .
  ceq now(tick(S,D))     = now(S) + D if now(S) + D <= u(S) .
  eq  l(tick(S,D))       = l(S) .
  eq  u(tick(S,D))       = u(S) .
  ceq tick(S,D)          = S          if not(now(S) + D <= u(S)) .
}