-- -- An automatic controller that opens and closes a gate at a railroad crossing. -- -- Train:: -- sect0: approach [0,oo] -- sect1: in [d1,oo] -- crossing: out [0,oo] -- sect2: exit [0,oo] -- sect3: -- -- Gate:: -- up: lower [d2,d2] (for synchronization) -- lowering: down [0,d3] -- down: raise [0,oo] (for synchronization) -- raising: up [0,oo] -- -- Controller:: -- state0: approach [0,oo] (for synchronization) -- state1: lower [d2,d2] -- state2: exit [0,oo] (for synchronization) -- state3: raise [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 -> Real+ {assoc comm} -- op _+_ : Real+ Real+ -> Real+ {assoc comm} op _=_ : Timeval Timeval -> Bool {comm} vars X Y Z W : Real+ vars T T1 T2 : Timeval eq X < oo = true . eq oo < X = false . eq X <= oo = true . eq oo <= X = false . eq 0 <= X = true . eq 0 + T = T . eq (T = T) = true . ceq (X = Y) = false if X < Y . ceq (X + Z = Y + Z) = true if X = Y . -- -- used in proof4.mod ceq X + Z < Y + W = true if X <= Y and Z < W . -- used in proof5.mod eq X <= X + Y = true . -- used in proof6.mod ceq X + Z < T + W = true if X <= T and Z < W . ceq (X = Y) = true if Y <= X and X <= Y . -- used in proof9.mod ceq X <= Y = false if Y < X . } mod! TRAINSTATE { [ TState ] ops sect0 sect1 crossing sect2 sect3 : -> TState op _=_ : TState TState -> Bool {comm} var S : TState eq (S = S) = true . eq (sect0 = sect1) = false . eq (sect0 = crossing) = false . eq (sect0 = sect2) = false . eq (sect0 = sect3) = false . eq (sect1 = crossing) = false . eq (sect1 = sect2) = false . eq (sect1 = sect3) = false . eq (crossing = sect2) = false . eq (crossing = sect3) = false . eq (sect2 = sect3) = false . } mod! GATESTATE { [ GState ] ops up lowering down raising : -> GState op _=_ : GState GState -> Bool {comm} var S : GState eq (S = S) = true . eq (up = lowering) = false . eq (up = down) = false . eq (up = raising) = false . eq (lowering = down) = false . eq (lowering = raising) = false . eq (down = raising) = false . } mod! CONTROLLERSTATE { [ CState ] ops state0 state1 state2 state3 : -> CState op _=_ : CState CState -> Bool {comm} var S : CState eq (S = S) = true . eq (state0 = state1) = false . eq (state0 = state2) = false . eq (state0 = state3) = false . eq (state1 = state2) = false . eq (state1 = state3) = false . eq (state2 = state3) = false . } mod* CROSSING { pr( TIMEVAL + TRAINSTATE + GATESTATE + CONTROLLERSTATE ) *[ Sys ]* -- initial state op init : -> Sys -- observation operators bop t : Sys -> TState bop g : Sys -> GState bop c : Sys -> CState bop now : Sys -> Real+ bop tl : Sys -> Real+ bop gu : Sys -> NzTimeval bop cl : Sys -> Real+ bop cu : Sys -> NzTimeval -- action operators bop approach : Sys -> Sys bop in : Sys -> Sys bop out : Sys -> Sys bop exit : Sys -> Sys bop down : Sys -> Sys bop up : Sys -> Sys bop lower : Sys -> Sys bop raise : Sys -> Sys bop tick : Sys Real+ -> Sys -- delays ops d1 d2 d3 : -> Real+ eq d2 + d3 < d1 = true . eq d2 < d1 = true . eq d3 < d1 = true . eq 0 < d1 = true . -- CafeOBJ variables var S : Sys var D : Real+ -- any initial condition eq t(init) = sect0 . eq g(init) = up . eq c(init) = state0 . eq now(init) = 0 . eq tl(init) = 0 . eq gu(init) = oo . eq cl(init) = 0 . eq cu(init) = oo . -- approach op c-approach : Sys -> Bool {strat: (0 1)} eq c-approach(S) = (t(S) = sect0 and c(S) = state0) . -- ceq t(approach(S)) = sect1 if c-approach(S) . eq g(approach(S)) = g(S) . ceq c(approach(S)) = state1 if c-approach(S) . eq now(approach(S)) = now(S) . ceq tl(approach(S)) = now(S) + d1 if c-approach(S) . eq gu(approach(S)) = gu(S) . ceq cl(approach(S)) = now(S) + d2 if c-approach(S) . ceq cu(approach(S)) = now(S) + d2 if c-approach(S) . ceq approach(S) = S if not c-approach(S) . -- in op c-in : Sys -> Bool {strat: (0 1)} eq c-in(S) = (t(S) = sect1 and tl(S) <= now(S)) . -- ceq t(in(S)) = crossing if c-in(S) . eq g(in(S)) = g(S) . eq c(in(S)) = c(S) . eq now(in(S)) = now(S) . ceq tl(in(S)) = 0 if c-in(S) . eq gu(in(S)) = gu(S) . eq cl(in(S)) = cl(S) . eq cu(in(S)) = cu(S) . ceq in(S) = S if not c-in(S) . -- out op c-out : Sys -> Bool {strat: (0 1)} eq c-out(S) = (t(S) = crossing) . -- ceq t(out(S)) = sect2 if c-out(S) . eq g(out(S)) = g(S) . eq c(out(S)) = c(S) . eq now(out(S)) = now(S) . eq tl(out(S)) = tl(S) . eq gu(out(S)) = gu(S) . eq cl(out(S)) = cl(S) . eq cu(out(S)) = cu(S) . ceq out(S) = S if not c-out(S) . -- exit op c-exit : Sys -> Bool {strat: (0 1)} eq c-exit(S) = (t(S) = sect2 and c(S) = state2) . -- ceq t(exit(S)) = sect3 if c-exit(S) . eq g(exit(S)) = g(S) . ceq c(exit(S)) = state3 if c-exit(S) . eq now(exit(S)) = now(S) . eq tl(exit(S)) = tl(S) . eq gu(exit(S)) = gu(S) . eq cl(exit(S)) = cl(S) . eq cu(exit(S)) = cu(S) . ceq exit(S) = S if not c-exit(S) . -- down op c-down : Sys -> Bool {strat: (0 1)} eq c-down(S) = (g(S) = lowering) . -- eq t(down(S)) = t(S) . ceq g(down(S)) = down if c-down(S) . eq c(down(S)) = c(S) . eq now(down(S)) = now(S) . eq tl(down(S)) = tl(S) . ceq gu(down(S)) = oo if c-down(S) . eq cl(down(S)) = cl(S) . eq cu(down(S)) = cu(S) . ceq down(S) = S if not c-down(S) . -- up op c-up : Sys -> Bool {strat: (0 1)} eq c-up(S) = (g(S) = raising) . -- eq t(up(S)) = t(S) . ceq g(up(S)) = up if c-up(S) . eq c(up(S)) = c(S) . eq now(up(S)) = now(S) . eq tl(up(S)) = tl(S) . eq gu(up(S)) = gu(S) . eq cl(up(S)) = cl(S) . eq cu(up(S)) = cu(S) . ceq up(S) = S if not c-up(S) . -- lower op c-lower : Sys -> Bool {strat: (0 1)} eq c-lower(S) = (g(S) = up and c(S) = state1 and cl(S) <= now(S)) . -- eq t(lower(S)) = t(S) . ceq g(lower(S)) = lowering if c-lower(S) . ceq c(lower(S)) = state2 if c-lower(S) . eq now(lower(S)) = now(S) . eq tl(lower(S)) = tl(S) . ceq gu(lower(S)) = now(S) + d3 if c-lower(S) . ceq cl(lower(S)) = 0 if c-lower(S) . ceq cu(lower(S)) = oo if c-lower(S) . ceq lower(S) = S if not c-lower(S) . -- raise op c-raise : Sys -> Bool {strat: (0 1)} eq c-raise(S) = (g(S) = down and c(S) = state3) . -- eq t(raise(S)) = t(S) . ceq g(raise(S)) = raising if c-raise(S) . ceq c(raise(S)) = state0 if c-raise(S) . eq now(raise(S)) = now(S) . eq tl(raise(S)) = tl(S) . eq gu(raise(S)) = gu(S) . eq cl(raise(S)) = cl(S) . eq cu(raise(S)) = cu(S) . ceq raise(S) = S if not c-raise(S) . -- tick op c-tick : Sys Real+ -> Bool {strat: (0 1 2)} eq c-tick(S,D) = (now(S) + D <= gu(S) and now(S) + D <= cu(S)) . -- eq t(tick(S,D)) = t(S) . eq g(tick(S,D)) = g(S) . eq c(tick(S,D)) = c(S) . ceq now(tick(S,D)) = now(S) + D if c-tick(S,D) . eq tl(tick(S,D)) = tl(S) . eq gu(tick(S,D)) = gu(S) . eq cl(tick(S,D)) = cl(S) . eq cu(tick(S,D)) = cu(S) . ceq tick(S,D) = S if not c-tick(S,D) . }