MACHINE
  Car_M1
REFINES
  ControlledSystem
SEES
  Car_C1
VARIABLES
  t
  x_s
  v
  x
INVARIANTS
  inv1: v : RRealPlus --> RReal
  inv2: x : RRealPlus --> RReal
  inv3: x_p = bind(v,x)
  inv4: ! t0 . t0 : RRealPlus => Rzero |-> v(t0) : leq
  inv5: ! t0 . t0 : RRealPlus & x_s = stopped => x(t0) |-> SP : leq
EVENTS
  INITIALISATION
  WITH
    x_p': x_p' = bind(v',x')
  THEN
    act1: t := Rzero
    act2: 
      v,x :|
        x' : RRealPlus --> RReal & v' : RRealPlus --> RReal &
        solutionOf(RRealPlus,bind(v',x'), ode(f_stable,(v0 |-> Rzero),Rzero))
    act3: x_s := stabilizing
  END

  Progress
  REFINES Progress
  THEN
    act1: t :| t' : RRealPlus & (t |-> t' : lt)
  END

  Behave
  REFINES Behave
  ANY
    e
  WHERE
    grd1: e : DE(S)
    grd2: Solvable(Closed2Infinity(t),e)
  WITH
    x_p': x_p' = bind(v',x')
  THEN
    act1: 
      v,x :|
        x' : RRealPlus --> RReal & v' : RRealPlus --> RReal &
        AppendSolutionBAP(
          e,
          RRealPlus,
          Closed2Open(Rzero,t), Closed2Infinity(t),
          bind(v,x), bind(v',x')
        )
  END

  Transition
  REFINES Transition
  ANY
    s
  WHERE
    grd1: s : POW1(STATES)
  THEN
    act1: x_s :: s
  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_sense_user_input_accelerate
  REFINES Sense
  WHERE
    grd1: plus(x(t) |-> divide(times(v(t) |-> v(t)) |-> times(Rtwo |-> b))) |-> SP : lt
  WITH
    s: s = {accelerating}
    p: p = STATES*RReal*{ v_ |-> x_ |  plus(x_ |-> divide(times(v_ |-> v_) |-> times(Rtwo |-> b))) |-> SP : lt }
  THEN
    act1: x_s := accelerating
  END

  ctrl_sense_user_input_stabilize
  REFINES Sense
  WHERE
    grd1: plus(x(t) |-> divide(times(v(t) |-> v(t)) |-> times(Rtwo |-> b))) |-> SP : lt
  WITH
    s: s = {stabilizing}
    p: p = STATES*RReal*{ v_ |-> x_ |  plus(x_ |-> divide(times(v_ |-> v_) |-> times(Rtwo |-> b))) |-> SP : lt }
  THEN
    act1: x_s := stabilizing
  END

  ctrl_sense_user_input_brake
  REFINES Sense
  WHERE
    grd1: v(t) |-> Rzero : gt
  WITH
    s: s = {braking}
    p: p = STATES*RReal*{ v_ |-> x_ |  v_ |-> Rzero : gt & x_ : RReal }
  THEN
    act1: x_s := braking
  END

  ctrl_actuate_brake
  REFINES Actuate
  WHERE
    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')
  THEN
    act1: 
      v,x :|
        x' : RRealPlus --> RReal & v' : RRealPlus --> RReal &
        AppendSolutionBAP(
          ode(f_deceleration(t |-> v(t)),(v(t) |-> x(t)),t),
          RRealPlus,
          Closed2Open(Rzero,t), Closed2Infinity(t),
          bind(v,x), bind(v',x')
        )
  END

  ctrl_actuate_accelerate
  REFINES Actuate
  WHERE
    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')
  THEN
    act1: 
      v,x :|
        x' : RRealPlus --> RReal & v' : RRealPlus --> RReal &
        AppendSolutionBAP(
          ode(f_acceleration,(v(t) |-> x(t)),t),
          RRealPlus,
          Closed2Open(Rzero,t), Closed2Infinity(t),
          bind(v,x), bind(v',x')
        )
  END

  ctrl_actuate_stabilize
  REFINES Actuate
  WHERE
    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')
  THEN
    act1: 
      v,x :|
        x' : RRealPlus --> RReal & v' : RRealPlus --> RReal &
        AppendSolutionBAP(
          ode(f_stable,(v(t) |-> x(t)),t),
          RRealPlus,
          Closed2Open(Rzero,t), Closed2Infinity(t),
          bind(v,x), bind(v',x')
        )
  END

END