CONTEXT
  Robot_0_Ctx
EXTENDS
  GenericCtx
CONSTANTS
  SpeedLimit
  CloseEnough
  px0
  py0
  CriticalDistance
AXIOMS
  axm1: SpeedLimit : RReal
  axm2: Rzero |-> SpeedLimit : lt
  axm3: px0 : RReal
  axm4: py0 : RReal
  axm5: CloseEnough : RReal
  axm6: Rzero |-> CloseEnough : lt
  axm7: CriticalDistance : RReal
  axm8: Rzero |-> CriticalDistance : lt
  axm9: CloseEnough |-> CriticalDistance : lt
  axm10: plannar_distance(px0|->py0,Rzero|->Rzero) |-> CriticalDistance : lt
END