//purpose: Show valued events and replies

enum result_t {
   OK,
   NOK
};


// This interface specifies the protocol of a device which has to be initialised and
// calibrated before it can perform actions.
// Each of these activities can succeed (OK) or fail (NOK).
interface IDevice {

    in result_t initialise();
    in result_t calibrate();
    in result_t perform_action1();
    in result_t perform_action2();

    behaviour {
        enum State {
            Uninitialised,
            Initialised,
            Calibrated
        };
        State s = State.Uninitialised;

        [s.Uninitialised] {
            on initialise: {
                [true] { reply(result_t.OK);   s = State.Initialised;   }
                [true] { reply(result_t.NOK);                           }
            }
            on calibrate,
               perform_action1,
               perform_action2:
                illegal;
        }
        [s.Initialised] {
            on calibrate: {
                [true] { reply(result_t.OK);    s = State.Calibrated;  }
                [true] { reply(result_t.NOK);                          }
            }
            on initialise:
                reply(result_t.OK);
            on perform_action1,
               perform_action2:
                illegal;
        }
        [s.Calibrated] {
            on perform_action1,
               perform_action2: {
                [true] { reply(result_t.OK);                           }
                [true] { reply(result_t.NOK);   s = State.Initialised; }
            }
            on calibrate:
                reply(result_t.OK);
            on initialise:
                reply(result_t.OK);
        }

    }
}

// This interface specifies the protocol of a component which, after being initialised,
// can perform actions and recover from error situations.
// Each of these activities can succeed (OK) or fail (NOK).
interface IComp {
    in result_t initialise();
    in result_t recover();
    in result_t perform_actions();

    behaviour {
        enum State {
            Uninitialised,
            Initialised,
            Error
        };
        State s = State.Uninitialised;

        [s.Uninitialised] {
            on initialise: {
                [true] { reply(result_t.OK);    s = State.Initialised;   }
                [true] { reply(result_t.NOK);                            }
            }
            on recover,
               perform_actions:
                illegal;
        }
        [s.Initialised] {
            on perform_actions: {
                [true] { reply(result_t.OK);                     }
                [true] { reply(result_t.NOK);   s = State.Error; }
            }
            on initialise,
               recover:
                 illegal;
        }
        [s.Error] {
            on recover: {
                [true] { reply(result_t.OK);  s = State.Initialised; }
                [true] { reply(result_t.NOK);                        }
            }
            on initialise,
               perform_actions:
                 illegal;
        }
    }
}

// This component initialises and controls two devices, and tries to recover
// from errors reported by these devices
component OK_NOK {
    provides IComp client;
    requires IDevice device_A;
    requires IDevice device_B;

    behaviour {
        enum State {
            Uninitialised,
            Initialised,
            Error
        };
        State s = State.Uninitialised;

        [s.Uninitialised] {
            on client.initialise(): {
                // try to initialise and calibrate both devices.
                // reply NOK in case of an error
                result_t res = device_A.initialise();
                if (res.OK) {
                    res = device_B.initialise();
                }
                if (res.OK) {
                    res = device_A.calibrate();
                }
                if (res.OK) {
                    res = device_B.calibrate();
                }

                if (res.OK) {
                    reply(result_t.OK);
                    s = State.Initialised;
                } else {
                    reply(result_t.NOK);
                }
            }
            on client.recover,
               client.perform_actions:
                 illegal;
        }
        [s.Initialised] {
            on client.perform_actions(): {
                // try to perform two actions on both devices.
                // reply NOK in case of an error
                result_t res = device_A.perform_action1();
                if (res.OK) {
                    res = device_B.perform_action1();
                }
                if (res.OK) {
                    res = device_A.perform_action2();
                }
                if (res.OK) {
                    res = device_B.perform_action2();
                }

                if (res.OK) {
                    reply(result_t.OK);
                } else {
                    reply(result_t.NOK);
                    s = State.Error;
                }
            }
            on client.initialise,
               client.recover:
                    illegal;
        }
        [s.Error] {
            on client.recover(): {
                // try to recover from a previous error by re-calibrating both devices.
                result_t res = device_A.calibrate();
                if (res.OK) {
                    res = device_B.calibrate();
                }

                if (res.OK) {
                    reply(result_t.OK);
                    s = State.Initialised;
                } else {
                    reply(result_t.NOK);
                }
            }
        }
    }
}

// This component provides an implementation of the IDevice interface.
// Performance of action1 will succeed, but action2 will fail, after which
// the component has to be re-calibrated.
component Device
{
  provides IDevice i;
  behaviour
    {
      enum State {
        Uninitialised,
        Initialised,
        Calibrated
      };

      State s = State.Uninitialised;
      on i.initialise(): {
        [s.Uninitialised] { reply(result_t.OK); s = State.Initialised; }
        [otherwise] reply(result_t.OK);
      }
      on i.calibrate(): {
        [!s.Uninitialised] { reply(result_t.OK); s = State.Calibrated;  }
      }
      on i.perform_action1(): {
        [s.Calibrated] { reply(result_t.OK); }
      }
      on i.perform_action2(): {
        [s.Calibrated] { reply(result_t.NOK); s = State.Initialised; }
      }
    }
}

// This system component combines the OK_NOK component
// with two identical Device components.
component TwoDevices
{
  provides IComp client;
  system
  {
    OK_NOK rv;
    Device deviceA;
    Device deviceB;

    client <=> rv.client;
    rv.device_A <=> deviceA.i;
    rv.device_B <=> deviceB.i;
  }

}