There is a very simple explanation of why TLC is evaluating both
clauses of the disjunction even when the first is true. Consider the
spec with this initial predicate and next state relation:
Init == x = 22
Next == \/ /\ x > 7
/\ x' = 42
\/ /\ x > 9
/\ x' = 24
Would you expect TLC never to find the state with x = 24 because when
evaluating Next, it always finds the first disjunct true and therefore
never evaluates the second disjunct?
When evaluating the next-state action, TLC keeps evaluating any
disjunct that might evaluate to true in order to find all possible
next states. There are some cases in which TLC reports an error when,
if it were more clever, it would know that a subexpression it can't
evaluate does not have to be evaluated to determine the set of
possible next states--for example,
Init == x = 0
Next == IF x = "abc" THEN x'= x+1 ELSE x'=x+1
This is not the case in your example, because the value of the first
conjunct of Tick is unspecified if record equals NoRecord, since that
subexpression is then of the form TRUE \/ e where the value of e is
not necessarily a Boolean. Hence, the set of possible next states in
that case is not specified by the semantics of TLA+.
Leslie