Question about Read Independence in LTSmin Paper

[fsankratz]

Hi,

i am not sure if this is the right place for it, but i have a question about the paper "LTSmin: High-Performance Language-Independent Model Checking" concerning the definition of Read Independence:

I can think of two ways of interpreting the definition below, and while i believe the first one makes more sense, i am not sure which one is correct.

1. r_j' is fixed to either be r_j for all r_j or t_j for all r_j, i.e. it cannot vary between two states that only differ in slot j whether the value is copied or overwritten in their successors.
2. the opposite: a different value in state slot j could change the transition behavior from copying to overwriting or the other way around.

Essentially, the question is, whether the part after the AND is implicitly part of the forall quantifier or not.

Thanks in advance for any response!