property := #synth AGnot(loc[observer] = obs_BAD);