Until

Syntax at a glance

a until b

How it works

Until is a future temporal concept in this application. At a conceptual level, a until b asks a to hold while waiting for b; the terminating sample has a different role from the earlier waiting samples. The current parser does not accept this operator.

The useful design question is whether a condition must remain asserted only before a termination event or also on the event's cycle. An example is holding a request while waiting for completion. That question cannot be answered by checking a single delayed endpoint alone.

In the usual non-inclusive until idea, the waiting condition is required before the terminating condition's sample. The related until_with concept includes the termination sample in the waiting requirement. Also distinguish whether termination must eventually happen from what is required while waiting: weak and strong temporal forms differ on that question.

This page intentionally provides a conceptual introduction rather than claiming complete IEEE property semantics. The current finite-trace backend has no implementation of these forms or their termination rules. For supported response-time exercises, use an explicit bounded delay window and the documented finite-trace behavior instead.