MACHINE
  Robot_2
REFINES
  Robot_1
SEES
  Robot_2_Ctx
VARIABLES
  t
  Target
  DirectionControl
  vC
  pC
INVARIANTS
  inv1: DirectionControl : RReal*RReal
  inv2: DeltaNeighborhood(ControllerSpeedLimit,DirectionControl,Rzero|->Rzero)
  inv3: pC : RReal +-> S
  inv6: Closed2Closed(Rzero,t) <: dom(pC)
  inv7: vC : RReal +-> S
  inv8: Closed2Closed(Rzero,t) <: dom(vC)
  inv11: Direction = DirectionControl
  inv12: DeltaApproximation(Closed2Closed(Rzero,t),AppDelta,pA,pC)
  inv13: ! t_ . t_ : Closed2Closed(Rzero,t) => plannar_distance(pC(t_),Rzero|->Rzero) |-> minus(CriticalDistance |-> AppDelta) : lt
EVENTS
  INITIALISATION
  THEN
    act1: t := Rzero
    act3: pC := { Rzero |-> (px0 |-> py0) }
    act4: vC := { Rzero |-> (Rzero |-> Rzero) }
    act5: Target :| Target' : RReal*RReal & plannar_distance(Target',Rzero|->Rzero) |-> minus(CriticalDistance |-> CloseEnough) : lt
    act6: DirectionControl := Rzero |-> Rzero
  END

  Behave
  REFINES Behave
  ANY
    e2
    tp
  WHERE
    grd1: e2 : DE(S2)
    grd2: Solvable(Closed2Closed(t,tp),e2)
    grd3: plannar_distance(Target,pC(t)) |-> plus(CloseEnough|->AppDelta) : gt
    grd4: tp : RRealPlus
    grd5: t |-> tp : lt
    grd6: CBAPsolutionOfFIS(t,tp,bind(vC,pC),e2,{ (vx_|->vy_)|->(px_|->py_) | plannar_distance(Target,px_|->py_) |-> CloseEnough : gt })
  WITH
    e: 
      e : DE(S) &
      Solvable(Closed2Closed(t,t'),e) & (
        ! etaA,etaC .
          etaA : RRealPlus +-> S & etaC : RRealPlus +-> S2 &
          Closed2Closed(Rzero,t') <: dom(etaA) &
          Closed2Closed(Rzero,t') <: dom(etaC) &
          solutionOf(Closed2Closed(t,t'),etaA,e) &
          solutionOf(Closed2Closed(t,t'),etaC,e2) =>
            DeltaApproximation(Closed2Closed(t,t'),AppDelta,etaA,fproj2(etaC))
      )
    pA': 
      pA' : RReal +-> S & Closed2Closed(Rzero,t') <: dom(pA') &
      DeltaApproximation(Closed2Closed(Rzero,t'),AppDelta,pA',pC')
  THEN
    act1: 
      t,pC,vC :|
        pC' : RReal +-> S &
        vC' : RReal +-> S &
        t' = tp &
        Closed2Closed(Rzero,t') <: dom(pC') &
        Closed2Closed(Rzero,t') <: dom(vC') &
        CBAPsolutionOf(t,t',bind(vC,pC),bind(vC',pC'),e2,{ (vx_|->vy_)|->(px_|->py_) | plannar_distance(Target,px_|->py_) |-> CloseEnough : gt })
  END

  sense_close_enough
  REFINES sense_close_enough
  ANY
    next_direction_ctrl
    next_target
  WHERE
    grd1: next_direction_ctrl : RReal*RReal
    grd2: next_target : RReal*RReal
    grd3: plannar_distance(Target,pC(t)) |-> minus(CloseEnough|->AppDelta) : leq
    grd4: DeltaNeighborhood(ControllerSpeedLimit,Rzero|->Rzero,next_direction_ctrl)
    grd5: plannar_distance(next_target,Rzero|->Rzero) |-> minus(CriticalDistance |-> CloseEnough) : lt
  WITH
    next_direction: next_direction = next_direction_ctrl
  THEN
    act1: DirectionControl := next_direction_ctrl
    act2: Target := next_target
  END

  transition_change_direction
  REFINES transition_change_direction
  ANY
    new_direction_ctrl
  WHERE
    grd1: new_direction_ctrl : RReal*RReal
    grd2: DeltaNeighborhood(ControllerSpeedLimit,Rzero|->Rzero,new_direction_ctrl)
  WITH
    new_direction: new_direction = new_direction_ctrl
  THEN
    act1: DirectionControl := new_direction_ctrl
  END

  transition_change_target
  REFINES transition_change_target
  END

  actuate_movement
  REFINES actuate_movement
  ANY
    tp
  WHERE
    grd1: plannar_distance(Target,pC(t)) |-> plus(CloseEnough|->AppDelta) : gt
    grd7: tp : RRealPlus
    grd8: t |-> tp : lt
    grd9: 
      CBAPsolutionOfFIS(t,tp,bind(vC,pC),
        withControl(
          Closed2Closed(t,tp),
          SecondOrder2DimensionSystem(
            ControlCoefficient,
            DeltaNeighborhoodSet(ControllerSpeedLimit,Rzero|->Rzero)*(RReal*RReal),
            t,
            vC(t)|->pC(t)
          ),
          PointwiseSlopedControl(
            Closed2Closed(t,tp),
            prj1(DirectionControl),prj2(DirectionControl),
            t
          )
        )
      ,{ (vC_|->pC_) | plannar_distance(Target,pC_) |-> plus(CloseEnough|->AppDelta) : gt })
  WITH
    pA': 
      pA' : RReal +-> S &
      Closed2Closed(Rzero,t') <: dom(pA') &
      CBAPsolutionOf(
          t,t',
          pA,pA',
          withControl(
            Closed2Closed(t,t'),
            FirstOrder2DimensionSystem(DeltaNeighborhoodSet(SpeedLimit,Rzero|->Rzero),t,pA(t)),
            PointwiseControl(Closed2Closed(t,t'),prj1(Direction),prj2(Direction),t)
          ),
          { px_|->py_ | plannar_distance(Target,px_|->py_) |-> CloseEnough : gt }
        ) &
      DeltaApproximation(Closed2Closed(Rzero,t'),AppDelta,pA',pC')
  THEN
    act1: 
      t,pC,vC :|
        pC' : RReal +-> S &
        vC' : RReal +-> S &
        t' = tp &
        Closed2Closed(Rzero,t') <: dom(pC') &
        Closed2Closed(Rzero,t') <: dom(vC') &
        CBAPsolutionOf(
          t,t',
          bind(vC,pC),
          bind(vC',pC'),
          withControl(
            Closed2Closed(t,t'),
            SecondOrder2DimensionSystem(
              ControlCoefficient,
              DeltaNeighborhoodSet(ControllerSpeedLimit,Rzero|->Rzero)*(RReal*RReal),
              t,
              vC(t)|->pC(t)
            ),
            PointwiseSlopedControl(
              Closed2Closed(t,t'),
              prj1(DirectionControl),prj2(DirectionControl),
              t
            )
          ),
          { (vC_|->pC_) | plannar_distance(Target,pC_) |-> plus(CloseEnough|->AppDelta) : gt }
        )
  END

END