constants top = 1000; sets bits = [0,top-1]; actions signal; fluents b: bits -> boolean; vars I:bits; X:boolean; rules b(0):= not prev(b(0)) if signal; b(I):= not prev(b(I)) if not b(I-1) and prev(b(I-1)) and I>0; initially b(I) if I<800, not b(I) if I>=800;