(************************************************************)
(* Property specification *)
(************************************************************)
property := #synth AGnot(loc[receiver] = FailureR);