Your specifications are indeed nonsensical--apparently much more
nonsensical than you suspect. You seem to be under the mistaken
impression that a TLA+ specification is some kind of program and the
_expression_ x'=x+1 is an assignment statement that changes the value of
x when it is evaluated.
A TLA+ specification is a formula, and evaluating a formula doesn't
change anything. Starting in the initial state, the possible next
states are specified by all possible values of a' and x' such that
your formula Next is true when x=1 and a=TRUE. To understand what is
going on, I suggest that for each of your definitions of Next, you
find 17 next states that it allows from the initial state. (This
isn't difficult, because there are so many next states that they don't
even form a set.)
When you understand what your specifications mean, you will appreciate
why TLC can't compute their possible behaviors. What particular error
messages TLC produces for them isn't of much interest.
Leslie