Two workers are quadratically better than one: modelling a queue with PRISM