% TESTED FEATURES: private constants
% EXPECTED OUTCOME: Safe
specification PrivateConsts_Safe
channel_model CCM

entity Env
{
	symbols
		bob : agent;
		nonpublic token : message;	
		knows(agent, message) : fact;

	entity Bob(Actor : agent) {
	       symbols
		   M : message;

	       body {
	       	    ? ->* Actor : ?M;
		    knows(Actor, M);
	       }
	}
		
	body {
	     new Bob(bob);
	}

	goals
	     unknown : [](!knows(bob, token));
}