We unify models of sequential computations which feature progress.

This covers models based on traces, real time, abstract time and Boolean time.

We distinguish finite, aborting, incomplete and actually infinite executions.

The unified model instantiates algebras for iteration and non-terminating executions.

We introduce capped omega algebras to describe fixpoints of bounded affine functions.