make TS dead-ends imply next(False)

and initial dead-end a False at time 0.

Instead of taking the conjunction of all negated states.
This is more explicit and less error-prone.

Otherwise correctness depends also on requiring an xor between states (if bool states) or the proper upper bound on the int state variable.
If one of these is buggy, then the dead-end condition will not be enforced.

Moreover it reduces the spec size and makes it more readable.