fmod TIME is 
   sorts Time NzTime .
   subsort NzTime < Time .
   
   op zero : -> Time .
   op _plus_ : Time Time -> Time [assoc comm prec 33 gather (E e)] .
   op _monus_ : Time Time -> Time [prec 33 gather (E e)] .
   op _le_ : Time Time -> Bool [prec 37] .
   op _lt_ : Time Time -> Bool [prec 37] .
   op _ge_ : Time Time -> Bool [prec 37] .
   op _gt_ : Time Time -> Bool [prec 37] .

   eq zero plus R:Time = R:Time .
   eq R:Time le R':Time = (R:Time lt R':Time) or (R:Time == R':Time) .
   eq R:Time ge R':Time = R':Time le R:Time .
   eq R:Time gt R':Time = R':Time lt R:Time .
endfm


fmod TIMED-PRELUDE is
   including TIME .
   sorts System GlobalSystem ClockedSystem .
   subsort GlobalSystem < ClockedSystem .
   
   op {_} : System -> GlobalSystem [format (g o g so)] .
   op _in time_ : GlobalSystem Time -> ClockedSystem  [format (o g g y o)] .
   
   eq (CLS:ClockedSystem in time R:Time) in time R':Time =
          CLS:ClockedSystem in time (R:Time plus R':Time) .
endfm

fmod TIME-INF is 
  including TIME .
  sort TimeInf .
  subsort Time < TimeInf .

  op INF : -> TimeInf .
  op _plus_ : TimeInf TimeInf -> TimeInf [ditto] .
  op _monus_ : TimeInf Time -> TimeInf [ditto] .
  op _le_ : TimeInf TimeInf -> Bool [prec 37] .
  op _lt_ : TimeInf TimeInf -> Bool [prec 37] .
  op _ge_ : TimeInf TimeInf -> Bool [prec 37] .
  op _gt_ : TimeInf TimeInf -> Bool [prec 37] .
  
  var TI TI' : TimeInf .
  var R : Time .

  eq INF plus TI = INF .
  eq INF monus R = INF .
  eq TI le INF = true .
  eq INF le R = false .
  eq INF lt TI = false .
  eq R lt INF = true .
  eq TI gt TI' = TI' lt TI .
  eq TI ge TI' = TI' le TI .
endfm

*** Now for linear time ...

fmod LTIME is 
  including TIME .

  ops minimum maximum : Time Time -> Time [assoc comm] .

  vars R R' : Time .
  ceq maximum(R, R') = R if R' le R .
  ceq minimum(R, R') = R' if R' le R .
endfm



*** Linear time with infinity value:

fmod LTIME-INF is
  including LTIME .
  including TIME-INF .

  ops minimum maximum : TimeInf TimeInf -> TimeInf [ditto] .

  eq maximum(INF, TI:TimeInf) = INF .
  eq minimum(INF, TI:TimeInf) = TI:TimeInf .
endfm



*** Discrete time domain, the natural numbers ...

fmod NAT-TIME-DOMAIN is
  inc LTIME .
  protecting NAT .
 
  subsort Nat < Time .
  subsort NzNat < NzTime .

  vars N N' : Nat .

  eq zero = 0 .
  eq N plus N' = N + N' .
  eq N monus N' = if N > N' then sd(N, N') else 0 fi .
  eq N lt N' = N < N' .
endfm



fmod NAT-TIME-DOMAIN-WITH-INF is
  protecting NAT-TIME-DOMAIN .
  including LTIME-INF .

  --- should for simplicity extend <, >=, etc to infinity:

  op _<_ : TimeInf TimeInf -> Bool [ditto] .
  op _<=_ : TimeInf TimeInf -> Bool [ditto] .
  op _>_ : TimeInf TimeInf -> Bool [ditto] .
  op _>=_ : TimeInf TimeInf -> Bool [ditto] .

  op _+_ : TimeInf TimeInf -> TimeInf [ditto] .

  var N : Nat .  var TI : TimeInf .

  eq INF < TI = false .
  eq N < INF = true .
  eq TI <= INF = true .
  eq INF <= N = false .
  eq INF >= TI = true .
  eq N >= INF = false .
  eq TI > INF = false .
  eq INF > N = true .

  eq INF + TI = INF .

  --- NEW: must also extend the built-in 'min' and'max' to TimeInf:
  ops min max : TimeInf TimeInf -> TimeInf [ditto] .
  eq max(INF, TI:TimeInf) = INF .
  eq min(INF, TI:TimeInf) = TI:TimeInf .
  endfm


--- changed!
*** --------------------------
fmod POSITIVE-RAT is
  protecting RAT .

  sort NNegRat .                 --- non-negative rationals!
  subsorts Zero PosRat Nat < NNegRat < Rat .
endfm



fmod POSRAT-TIME-DOMAIN is
  inc LTIME .
  protecting POSITIVE-RAT .

  subsort NNegRat < Time .
  subsort PosRat < NzTime .

  vars R R' : NNegRat .

  eq zero = 0 .
  eq R plus R' = R + R' .
  eq R monus R' = if R > R' then R - R' else 0 fi .
  eq R lt R' = R < R' .
endfm



fmod POSRAT-TIME-DOMAIN-WITH-INF is
  protecting POSRAT-TIME-DOMAIN .
  including LTIME-INF .

  --- again, we should extend the comparison operators to infinity:
  op _<_ : TimeInf TimeInf -> Bool [ditto] .
  op _<=_ : TimeInf TimeInf -> Bool [ditto] .
  op _>_ : TimeInf TimeInf -> Bool [ditto] .
  op _>=_ : TimeInf TimeInf -> Bool [ditto] .

  op _+_ : TimeInf TimeInf -> TimeInf [ditto] .
  op _+_ : NNegRat NNegRat -> NNegRat [ditto] .

  var R : NNegRat .  var TI : TimeInf .

  eq INF < TI = false .
  eq R < INF = true .
  eq TI <= INF = true .
  eq INF <= R = false .
  eq INF >= TI = true .
  eq R >= INF = false .
  eq TI > INF = false .
  eq INF > R = true .

  eq INF + TI = INF .

  --- NEW: must also extend the built-in 'min' and'max' to TimeInf:
  ops min max : TimeInf TimeInf -> TimeInf [ditto] .
  eq max(INF, TI:TimeInf) = INF .
  eq min(INF, TI:TimeInf) = TI:TimeInf .

  --- Some additional declarations for preregularity:
  ops min max : NNegRat NNegRat -> NNegRat [ditto] .
  ops min max : Zero Zero -> Zero [ditto] .
  op min : Zero NzNat -> Zero [ditto] .
  op max : Zero NzNat -> NzNat [ditto] .
  op max : Rat TimeInf -> TimeInf [ditto] .
  op max : Rat NNegRat -> NNegRat [ditto] .
endfm

