# [tlaplus] Re: About ordinary assignment

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

On Tuesday, August 6, 2019 at 5:30:32 AM UTC-7, LUMING DONG wrote:
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"]

--
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/0b66c94f-439b-4ae4-bc62-69abd3b0b34c%40googlegroups.com.