# Re: Specifying a stopping condition

If, at the end of error trace, it says something like "back to state 17", then the error trace is an infinite trace that ends by infinitely repeating the sequence of states from state number 17 through the last displayed state.

Leslie

On Saturday, December 15, 2018 at 4:36:27 PM UTC-8, nickkell at gmail.com wrote:
Hello all!

I've been working on a spec for a print queue, and ideally it should stop when all the items to be printed are either "printed" or "failed". Multiple "worker" applications are competing to be the next to print for any given printer so have to acquire a lock. I also wanted to model what happens when the workers crash and restart. This is the end of the spec (for brevity):

RetrieveNextPrintjob == \E worker \in WORKER, printer \in PRINTER : GetNextForPrinting(worker, printer)
DoPrint == \E worker \in WORKER, printjob \in PRINTJOB : WorkerProcessPrintJob(worker, printjob)
UpdateStatus == \E worker \in WORKER, printjob \in PRINTJOB : HubReceivedPrintJobMessage(worker, printjob)
\/ RetrieveNextPrintjob
\/ DoPrint

Failure == \E worker \in WORKER : WorkerRestart(worker)

Next ==