interface I
{
	in void e();
	behaviour
	{
		enum State { Off, On };
		State state = State.Off;
		[state.Off]
		{
			on e: {state = State.On;}
		}
		[state.On]
		{
			on e: {}
		}
	}
}

interface II
{
	in void e();
	in void ack();
	out void c();
	
	behaviour
	{
		enum State { Off, On, ACKneeded };
		State s = State.Off;
		
		[s.Off]
		{
			on e: { s = State.On; }
			on ack: illegal;
		}
		[s.On]
		{
			on e: illegal;
			on ack: illegal;
			on inevitable: { c; s = State.ACKneeded; }
		}
		[s.ACKneeded]
		{
			on e: illegal;
			on ack: s = State.On;
		}
	}	
}



component LivelockAck
{
	provides I p;
	requires external II r;
	
	behaviour
	{
		enum State { Off, On, Paused };
		State s = State.Off;
		[s.Off]
		{		
			on p.e(): {	r.e(); s=State.On; }
		}
		[s.On]
		{
			on p.e(): {}
			on r.c(): { r.ack(); }
		}
	}
}