// ctrl.hcalibrate robot.tcalibrate robot.tcalibrated robot.return ctrl.return

interface IHandle
{
  in void hcalibrate();
  out void hcalibrated();
  in void stop();

  in void operate(); // start next batch
  out void finished(); // batch finished

  behaviour
  {
    enum State {Lost, Calibrating, Idle, Operating};
    State s = State.Lost;

    on stop: {s = State.Lost;}

    [s.Lost]
    {
      on hcalibrate:
        {
          s = State.Calibrating;
        }
      on operate:
        illegal;
      on operate:
        {}
    }
    [s.Calibrating]
      {
       on hcalibrate:
         illegal;
       on operate:
         illegal;
       on operate:
         {}
       on inevitable:
         {
           hcalibrated;
           s = State.Idle;
         }
     }
     [s.Idle]
     {
       on hcalibrate:
         illegal;
       on hcalibrate:
         {}
       on operate:
         s = State.Operating;
       on operate:
         finished;
     }
    [s.Operating]
    {
      on hcalibrate:
        illegal;
      on hcalibrate:
        {}
      on operate:
        illegal;
      on operate:
        {}
      on inevitable:
        {
          s = State.Idle;
          finished;
        }
    }
  }
}

interface ITransfer
{
  extern TrPosition $int$;

  in void tcalibrate();
  out void tcalibrated();
  in void stop();

  in void move(TrPosition x, TrPosition y);
  out void arrived();
  in void transfer(TrPosition x, TrPosition y);
  out void picked();
  out void placed();

  behaviour
  {
    enum State {Lost, Calibrating, Ready};
    State s = State.Lost;
    bool isPicked = false;

    on stop: s = State.Lost;

    [s.Lost]
    {
      on tcalibrate:
        {
          tcalibrated;
          s = State.Ready;
        }
      on move, transfer: illegal;
    }
    [s.Calibrating]
    {
      on inevitable:
        {
          tcalibrated;
          s = State.Ready;
        }
      on tcalibrate, move, transfer: illegal;
    }
    [s.Ready]
    {
       on move: arrived;

       on transfer: {s = State.Ready; picked; placed;}

       on tcalibrate: illegal;
    }
  }
}


component h
{
  provides IHandle ctrl;
  requires ITransfer robot;


  behaviour
  {
    enum State {Lost, Calibrating, Idle, Operating};
    subint usedCount {0..4};

    enum Operation {PreparingInput, TransferringInput, PreparingOutput, TransferringOutput, Finalizing};

    State s = State.Lost;
    usedCount calibrated = 0;
    usedCount requiredCalibrations = 3; // nr of subsystems requiring calibration (robot, inspector, feedPort)
    Operation o = Operation.PreparingInput;


    void tryCalibrated() {
      calibrated = calibrated + 1;
      if (calibrated == requiredCalibrations)
      {
        s = State.Idle;
        ctrl.hcalibrated();
      }
    }
    void ignoreIllegal() {
    }

    on ctrl.hcalibrate(): [s.Lost]
    {
      robot.tcalibrate();

      calibrated = 0;
      s = State.Calibrating;
    }
    on ctrl.hcalibrate(): [!s.Lost] ignoreIllegal();

    [s.Calibrating]
      {
       on robot.tcalibrated(): tryCalibrated();
     }

    [!s.Calibrating]
    {
      on
        robot.tcalibrated() :illegal;
    }
  }
}