#define p (request >= response + error)

/*
 * 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:
     
       [] <> p: p est vérifié une infinité de fois dans le futur
       <> [] p: p est toujours vérifié à partir d'un certain état 

       <> p avec p (request == response + error)

#endif