specification Assert_Unsafe
channel_model CCM
entity Env
{
	symbols
           alice, bob : agent;
	   token1, token2 : message;
	entity Alice(Actor, B : agent) 
	{
		body {
			Actor *->* B : token1;
		}
	}
	entity Bob(Actor, A : agent)
	{
		symbols 
			M : message;
		body {
			A *->* Actor : ?M;
			assert Right_Message : M = token2;
		}
	}
	body  {
		new Alice(alice, bob);
		new Bob(bob, alice);
	}
}