[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: About ordinary assignment

As I understand it:
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.


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.