CONTEXT
  PendulumCtx
EXTENDS
  GenericCtx
CONSTANTS
  omega0
  thetamax
  theta0
  control
AXIOMS
  axm1: omega0 : RReal
  axm2: omega0 /= Rzero
  axm3: thetamax = theta_max(omega0)
  axm4: theta0 : RReal
  axm5: abs(theta0) |-> thetamax : lt
  axm6: partition(STATES,{control})
END