(************************************************************)
(* Property specification *)
(************************************************************)

property := #synth AGnot(loc[receiver] = FailureR)