// Commentary:
//
// This model demonstrates a possible livelock in a component.  Here an
// initial h.hello enter into a potential infinite synchronous loop,
// unless bye is chosen over world by the implementation behind the
// iworld interface.
//
// Code:

interface ihello
{
  in void hello();

  behavior
  {
    on hello: {}
  }
}

interface iworld
{
  in void hello();
  out void world();
  out void bye();

  behavior
  {
    on hello: world;
    on hello: bye;
  }
}

component livelock
{
  provides ihello h;
  requires iworld w;

  behavior
  {
    on h.hello(): w.hello();
    on w.world(): w.hello();
    on w.bye(): {}
  }
}