MACHINE
  Autobrake
REFINES
  Generic
SEES
  AutobrakeCtx
VARIABLES
  t
  x_s
  v
  x
INVARIANTS
  inv1: v : RReal +-> RReal
  inv2: Closed2Closed(Rzero,t) <: dom(v)
  inv3: x : RReal +-> RReal
  inv4: Closed2Closed(Rzero,t) <: dom(x)
  inv5: x_p = bind(v,x)
  inv6: boundedBy(Closed2Closed(Rzero,t), v, Rzero, Vmax)
  inv7: ! t_ . t_ : Closed2Closed(Rzero,t) & x(t_) |-> SP : geq => x_s = stopped
EVENTS
  INITIALISATION
  WITH
    x_p': x_p' = bind(v',x')
  THEN
    act1: t := Rzero
    act2: v,x :| v' = { Rzero |-> v0 } & x' = { Rzero |-> x0 }
    act4: x_s := stabilizing
  END

  Behave
  REFINES Behave
  ANY
    tp
    e
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: e : DE(S)
    grd2: Solvable(Closed2Closed(t,tp),e)
  WITH
    x_p': x_p' = bind(v',x')
    Inv: Inv = S
  THEN
    act1: 
      t,x,v :| 
        t' = tp &
        x' : RRealPlus --> RReal & v' : RRealPlus --> RReal &
        CBAPsolutionOf(t,t',bind(v,x),bind(v',x'),e,S)
  END

  ctrl_transition_accelerate
  REFINES Transition
  WHERE
    grd1: plus(x(t) |-> divide(times(v(t) |-> v(t)) |-> times(Rtwo |-> b))) |-> SP : lt
  WITH
    s: s = { accelerating }
  THEN
    act1: x_s := accelerating
  END

  ctrl_transition_stabilize
  REFINES Transition
  WHERE
    grd1: plus(x(t) |-> divide(times(v(t) |-> v(t)) |-> times(Rtwo |-> b))) |-> SP : lt
  WITH
    s: s = { stabilizing }
  THEN
    act1: x_s := stabilizing
  END

  ctrl_transition_brake
  REFINES Transition
  WHERE
    grd1: plus(x(t) |-> divide(times(v(t) |-> v(t)) |-> times(Rtwo |-> b))) |-> SP : lt
  WITH
    s: s = { braking }
  THEN
    act1: x_s := braking
  END

  ctrl_sense_near_stop
  REFINES Sense
  WHERE
    grd1: plus(x(t) |-> divide(times(v(t) |-> v(t)) |-> times(Rtwo |-> b))) |-> SP : geq
    grd2: v(t) |-> Rzero : gt
  WITH
    s: s = {nearing_stop}
    p: p = STATES*RReal*{ v_ |-> x_ | plus(x_ |-> divide(times(v_ |-> v_) |-> times(Rtwo |-> b))) |-> SP : geq & v_ |-> Rzero : gt }
  THEN
    act1: x_s := nearing_stop
  END

  ctrl_sense_stopping
  REFINES Sense
  WHERE
    grd1: v(t) = Rzero
  WITH
    s: s = {stabilizing, stopped}
    p: p = STATES*RReal*{ v_ |-> x_ |  v_ = Rzero & x_ : RReal }
  THEN
    act1: 
      x_s :|
        (x_s = nearing_stop => x_s' = stopped) &
        (x_s /= nearing_stop => x_s' = stabilizing)
  END

  ctrl_actuate_brake
  REFINES Actuate
  ANY
    tp
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s : { braking, nearing_stop }
  WITH
    e: e = ode(f_deceleration(t|->v(t)),v(t)|->x(t),t)
    s: s = { braking, nearing_stop }
    x_p': x_p' = bind(v',x')
    Inv: Inv = { (v_|->x_) | x_ : RReal & Rzero |-> v_ : leq }
  THEN
    act1: 
      t,v,x :|
        t' = tp &
        v' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(v') &
        x' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(x') &
        CBAPsolutionOf(
          t,t',bind(v,x),bind(v',x'),
          ode(f_deceleration(t|->v(t)),v(t)|->x(t),t),
          { (v_|->x_) | x_ : RReal & Rzero |-> v_ : leq }
        )
  END

  ctrl_actuate_stabilize
  REFINES Actuate
  ANY
    tp
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s : { stabilizing, stopped }
  WITH
    e: e = ode(f_stable,v(t)|->x(t),t)
    s: s = { stabilizing, stopped }
    x_p': x_p' = bind(v',x')
    Inv: 
      Inv = { (v_|->x_) | v_ : RReal & x_ : RReal & 
                           plus(x_ |-> divide(times(v_ |-> v_) |-> times(Rtwo |-> b))) |-> SP : lt }
  THEN
    act1: 
      t,v,x :|
        t' = tp &
        v' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(v') &
        x' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(x') &
        CBAPsolutionOf(
          t,t',bind(v,x),bind(v',x'),
          ode(f_stable,v(t)|->x(t),t),
          { (v_|->x_) | v_ : RReal & x_ : RReal & 
                             plus(x_ |-> divide(times(v_ |-> v_) |-> times(Rtwo |-> b))) |-> SP : lt }
        )
  END

  ctrl_actuate_accelerate
  REFINES Actuate
  ANY
    tp
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s = accelerating
  WITH
    e: e = ode(f_acceleration,v(t)|->x(t),t)
    s: s = { accelerating }
    x_p': x_p' = bind(v',x')
    Inv: 
      Inv = { (v_|->x_) | v_ : RReal & x_ : RReal & 
                           plus(x_ |-> divide(times(v_ |-> v_) |-> times(Rtwo |-> b))) |-> SP : lt &
                 v_ |-> Vmax : leq }
  THEN
    act1: 
      t,v,x :|
        t' = tp &
        v' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(v') &
        x' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(x') &
        CBAPsolutionOf(
          t,t',bind(v,x),bind(v',x'),
          ode(f_acceleration,v(t)|->x(t),t),
          { (v_|->x_) |v_ : RReal & x_ : RReal & 
                             plus(x_ |-> divide(times(v_ |-> v_) |-> times(Rtwo |-> b))) |-> SP : lt &
                             v_ |-> Vmax : leq }
        )
  END

END