property := #synth CycleThrough(loc[pta] = l3);