// Example of livelock due to endless iteration.
// (List iterator is not guaranteed to reach list end.)

interface IIterator
{
  extern ListElement $int$;
  enum IsPastEnd {Yes, No};
  in IsPastEnd getFirstElmt(ListElement elmt);
  in IsPastEnd getNextElmt(ListElement elmt);

  behaviour
  {
    IsPastEnd isPastEnd = IsPastEnd.Yes;
    on getFirstElmt: {isPastEnd = IsPastEnd.No; reply(isPastEnd);}
    on getFirstElmt: {isPastEnd = IsPastEnd.Yes; reply(isPastEnd);} // empty list
    on getNextElmt: [isPastEnd.No] {isPastEnd = IsPastEnd.Yes; reply(isPastEnd);}
    on getNextElmt: {reply(isPastEnd);}
  }
}

interface IDriver
{
  in void step();

  behaviour
  {
    on step:{}
  }
}

component SynchronousLivelockExternal
{
  provides IDriver pp;
  requires external IIterator listIt;

  behaviour
  {
    IIterator.IsPastEnd consumeListHead()
    {
      IIterator.ListElement elmt;
      IIterator.IsPastEnd v = listIt.getFirstElmt(elmt);
      return v;
    }

    void consumeListTail(IIterator.IsPastEnd pastEnd)
    {
      if (pastEnd == IIterator.IsPastEnd.No)
      {
        IIterator.ListElement elmt;
        pastEnd = listIt.getNextElmt(elmt);
        consumeListTail(pastEnd);
      }
    }

    on pp.step():
    {
      IIterator.IsPastEnd ipe = consumeListHead();
      consumeListTail(ipe);
    }
  }
}