MACHINE
  PendulumLin
REFINES
  Pendulum
SEES
  PendulumLinCtx
VARIABLES
  t
  theta
  thetap
  t_sense
  control_fun
  theta_sense
  thetap_sense
  control_fun_lin
  theta_lin
  thetap_lin
  theta_lin_sense
  thetap_lin_sense
INVARIANTS
  inv1: theta_lin : RReal +-> RReal
  inv2: thetap_lin : RReal +-> RReal
  inv3: Closed2Closed(Rzero,t) <: dom(theta_lin)
  inv4: Closed2Closed(Rzero,t) <: dom(thetap_lin)
  inv5: DeltaApproximation(Closed2Closed(Rzero,t),delta,bind(theta,thetap),bind(theta_lin,thetap_lin))
  inv6: 
    ! t_ . t_ : Closed2Closed(Rzero,t) =>
      abs(theta(t_)) |-> thetabound : lt &
      abs(theta_lin(t_)) |-> minus(thetabound|->delta) : lt
  inv7: control_fun_lin : RReal +-> RReal
  inv8: DeltaApproximation(Closed2Infinity(t),control_delta,control_fun,control_fun_lin)
  inv9: theta_lin_sense : RReal
  inv10: thetap_lin_sense : RReal
  inv11: abs(theta_lin_sense) |-> minus(thetabound |-> delta) : leq
  inv12: DeltaNeighborhood(delta,theta_sense|->thetap_sense,theta_lin_sense|->thetap_lin_sense)
EVENTS
  INITIALISATION
  THEN
    act1: t := Rzero
    act2: theta := { Rzero |-> theta0 }
    act3: thetap := { Rzero |-> Rzero }
    act4: t_sense := Rzero
    act5: theta_sense,thetap_sense := theta0,Rzero
    act6: control_fun := PendulumRawControl(omega0,theta0,Rzero,Rzero)
    act7: control_fun_lin := PendulumLinControl(omega0,theta0,Rzero,Rzero)
    act8: theta_lin := { Rzero |-> theta0 }
    act9: thetap_lin := { Rzero |-> Rzero }
    act10: theta_lin_sense,thetap_lin_sense := theta0,Rzero
  END

  Behave
  REFINES Behave
  ANY
    e
    tp
  WHERE
    grd1: e : DE(S)
    grd2: Solvable(Closed2Closed(t,tp),e)
    grd4: theta(t) |-> thetabound : lt
    grd5: tp : RRealPlus
    grd6: t |-> tp : lt
    grd7: 
      CBAPsolutionOfFIS(t,tp,bind(theta,thetap),e,
        { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            abs(theta_) |-> thetabound : lt
          | theta_|->thetap_ })
    grd8: 
      CBAPsolutionOfFIS(t,tp,bind(theta_lin,thetap_lin),e,
        { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            abs(theta_) |-> thetabound : lt
          | theta_|->thetap_ })
  THEN
    act1: 
      t,theta,thetap,theta_lin,thetap_lin :|
        t' = tp &
        theta' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(theta') &
        thetap' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(thetap') &
        CBAPsolutionOf(t,t',bind(theta,thetap),bind(theta',thetap'),e,
          { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            abs(theta_) |-> thetabound : lt
          | theta_|->thetap_ }) &
        theta_lin' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(theta_lin') &
        thetap_lin' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(thetap_lin') &
        CBAPsolutionOf(t,t',bind(theta_lin,thetap_lin),bind(theta_lin',thetap_lin'),e,
          { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            abs(theta_) |-> thetabound : lt
          | theta_|->thetap_ })
  END

  sense_angle
  REFINES sense_angle
  WHERE
    grd1: Rzero |-> abs(theta_lin(t)) : lt
  THEN
    act1: t_sense,theta_sense,thetap_sense := t,theta(t),thetap(t)
    act2: theta_lin_sense,thetap_lin_sense := theta_lin(t),thetap_lin(t)
  END

  transition_calculate_control
  REFINES transition_calculate_control
  THEN
    act1: control_fun := PendulumRawControl(omega0,theta_sense,thetap_sense,t_sense)
    act2: control_fun_lin := PendulumLinControl(omega0,theta_lin_sense,thetap_lin_sense,t_sense)
  END

  actuate_balance
  REFINES actuate_balance
  ANY
    tp
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd2: 
      SolvableWith(
        Closed2Closed(t,tp),
        PendulumRaw(omega0,(theta(t)|->thetap(t)),t),
          control_fun
      )
    grd3: 
      SolvableWith(
        Closed2Closed(t,tp),
        PendulumLin(omega0,(theta_lin(t)|->thetap_lin(t)),t),
        control_fun_lin
      )
    grd4: abs(theta(t)) |-> thetabound : lt
    grd5: abs(theta_lin(t)) |-> minus(thetabound|->delta) : lt
  THEN
    act1: 
      t,theta,thetap,theta_lin,thetap_lin :|
        t' = tp &
        theta' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(theta') &
        thetap' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(thetap') &
        CBAPsolutionOf(
          t,t',
          bind(theta,thetap),
          bind(theta',thetap'),
          withControl(
            Closed2Closed(t,t'),
            PendulumRaw(omega0,(theta(t)|->thetap(t)),t),
            control_fun
          ),
          { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            abs(theta_) |-> thetabound : lt
          | theta_|->thetap_ }
        ) &
        theta_lin' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(theta_lin') &
        thetap_lin' : RReal +-> RReal & Closed2Closed(Rzero,t') <: dom(thetap_lin') &
        CBAPsolutionOf(
          t,t',
          bind(theta_lin,thetap_lin),
          bind(theta_lin',thetap_lin'),
          withControl(
            Closed2Closed(t,t'),
            PendulumLin(omega0,(theta_lin(t)|->thetap_lin(t)),t),
            control_fun_lin
          ),
          { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            abs(theta_) |-> minus(thetabound|->delta) : lt
          | theta_|->thetap_ }
        )
  END

END