| If you omit "big' = big" in the definition of the action FillSmall, the value of the variable big is completely unconstrained in the successor state (it could be unchanged but also equal 42, {}, "foo" or whatever value). It is almost impossible to reason about a specification that includes such an action, and TLC will produce an error. Leslie's point is to emphasize the fact that a TLA action x' = some_expression is different from the assignment x = some_expression in an imperative programming language such as C.
-- Looking at the "first_number" example, it is easy to see (or check with TLC) that the invariant pc = "middle" => i \in 0 .. 1000 holds of that specification, so adding "i \in 0 .. 1000" as a pre-condition to action Add is redundant. And in fact, the specification also verifies the invariant pc = "start" => i = 0 so the conjunct "i=0" in the Pick action is redundant as well. Of course, there is nothing logically wrong with adding redundant constraints. Stephan
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CC9BC36E-5700-458E-951E-01DA052120B7%40gmail.com. |