// purpose: Show example of error pattern.
// The following interface contains the so-called error pattern.
// An device can report an error to its clients and then waits for its
// client to terminate the device and (re)initialize it again.
interface IDevice {
  in void initialize();
  in void open();
  in void close();
  in void terminate();

  out void error();

  behaviour {
    enum State { Uninitialized, Closed, Open, Error };
    State s = State.Uninitialized;

    [s.Uninitialized] {
      on initialize: {s = State.Closed;}
      on open, close: illegal;
    }
    [!s.Uninitialized] {
      on initialize: illegal;

      [s.Closed] {
        on open: {s = State.Open;}
        on close: illegal;
      }
      [s.Open] {
        on open: illegal;
        on close: {s = State.Closed;}
      }

      [!s.Error] {
        on optional: {s = State.Error; error;}
      }
      [s.Error] {
        on open, close: {}
      }
    }

    on terminate: s = State.Uninitialized;
  }
}

// If all interfaces follow the error pattern as described above it
// is for an component easy to recover if a required device report
// and error: upon receiving an error of a required device, the
// error is propagated towards its client and enters the error state.
// In the error state, the component waits for a terminate request
// which will be forwarded to all its required devices. After
// termination, the component and its required devices can be
// (re)initialized again.
component ErrorPattern {
  provides IDevice p;
  requires IDevice a;
  requires IDevice b;

  behaviour {
    enum State { Uninitialized, Closed, Open, Error };
    State s = State.Uninitialized;

    [s.Uninitialized] {
      on p.initialize(): {s = State.Closed; a.initialize(); b.initialize(); }
    }
    [!s.Uninitialized] {
      [s.Closed] {
        on p.open(): {s = State.Open; a.open();	b.open(); }
      }
      [s.Open] {
        on p.close(): {s = State.Closed; a.close(); b.close(); }
      }

      [!s.Error] {
        on a.error(), b.error(): {s = State.Error; p.error(); }
      }
      [s.Error] {
        on p.open(), p.close(): {}
        on a.error(), b.error(): {}
      }
    }

    on p.terminate(): {s = State.Uninitialized; a.terminate(); b.terminate(); }
  }
}