#define p ( len( server ) <= MAX_CLIENT )

/*
 * Formula As Typed: [] p
 * The Never Claim Below Corresponds
 * To The Negated Formula !([] p)
 * (formalizing violations of the original)
 */

never {    /* !([] p) */
T0_init:
	if
	:: (! ((p))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

#ifdef NOTES
  Some other properties:
     
     

#endif