Changed so that finish and put_byte in Compressor make a nondeterministic choice over the _tail_ of output (the part that has not yet been read). This sped up animation with ProB (we think) and also made the specification a tad bit more understandable.