Specifying a stopping condition

[nick...@xxxxxxxxx]

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) 
Advance == 
    \/ RetrieveNextPrintjob    
    \/ DoPrint
    \/ UpdateStatus

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

Next ==
    \/ Advance
    \/ Failure    
    
PQ == Init /\ [][Next]_vars

AllPrintJobsFinished == \A printjob \in PRINTJOB : printjobState[printjob] \in {"printed","failed"}

Spec == PQ /\ SF_vars(Advance)

Liveness == <>[]AllPrintJobsFinished


The model checker seems to report that after a WorkerRestart, it goes back to a previous state. Does this mean it will repeatedly flip back and forth without terminating?