MACHINE
  LeftTurnAssist
REFINES
  Generic
SEES
  LeftTurnAssistCtx
VARIABLES
  t
  x_s
  ppov
  psv
  vsv
  vpov
  asv
INVARIANTS
  inv1: ppov : RReal +-> RReal
  inv2: Closed2Closed(Rzero,t) <: dom(ppov)
  inv5: vsv : RReal +-> RReal
  inv3: psv : RReal +-> RReal
  inv4: Closed2Closed(Rzero,t) <: dom(psv)
  inv6: Closed2Closed(Rzero,t) <: dom(vsv)
  inv7: vpov : Closed2Closed(uminus(Vmax),Rzero)
  inv8: asv : Closed2Closed(uminus(B),Amax)
  inv9: x_p = bind(bind(vsv,psv),ppov)
  inv10: ! t_ . t_ : Closed2Closed(Rzero,t) & ppov(t_) |-> k : lt => (psv(t_) |-> Rzero : leq or psv(t_) |-> q : geq)
EVENTS
  INITIALISATION
  WITH
    x_p': x_p' = bind(bind(vsv',psv'),ppov')
  THEN
    act1: t := Rzero
    act2: vsv,psv,ppov := { Rzero |-> Rzero }, { Rzero |-> Rzero }, { Rzero |-> ppov_init }
    act3: x_s := waiting
    act4: vpov := vpov_init
    act5: asv := Rzero
  END

  Behave
  REFINES Behave
  ANY
    e
    tp
    v
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: e : DE(S)
    grd2: Solvable(Closed2Closed(t,tp),e)
    grd3: v : Closed2Closed(Rzero,Vmax)
  WITH
    x_p': x_p' = bind(bind(vsv',psv'),ppov')
    Inv: Inv = S
  THEN
    act1: 
      t,vsv,psv,ppov :| 
        t' = tp &
        vsv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(vsv') &
        psv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(psv') &
        ppov' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(ppov') &
        CBAPsolutionOf(t,t',bind(bind(vsv,psv),ppov),bind(bind(vsv',psv'),ppov'),e,S)
    act2: vpov := uminus(v)
  END

  ctrl_transition_attempt_turn
  REFINES Transition
  WHERE
    grd1: x_s = waiting
    grd2: Tsv(Amin |-> vsv(t) |-> psv(t)) |-> Tpov(ppov(t)) : lt
  WITH
    s: s = {turning}
  THEN
    act1: x_s := turning
  END

  ctrl_sense_turn_end
  REFINES Sense
  WHERE
    grd1: psv(t) |-> q : geq
  WITH
    s: s = {passed}
    p: p = STATES*RReal*{ vsv_ |-> psv_ |-> ppov_ | vsv_ : RReal & psv_ |-> q : geq & ppov_ : RReal }
  THEN
    act1: x_s := passed
  END

  ctrl_actuate_waiting
  REFINES Actuate
  ANY
    tp
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s = waiting
  WITH
    e: e = ode(f_stable(vpov),(vsv(t) |-> psv(t) |-> ppov(t)),t)
    s: s = {waiting}
    x_p': x_p' = bind(bind(vsv',psv'),ppov')
    Inv: Inv = S
  THEN
    act1: 
      t,vsv,psv,ppov :| 
        t' = tp &
        vsv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(vsv') &
        psv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(psv') &
        ppov' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(ppov') &
        CBAPsolutionOf(t,t',bind(bind(vsv,psv),ppov),bind(bind(vsv',psv'),ppov'),
          ode(f_stable(vpov),(vsv(t) |-> psv(t) |-> ppov(t)),t),
        S)
  END

  ctrl_actuate_turning
  REFINES Actuate
  ANY
    tp
    a
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s = turning
    grd2: a : Closed2Closed(Amin,Amax)
  WITH
    e: e = ode(f_accelerate_min(a |-> vpov |-> vsv(t)),(vsv(t) |-> psv(t) |-> ppov(t)),t)
    s: s = {turning}
    x_p': x_p' = bind(bind(vsv',psv'),ppov')
    Inv: Inv = { vsv_|->psv_|->ppov_ | vsv_ : RReal & psv_ |-> q : leq & ppov_ : RReal }
  THEN
    act1: 
      t,vsv,psv,ppov :| 
        t' = tp &
        vsv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(vsv') &
        psv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(psv') &
        ppov' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(ppov') &
        CBAPsolutionOf(t,t',bind(bind(vsv,psv),ppov),bind(bind(vsv',psv'),ppov'),
          ode(f_accelerate_min(a |-> vpov |-> vsv(t)),(vsv(t) |-> psv(t) |-> ppov(t)),t),
          { vsv_|->psv_|->ppov_ | vsv_ : RReal & psv_ |-> q : leq & ppov_ : RReal }
        )
    act2: asv := a
  END

  ctrl_actuate_passed_stable
  REFINES Actuate
  ANY
    tp
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s = turning
  WITH
    e: e = ode(f_stable(vpov),(vsv(t) |-> psv(t) |-> ppov(t)),t)
    s: s = {passed}
    x_p': x_p' = bind(bind(vsv',psv'),ppov')
    Inv: Inv = S
  THEN
    act1: 
      t,vsv,psv,ppov :| 
        t' = tp &
        vsv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(vsv') &
        psv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(psv') &
        ppov' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(ppov') &
        CBAPsolutionOf(t,t',bind(bind(vsv,psv),ppov),bind(bind(vsv',psv'),ppov'),
          ode(f_stable(vpov),(vsv(t) |-> psv(t) |-> ppov(t)),t),
        S)
  END

  ctrl_actuate_passed_accelerate
  REFINES Actuate
  ANY
    tp
    a
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s = turning
    grd2: a : Open2Closed(Rzero,Amax)
  WITH
    e: e = ode(f_accelerate(a |-> vpov |-> vsv(t)),(vsv(t) |-> psv(t) |-> ppov(t)),t)
    s: s = {passed}
    x_p': x_p' = bind(bind(vsv',psv'),ppov')
    Inv: Inv = S
  THEN
    act1: 
      t,vsv,psv,ppov :| 
        t' = tp &
        vsv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(vsv') &
        psv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(psv') &
        ppov' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(ppov') &
        CBAPsolutionOf(t,t',bind(bind(vsv,psv),ppov),bind(bind(vsv',psv'),ppov'),
          ode(f_accelerate(a |-> vpov |-> vsv(t)),(vsv(t) |-> psv(t) |-> ppov(t)),t),
        S)
  END

  ctrl_actuate_passed_decelerate
  REFINES Actuate
  ANY
    tp
    a
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: x_s = turning
    grd2: a : Closed2Open(uminus(B),Rzero)
  WITH
    e: e = ode(f_decelerate(a |-> vpov |-> vsv(t)),(vsv(t) |-> psv(t) |-> ppov(t)),t)
    s: s = {passed}
    x_p': x_p' = bind(bind(vsv',psv'),ppov')
    Inv: Inv = S
  THEN
    act1: 
      t,vsv,psv,ppov :| 
        t' = tp &
        vsv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(vsv') &
        psv' : RReal +-> RReal  & Closed2Closed(Rzero,t') <: dom(psv') &
        ppov' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(ppov') &
        CBAPsolutionOf(t,t',bind(bind(vsv,psv),ppov),bind(bind(vsv',psv'),ppov'),
          ode(f_decelerate(a |-> vpov |-> vsv(t)),(vsv(t) |-> psv(t) |-> ppov(t)),t),
        S)
  END

END