About ordinary assignment

[LUMING DONG]

Hello, I  need to check temporal  properties in my spec and the picture below is the input constant value.  I heard that we'd better not use symmetry set  for such scenario.   

But I am really confused, what's the result of ordinary assignment below instead of choose Model value? 

Terminal == <>[] ( \A cli \in SRVLET: 

                                   /\ CliState[cli] = "work"

                                   /\ CliRegState[cli] = "online"

                                   /\ (\A m \in CliSubedCache[cli] : m \in CliSubInfo[m[1]])

                                    )

TCFSInit == /\ C2SMsgQ = [Cli \in SRVLET |-> <<>>]

        /\ S2CMsgQ = [Cli \in SRVLET |-> <<>>] 

        /\ DataChannel = [Cli \in SRVLET |-> [idx \in SRVLET |-> <<>> ]]

        /\ CliState = [Cli \in SRVLET |-> "PowerOn"]

        /\ CliRegState = [Cli \in SRVLET |-> "offline"]

[Andrew Helwer]

As I understand it:

• Use ordinary assignment to assign the constant a value of any valid TLA+ expression (set of numbers, set of strings, etc.)
• Use model value to assign the constant a value of a singleton object
• Use set of model values to assign the constant a value of a set of singleton objects

So when you run TLC, it creates an object instance for each of your model values. These objects can be checked for equality against each other and nothing else.

Andrew