-- 
-- Fischer's protocol: a real-time mutual exclusion protocol
--
--  a:  remainder section             try_i    [0,oo]
--      loop  
--  b:    repeat while turn = 0       test_i   [0,oo]
--  c:    turn := i                   set_i    [0,d1]
--  d:    if turn = i then goto cs    check_i  [d2,oo]
-- cs:  critical section              exit_i   [0,oo]
--  e:  turn := 0                     reset_i  [0,oo]
--

mod! TIMEVAL {
  [Zero NzReal+ < Real+]
  [NzReal+ Inf < NzTimeval]
  [Real+ NzTimeval < Timeval]
  op 0    : -> Zero
  op oo   : -> Inf
  op _<_  : Timeval Timeval -> Bool
  op _<=_ : Timeval Timeval -> Bool
  op _+_  : Timeval Timeval -> Timeval {assoc comm}
  vars X Y Z W : Real+
  var T : Timeval
  eq X < oo  = true .
  eq oo < X  = false .
  eq X <= oo = true .
  eq oo <= X = false .
  eq 0 <= X  = true .
--
  -- used in proof3.mod
  ceq X + Z < X + Y = true if Z < Y .
  ceq T < X + Y = true if T < X .
  -- used in proof4.mod
  ceq T < X = false if X <= T .
  -- used in proof5.mod
  eq X <= X + Y = true .
}

mod* PID {
  [NoPid Pid < Pid+]
  op nop : -> NoPid
  op _=_ : Pid+ Pid+ -> Bool {comm}
  var P : Pid 
  eq (P = P) = true .
  eq (nop = nop) = true .
  eq (P = nop) = false .
}

mod! LOC {
  [ Loc ]
  ops a b c d cs e : -> Loc
  op _=_ : Loc Loc -> Bool {comm}
  var L : Loc
  eq (L = L)  = true .
  eq (a = b)  = false .
  eq (a = c)  = false .
  eq (a = d)  = false .
  eq (a = cs) = false .
  eq (a = e)  = false .
  eq (b = c)  = false .
  eq (b = d)  = false .
  eq (b = cs) = false .
  eq (b = e)  = false .
  eq (c = d)  = false .
  eq (c = cs) = false .
  eq (c = e)  = false .
  eq (d = cs) = false .
  eq (d = e)  = false .
  eq (cs = e) = false .
}

mod* FISCHER {
  pr( PID + LOC + TIMEVAL )
  *[ Sys ]*
-- initial state
   op init : -> Sys
-- observation operators
  bop turn : Sys -> Pid+
  bop loc  : Sys Pid -> Loc  
  bop now  : Sys -> Real+
  bop l    : Sys Pid -> Real+
  bop u    : Sys Pid -> NzTimeval
-- action operators
  bop try   : Sys Pid -> Sys
  bop test  : Sys Pid -> Sys
  bop set   : Sys Pid -> Sys
  bop check : Sys Pid -> Sys
  bop exit  : Sys Pid -> Sys
  bop reset : Sys Pid -> Sys
  bop tick  : Sys Real+ -> Sys
-- delays
  op d1 : -> NzTimeval
  op d2 : -> Real+
  eq d1 < d2 = true .
  eq 0 < d1 = true .
  eq 0 < d2 = true .
-- CafeOBJ variables
  var S : Sys
  vars I J : Pid
  var D : Real+
-- any initial state
  eq turn(init)  = nop .
  eq loc(init,I) = a .
  eq now(init)   = 0 .
  eq l(init,I)   = 0 .
  eq u(init,I)   = oo .
-- 1 try(S,I)
  op c-try : Sys Pid -> Bool {strat: (0 1 2)}
  eq c-try(S,I) = (loc(S,I) = a) .
  --
  eq  turn(try(S,I))  = turn(S) .
  ceq loc(try(S,I),J) 
      = (if I = J then b else loc(S,J) fi) if c-try(S,I) .
  eq  now(try(S,I))   = now(S) .
  eq  l(try(S,I),J)   = l(S,J) .
  eq  u(try(S,I),J)   = u(S,J) .
  ceq try(S,I)        = S                  if not c-try(S,I) .
-- 2 test(S,I)
  op c-test : Sys Pid -> Bool {strat: (0 1 2)}
  eq c-test(S,I) = (loc(S,I) = b and turn(S) = nop) .
  --
  eq  turn(test(S,I))  = turn(S) .
  ceq loc(test(S,I),J) 
      = (if I = J then c else loc(S,J) fi)         if c-test(S,I) .
  eq  now(test(S,I))    = now(S) .
  eq  l(test(S,I),J)    = l(S,J) .
  ceq u(test(S,I),J)    
      = (if I = J then now(S) + d1 else u(S,J) fi) if c-test(S,I) .
  ceq test(S,I)         = S                        if not c-test(S,I) .
-- 3 set(S,I)
  op c-set : Sys Pid -> Bool {strat: (0 1 2)}
  eq c-set(S,I) = (loc(S,I) = c) .
  --
  ceq turn(set(S,I))  = I                          if c-set(S,I) .
  ceq loc(set(S,I),J) 
      = (if I = J then d else loc(S,J) fi)         if c-set(S,I) .
  eq  now(set(S,I))   = now(S) .
  ceq l(set(S,I),J)   
      = (if I = J then now(S) + d2 else l(S,J) fi) if c-set(S,I) .
  ceq u(set(S,I),J)   
      = (if I = J then oo else u(S,J) fi)          if c-set(S,I) .
  ceq set(S,I)        = S                          if not c-set(S,I) .
-- 4 check(S,I)
  op c-check : Sys Pid -> Bool {strat: (0 1 2)}
  eq c-check(S,I) = (loc(S,I) = d and l(S,I) <= now(S)) .
  --
  eq  turn(check(S,I))  = turn(S) .
  ceq loc(check(S,I),J) 
      = (if I = J then (if turn(S) = I then cs else b fi) else loc(S,J) fi)
      if c-check(S,I) .
  eq  now(check(S,I))   = now(S) .
  ceq l(check(S,I),J)   
      = (if I = J then 0 else l(S,J) fi) if c-check(S,I) .
  eq  u(check(S,I),J)   = u(S,J) .
  ceq check(S,I)        = S              if not c-check(S,I) .
-- 5 exit(S,I)
  op c-exit : Sys Pid -> Bool {strat: (0 1 2)}
  eq c-exit(S,I) = (loc(S,I) = cs) .
  --
  eq  turn(exit(S,I))  = turn(S) .
  ceq loc(exit(S,I),J) 
      = (if I = J then e else loc(S,J) fi) if c-exit(S,I) .
  eq  now(exit(S,I))   = now(S) .
  eq  l(exit(S,I),J)   = l(S,J) .
  eq  u(exit(S,I),J)   = u(S,J) .
  ceq exit(S,I)        = S                 if not c-exit(S,I) .
-- 6 reset(S,I)
  op c-reset : Sys Pid -> Bool {strat: (0 1 2)}
  eq c-reset(S,I) = (loc(S,I) = e) .
  --
  ceq turn(reset(S,I))  = nop              if c-reset(S,I) .
  ceq loc(reset(S,I),J) 
      = (if I = J then a else loc(S,J) fi) if c-reset(S,I) .
  eq  now(reset(S,I))   = now(S) .
  eq  l(reset(S,I),J)   = l(S,J) .
  eq  u(reset(S,I),J)   = u(S,J) .
  ceq reset(S,I)        = S                if not c-reset(S,I) .
-- 7 tick(S,D)
  op c-tick : Sys Real+ -> Bool {strat: (0 1 2)}
  eq c-tick(S,D) = (now(S) + D <= u(S,I)) .
  --
  eq  turn(tick(S,D))  = turn(S) .
  eq  loc(tick(S,D),I) = loc(S,I) .
  ceq [tick1] : now(tick(S,D)) = now(S) + D if c-tick(S,D) .
  eq  l(tick(S,D),I)   = l(S,I) .
  eq  u(tick(S,D),I)   = u(S,I) .
  ceq tick(S,D)        = S if not c-tick(S,D) .
}