| I am not sure that I understand your question (and since nobody else answered, I am perhaps not the only one). In particular, your modified specification has an initial condition, and it is not clear to me why it would somehow indicate that you can get rid of initial conditions. In general, note that nothing in TLA+ requires you to state an initial condition. For example, [][x \in Nat /\ x' = x+1]_x is a well-formed TLA+ formula with well-defined semantics. It can be thought of as a specification that has two kinds of behaviors: - in the first kind, the value of variable x is not a natural number in the initial state, and it never changes along the behavior; - in the second kind, the initial value of x is a natural number and it may increase any number of times along the behavior. You could even rule out the first kind of behaviors by adding a liveness condition such as []<>(x \in Nat) rather than adding the obvious initial condition. Since a specification is a definition, there is nothing "wrong" with the above specification. Whether it is useful is another question. In particular, TLC expects specifications to be of the form Init /\ [][Next]_v /\ L and it expects the initial condition to fix values for all of the variables used in the specification. This is a simplifying assumption, and you could certainly come up with reasonable specifications that do not fix the values of some variables initially because they will be needed only later. This is fairly frequently case in PlusCal when you declare a variable without specifying an initial value; the PlusCal translator then adds default initializations to make TLC happy. Not sure if I even started answering your question – please feel free to rephrase it. Regards, Stephan
|