Syntax at a glance
busy |-> $stable(data)How it works
$stable(signal) is true when a signal's current sample equals its previous sample. Both a held zero and a held one are stable. At cycle zero, the lab defines $stable as false because no earlier sample exists.
For data = [0, 0, 1, 1, 0], $stable(data) produces [0, 1, 0, 1, 0]. The changes at cycles 2 and 4 make it false. In busy |-> $stable(data), data must be unchanged whenever busy is high. It can change while busy is low.
Checking busy |-> data is not equivalent: that requires data to be high rather than unchanged, rejects a stable zero, and can accept a transition to one. A standalone $stable(data) also differs because it requires stability on every sample, including cycle zero, which is false by definition here.
Stability is local to the endpoint being checked. In req |-> ##2 (ack && $stable(data)), ack must be high at t+2 and data at t+2 must equal data at t+1. This does not require data to stay constant throughout the entire interval from the request to the response.
For cycles with history, data == $past(data) gives the same binary comparison. At cycle zero it can differ because $past returns zero. If your requirement includes the first sample, decide how that initialization should be handled. The introductory stability lesson keeps busy low at cycle zero so no impossible initial stability obligation is created.