///////////////////////////////////////////////////////////////////////////////
// This model is part of the Camera Dezyne Example Project.
// The model contains the specification of the following component systems:
// - Acquisition
// - Optics
// - HardwareLayer
// - Camera 
// - Camera2
// ... and the behavioural specification for:
// - the IControl interface
// - the Driver component
// - the IAcquisition interface
// - the Acquire component
// - the IOptics interface
// - the OpticsControl component
// The example contains artificially inserted design bugs:
// - the acquired image is not stored in memory. 
//     Simulate the Acquire component and see if you spot the error
// - the verification of the Driver component fails
//     Verify the Driver component and see if you can fix the problem
///////////////////////////////////////////////////////////////////////////////

import ihal.dzn;
import simhal.dzn;

interface IControl
{
  in void setup();
  in void shoot();
  in void release();

  out void ready();
  out void focus();
  out void image();

  behaviour
  {
    enum State {Idle, Setup, Ready, Acquire};
    State state = State.Idle;

    [state.Idle] {
      on setup:{ state = State.Setup; }
      on shoot,
      release: illegal;
    }
    [state.Setup] {
      on setup: illegal;
      on shoot: { state = State.Acquire; }
      on release: { state = State.Idle; }
      on inevitable: { focus; }
      on inevitable: { ready; state = State.Ready; }
    }
    [state.Ready] {
      on setup: illegal;
      on release: { state = State.Idle; }
      on shoot: { state = State.Acquire; }
      on inevitable: { focus; }
    }
    [state.Acquire] {
      on setup,
      release,
      shoot: illegal;
      on inevitable: { image; state = State.Idle; }
    }
  }
}

component Acquisition
{
  provides IAcquisition port;

  requires IHardware acquire_hardware;
  requires IHardware contrast_hardware;

  system
  {
    Acquire acquire;

    Memory memory;
    CMOS sensor;

    port <=> acquire.port;

    acquire.memory <=> memory.port;
    acquire.sensor <=> sensor.port;
    acquire_hardware <=> sensor.acquire_hardware;
    contrast_hardware <=> sensor.contrast_hardware;
  }
}

component Optics
{
  provides IOptics port;
  requires IHardware flash_hardware;

  system
  {
    OpticsControl optics;
    Lens lens;
    Shutter shutter;
    Flash flash;

    port <=> optics.port;
    optics.lens <=> lens.port;
    optics.shutter <=> shutter.port;
    optics.flash <=> flash.port;
    flash_hardware <=> flash.hardware;
  }
}

component HardwareLayer
{
  provides IHardware acquire;
  provides IHardware contrast;
  provides IHardware flash;

  system
  {
    Hardware acquire_hardware;
    Hardware contrast_hardware;
    Hardware flash_hardware;

    acquire <=> acquire_hardware.port;
    contrast <=> contrast_hardware.port;
    flash <=> flash_hardware.port;
  }
}

component Camera
{
  provides IControl control;

  system
  {
    Driver driver;

    Acquisition acquisition;
    Optics optics;
    HardwareLayer hardware;

    control <=> driver.control;
    driver.acquisition <=> acquisition.port;
    driver.optics <=> optics.port;

    hardware.acquire <=> acquisition.acquire_hardware;
    hardware.contrast <=> acquisition.contrast_hardware;
    hardware.flash <=> optics.flash_hardware;
  }
}

component Camera2
{
  provides IControl control;

  system
  {
    Driver driver;

    Acquire acquisition;
    Memory memory;
    CMOS sensor;
    Hardware acquire_hardware;
    Hardware contrast_hardware;

    OpticsControl optics;
    Lens lens;
    Shutter shutter;
    Flash flash;
    Hardware flash_hardware;

    control <=> driver.control;
    driver.acquisition <=> acquisition.port;
    driver.optics <=> optics.port;

    acquisition.memory <=> memory.port;
    acquisition.sensor <=> sensor.port;
    acquire_hardware.port <=> sensor.acquire_hardware;
    contrast_hardware.port <=> sensor.contrast_hardware;


    optics.lens <=> lens.port;
    optics.shutter <=> shutter.port;
    optics.flash <=> flash.port;
    flash_hardware.port <=> flash.hardware;
  }
}

component Driver
{
  provides IControl control;
  requires IAcquisition acquisition;
  requires IOptics optics;

  behaviour
  {
    enum State {Idle, Setup, Ready, Acquire};
    enum Contrast {Down, Up, Max};
    enum Zoom {In, Out};

    State state = State.Idle;
    Contrast contrast = Contrast.Down;
    Zoom zoom = Zoom.In;
    bool ready = false;

    [state.Idle]
    {
      on control.setup(): {optics.prepare(); acquisition.contrast_gradient(); state = State.Setup;}
    }
    [state.Setup]
    {
      on acquisition.lower_contrast():
      {
        [contrast.Up]
        {
          if(zoom.In) {optics.focus_out(); zoom = Zoom.Out;}
          else        {optics.focus_in(); zoom = Zoom.In;}

          contrast = Contrast.Max;

          if(ready)   {contrast = Contrast.Down; control.ready(); ready = false; state = State.Ready;}
          else        {control.focus();}
        }
        [contrast.Down]
        {
          if(zoom.In) {optics.focus_out(); zoom = Zoom.Out;}
          else        {optics.focus_in(); zoom = Zoom.In;}
          contrast = Contrast.Down;
          control.focus();
        }
        [otherwise]   {control.focus();}
      }
      on acquisition.higher_contrast():
      {
        if(zoom.In) {optics.focus_in();}
        else        {optics.focus_out();}
        contrast = Contrast.Up;
        control.focus();
      }
      on optics.ready():
      {
        if(contrast.Max) {control.ready(); ready = false; state = State.Ready;}
        else             {ready = true;}
      }
      on control.release(): {acquisition.cancel(); state = State.Idle;}
      on control.shoot(): {acquisition.acquire(); optics.capture(); state = State.Acquire;}
    }
    [state.Ready]
    {
      on control.shoot(): {acquisition.acquire(); optics.capture(); state = State.Acquire;}
      on control.release(): {acquisition.cancel(); state = State.Idle;}
      on acquisition.lower_contrast(),
      acquisition.higher_contrast(),
      optics.ready(): {control.focus();}
    }
    [state.Acquire]
    {
      on acquisition.image(): {control.image(); state = State.Idle;}
      on optics.ready(): {}
    }
  }
}

interface IAcquisition
{
  in void contrast_gradient();
  in void cancel();
  in void acquire();
  out void image();
  out void higher_contrast();
  out void lower_contrast();

  behaviour
  {
    enum State {Idle, Contrast, Acquire};
    State state = State.Idle;

    on contrast_gradient:
    {
      [state.Idle] {state = State.Contrast;}
      [otherwise]  illegal;
    }
    on acquire:
    {
      [state.Contrast] {state = State.Acquire;}
      [otherwise]      illegal;
    }
    on cancel:
    {
      [state.Idle] illegal;
      [otherwise]  {state = State.Idle;}
    }
    on inevitable:
    {
      [state.Contrast] lower_contrast;
      [state.Contrast] higher_contrast;
      [state.Acquire]  {image; state = State.Idle;}
    }
  }
}

component Acquire
{
  provides IAcquisition port;
  requires IMemory memory;
  requires ISensor sensor;
  behaviour
  {
    enum State {Idle, Contrast, Acquire};
    State state = State.Idle;

    [state.Idle]
    {
      on port.contrast_gradient():
      {
        sensor.enable();
        state = State.Contrast;
      }
    }
    [state.Contrast]
    {
      on port.acquire(): {sensor.acquire(); state = State.Acquire;}
      on port.cancel(): {sensor.cancel(); state = State.Idle;}
      on sensor.higher_contrast(): port.higher_contrast();
      on sensor.lower_contrast(): port.lower_contrast();
    }
    [state.Acquire]
    {
      on port.cancel(): {sensor.cancel(); state = State.Idle;}
      on sensor.image():{/*memory.store();*/ port.image(); state = State.Idle;}
    }
  }
}

interface IOptics
{
  in void prepare();
  in void capture();
  in void cancel();
  out void ready();

  in void focus_in();
  in void focus_out();

  behaviour
  {
    enum State {Idle, Prepare, Ready};
    State state = State.Idle;
    on prepare:
    {
      [state.Idle] state = State.Prepare;
      [otherwise]  illegal;
    }
    on cancel:
    {
      state = State.Idle;
    }
    on inevitable: [state.Prepare] {ready; state = State.Ready;}
    on capture:
    {
      [state.Idle] illegal;
      [otherwise]  state = State.Idle;
    }
    on focus_in:  {}
    on focus_out: {}
  }
}

component OpticsControl
{
  provides IOptics port;

  requires ILens lens;
  requires IShutter shutter;
  requires IFlash flash;

  behaviour
  {
    enum State {Idle, Prepare, Ready};
    State state = State.Idle;
    bool ready = false;
    on port.prepare():
    {
      [state.Idle] {state = State.Prepare; flash.prepare();}
    }
    on port.cancel():
    {
      flash.cancel();
      state = State.Idle;
    }
    on flash.ready():
    {
      if(state.Prepare) {state = State.Ready; port.ready();}
    }
    on port.capture():
    {
      [state.Prepare] {state = State.Idle; flash.cancel(); shutter.expose();}
      [state.Ready]   {state = State.Idle; flash.flash();  shutter.expose(); }
    }
    on port.focus_in(): lens.zoom_in();
    on port.focus_out(): lens.zoom_out();
  }
}