//purpose: A very simple illustration of how two devices might be started
///////////////////////////////////////////////////////////////////////////////
// This is the behavioural specification for the StartDevices component.
// The responsibility of the component is to control the starting and stopping 
// of two devices.  
// The purpose of the example is to familiarise you with Dezyne features like 
// simulation and verification using a simple case.
// As a start you might want to start a verification and see if you can fix the 
// reported problem.
///////////////////////////////////////////////////////////////////////////////

component StartDevices
{
  provides StartControlIF startIF;
  requires Device1IF device1IF;
  requires Device2IF device2IF;

  behaviour
  {
    subint Count {0..5};
    enum States { Idle, Starting, Started };
    Device2IF.Result result2 = Device2IF.Result.NOK;
    States state = States.Idle;
    Count count = 0;

    [state.Idle]
    {
      on startIF.startAll():
      {
        count = 0;
        state = States.Starting;        
        device1IF.turnon();
      }
    }

    [state.Starting]
    {
      on device1IF.ok(): 
      {
        result2 = device2IF.turnon(); 
        if ( result2 == Device2IF.Result.OK )
        {
          state = States.Started;
          startIF.allStarted();         
        }
        else
        {
//          device1IF.turnoff();
          state = States.Idle;
          startIF.startFailed();
        }

      } 
      on device1IF.nok():
      {
        if ( count < 5 )
        {
          count = count + 1;
          device1IF.turnon();
        }
        else
        {
          state = States.Idle;
          startIF.startFailed();
        }
      }
    }

    [state.Started]
    {
      on startIF.stopAll(): 
      { 
        device1IF.turnoff(); 
        device2IF.turnoff();
        state = States.Idle;
      }
    } 
  }
}

///////////////////////////////////////////////////////////////////////////////
// These are the behavioural specifications of the interface to 
// two devices which can be turned on and turned off. 
///////////////////////////////////////////////////////////////////////////////

interface Device1IF
{
  in void turnon();
  in void turnoff();
  out void ok();
  out void nok();

  behaviour
  {
    enum State { Off, GoingOn, On };
    State state = State.Off;

    [state.Off]
    {
      on turnon: state = State.GoingOn; 
      on turnoff: illegal;
    }

    [state.GoingOn]
    {
      on inevitable: { ok; state = State.On; }
      on inevitable: { nok; state = State.Off;  }
      on turnon: illegal;
      on turnoff: illegal;      
    }     

    [state.On]
    {
      on turnon: illegal;
      on turnoff: { state = State.Off; }
    }
  }
}


interface Device2IF
{
  enum Result { OK, NOK };
  in Result turnon();
  in void turnoff();

  behaviour
  {
    enum State { Off, On };
    State state = State.Off;

    [state.Off]
    {
      on turnon: { reply( Result.OK ); state = State.On; }
      on turnon: { reply( Result.NOK); }
      on turnoff: illegal;
    }
    [state.On]
    {
      on turnon: illegal;
      on turnoff: { state = State.Off; }
    }   
  }
}

///////////////////////////////////////////////////////////////////////////////
// This is the behavioural specification of the interface to the 
// StartControl component which controls the starting and stopping of two devices.
///////////////////////////////////////////////////////////////////////////////

interface StartControlIF
{
  enum Result { OK, NOK };
  in void startAll();
  in void stopAll();
  out void allStarted();
  out void startFailed();

  behaviour
  {
    enum States { Idle, Starting, Started };
    States state = States.Idle; 

    [state.Idle]
    {
      on startAll: state = States.Starting;
      on stopAll: illegal;
    }
    [state.Starting]
    {
      on startAll, stopAll: illegal;
      on inevitable: { state = States.Idle; startFailed; }
      on inevitable: { state = States.Started; allStarted; }
    }
    [state.Started]
    {
      on startAll: illegal;
      on stopAll: state = States.Idle; 
    } 
  }
}