CONTEXT
  LeftTurnAssistCtx
EXTENDS
  ControlledSystemCtx
CONSTANTS
  waiting
  turning
  passed
  Amax
  Amin
  B
  k
  q
  Vmax
  Tsv
  Tpov
  Tto0
  Ttovmax
  fsv1_decelerate
  fsv1_accelerate
  fsv1_accelerate_min
  fsv1_stable
  fsv2_speed
  fpov_speed
  f_decelerate
  f_accelerate
  f_accelerate_min
  f_stable
  ppov_init
  vpov_init
AXIOMS
  axm1: partition(STATES,{waiting},{turning},{passed})
  axm2: Amax : RRealPlusStar
  axm3: Amin : RRealPlusStar
  axm32: Amin |-> Amax : lt
  axm4: B : RRealPlusStar
  axm5: k : RRealPlusStar
  axm6: q : RRealPlusStar
  axm7: Vmax : RRealPlusStar
  axm8: 
    Tsv = (% asv |-> vsv |-> psv . asv : RReal & Rzero |-> asv : lt & vsv : RRealPlus & psv : RRealPlus & psv |-> q : leq |
            divide(plus(uminus(vsv) |-> sqrt(plus(times(vsv |-> vsv) |-> times(times(Rtwo |-> asv) |-> minus(q |-> psv))))) |-> asv)
          )
  axm9: Tsv : (RReal*RReal*RReal) +-> RReal
  axm10: Tpov = (% ppov . ppov : RReal | divide(minus(ppov |-> k) |-> Vmax))
  axm11: Tpov : RReal --> RReal
  axm12: Tto0 = (% a_ |-> v0_ . a_ : RReal & a_ |-> Rzero : lt & v0_ : RRealPlus | uminus(divide(v0_ |-> a_)))
  axm13: Ttovmax = (% a_ |-> v0_ . a_ : RReal & a_ |-> Rzero : gt & v0_ : RRealPlus & v0_ |-> Vmax : leq | divide(minus(Vmax |-> v0_) |-> a_))
  axm14: 
    fsv1_decelerate = (% a_ |-> v0_ . a_ : RReal & a_ |-> Rzero : lt & uminus(B) |-> a_ : leq & v0_ : RRealPlus |
                        untilF(Rzero,fcste(RReal*S,a_),Tto0(a_ |-> v0_),fcste(RReal*S,Rzero))
                      )
  axm15: 
    fsv1_accelerate = (% a_ |-> v0_ . a_ : RReal & a_ |-> Rzero : gt & v0_ : RRealPlus & v0_ |-> Vmax : leq |
              untilF(Rzero,fcste(RReal*S,a_),Ttovmax(a_ |-> v0_),fcste(RReal*S,Rzero))
                      )
  axm16: 
    fsv1_accelerate_min = (% a_ |-> v0_ . a_ : RReal & a_ |-> Amin : gt & v0_ : RRealPlus & v0_ |-> Vmax : leq |
                        untilF(Rzero,fcste(RReal*S,a_),Ttovmax(a_ |-> v0_),fcste(RReal*S,Rzero))
                      )
  axm17: fsv1_stable = (% t_ |-> eta_ . t_ : RRealPlus & eta_ : S | Rzero)
  axm18: fsv2_speed = (% t_ |-> (vsv_ |-> psv_ |-> ppov_) . t_ : RRealPlus & (vsv_ |-> psv_ |-> ppov_) : S | vsv_ )
  axm22: 
    fpov_speed = (% v_ . v_ : RReal & v_ : Closed2Closed(uminus(Vmax),Rzero) |
             fcste(RReal*S,v_)
           )
  axm23: 
    f_decelerate =
      (% vpov_ |-> a_ |-> v0_ . vpov_ : Closed2Closed(uminus(Vmax),Rzero) & a_ : Closed2Open(uminus(B),Rzero) & v0_ : RRealPlus |
        bind(bind(fsv1_decelerate(a_ |-> v0_),fsv2_speed),fpov_speed(vpov_))
      )
  axm24: 
    f_accelerate =
      (% vpov_ |-> a_ |-> v0_ . vpov_ : Closed2Closed(uminus(Vmax),Rzero) & a_ : Open2Closed(Rzero,Amax) & v0_ : RRealPlus & v0_ |-> Vmax : leq |
        bind(bind(fsv1_accelerate(a_ |-> v0_),fsv2_speed),fpov_speed(vpov_))
      )
  axm25: 
    f_accelerate_min =
      (% vpov_ |-> a_ |-> v0_ . vpov_ : Closed2Closed(uminus(Vmax),Rzero) & a_ : Open2Closed(Amin,Amax) & v0_ : RRealPlus & v0_ |-> Vmax : leq |
        bind(bind(fsv1_accelerate_min(a_ |-> v0_),fsv2_speed),fpov_speed(vpov_))
      )
  axm26: 
    f_stable =
      (% vpov_ . vpov_ : Closed2Closed(uminus(Vmax),Rzero) |
        bind(bind(fsv1_stable,fsv2_speed),fpov_speed(vpov_))
      )
  axm33: 
    ! vpov_,a_,v0_ .
      vpov_ : Closed2Closed(uminus(Vmax),Rzero) & a_ : Closed2Open(uminus(B),Rzero) & v0_ : RRealPlus =>
        partialPiecewiseContinuous(
          {Closed2Open(Rzero,Tto0(a_|->v0_)),Closed2Infinity(Tto0(a_|->v0_))},
          S,S,
          f_decelerate(vpov_|->a_|->v0_)
        )
  axm34: 
    ! vpov_,a_,v0_ .
      vpov_ : Closed2Closed(uminus(Vmax),Rzero) & a_ : Open2Closed(Rzero,Amax) & v0_ : RRealPlus & v0_ |-> Vmax : leq =>
        partialPiecewiseContinuous(
          {Closed2Open(Rzero,Ttovmax(a_|->v0_)),Closed2Infinity(Ttovmax(a_|->v0_))},
          S,S,
          f_accelerate(vpov_|->a_|->v0_)
        )
  axm35: 
    ! vpov_,a_,v0_ .
      vpov_ : Closed2Closed(uminus(Vmax),Rzero) & a_ : Closed2Closed(Amin,Amax) & v0_ : RRealPlus & v0_ |-> Vmax : leq =>
        partialPiecewiseContinuous(
          {Closed2Open(Rzero,Ttovmax(a_|->v0_)),Closed2Infinity(Ttovmax(a_|->v0_))},
          S,S,
          f_accelerate_min(vpov_|->a_|->v0_)
        )
  axm36: 
    ! vpov_ .
      vpov_ : Closed2Closed(uminus(Vmax),Rzero) =>
        f_stable(vpov_) : C0(RRealPlus*S,S)
  axm37: ppov_init : RReal
  axm38: ppov_init |-> k : gt
  axm39: vpov_init : Closed2Closed(uminus(Vmax),Rzero)
END