MACHINE
  Pendulum
REFINES
  Generic
SEES
  PendulumCtx
VARIABLES
  t
  theta
  thetap
  t_sense
  theta_sense
  thetap_sense
  control_fun
INVARIANTS
  inv1: theta : RReal +-> RReal
  inv2: thetap : RReal +-> RReal
  inv3: Closed2Closed(Rzero,t) <: dom(theta)
  inv4: Closed2Closed(Rzero,t) <: dom(thetap)
  inv5: x_p = bind(theta,thetap)
  inv6: ! t_ . t_ : Closed2Closed(Rzero,t) => abs(theta(t_)) |-> thetamax : lt
  inv7: x_s = control
  inv8: t_sense : RRealPlus
  inv9: theta_sense : RReal
  inv10: thetap_sense : RReal
  inv11: control_fun : RReal +-> RReal
  inv12: Closed2Infinity(t_sense) <: dom(control_fun)
  inv13: abs(theta_sense) |-> thetamax : leq
EVENTS
  INITIALISATION
  WITH
    x_p': x_p' = { Rzero |-> (theta0|->Rzero) }
    x_s': x_s' = control
  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)
  END

  Behave
  REFINES Behave
  ANY
    e
    tp
  WHERE
    grd1: e : DE(S)
    grd2: Solvable(Closed2Closed(t,tp),e)
    grd4: theta(t) |-> thetamax : lt
    grd5: tp : RRealPlus
    grd6: t |-> tp : lt
    grd7: 
      CBAPsolutionOfFIS(t,tp,bind(theta,thetap),e,
        { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            theta_ |-> thetamax : lt
          | theta_|->thetap_ })
  WITH
    Inv: 
      Inv = { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            theta_ |-> thetamax : lt
          | theta_|->thetap_ }
    x_p': x_p' = bind(theta',thetap')
  THEN
    act1: 
      t,theta,thetap :|
        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 &
            theta_ |-> thetamax : lt
          | theta_|->thetap_ })
  END

  sense_angle
  REFINES Sense
  WHERE
    grd1: Rzero |-> abs(theta(t)) : lt
  WITH
    x_s': x_s' = control
    s: s = { control }
    p: 
      p = {control}*RReal*{ theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
                  abs(theta_) |-> thetamax : geq
                | theta_|->thetap_ }
  THEN
    act1: t_sense,theta_sense,thetap_sense := t,theta(t),thetap(t)
  END

  transition_calculate_control
  REFINES Transition
  WITH
    x_s': x_s' = control
    s: s = { control }
  THEN
    act1: control_fun := PendulumRawControl(omega0,theta_sense,thetap_sense,t_sense)
  END

  actuate_balance
  REFINES Actuate
  ANY
    tp
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd2: 
      SolvableWith(
        Closed2Closed(t,tp),
        PendulumRaw(omega0,(theta(t)|->thetap(t)),t),
          control_fun
      )
    grd4: theta(t) |-> thetamax : lt
  WITH
    e: 
      e = withControl(
        Closed2Closed(t,t'),
        PendulumRaw(omega0,(theta(t)|->thetap(t)),t),
        control_fun
      )
    Inv: 
      Inv = { theta_,thetap_ . theta_ : RReal & thetap_ : RReal &
            abs(theta_) |-> thetamax : lt
          | theta_|->thetap_ }
    x_p': x_p' = bind(theta',thetap')
    s: s = {control}
  THEN
    act1: 
      t,theta,thetap :|
        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_) |-> thetamax : lt
          | theta_|->thetap_ }
        )
  END

END