DEFINED startheight <= height < timeoutheight STARTED (lockinontimeout == false) AND (height < timeoutheight) AND (threshold reached) OR (lockinontimeout == true) AND ((height >= timeoutheight) OR (threshold reached)) LOCKED_IN Always ACTIVE FAILING timeoutheight <= height (lockinontimeout == false) AND (timeoutheight <= height) NOT all blocks signal all blocks signal FAILED